[Version Information]
WALi-OpenNWA version: 3673b90a57074c9f370793780d59fdd8e92f61a6 (2018-02-20 22:40:05 -0600) "Merge branch 'NewtonDuetGaussian' of https://github.com/WaliDev/WALi-OpenNWA into NewtonDuetGaussian"
duet version: e0a1b1e22f1b8f755b70e388abf4b098326cd3c9 (2017-12-11 14:36:14 -0500) "Symbolic bounds always include constant bounds if they exist"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.7.0  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
camlp4               4.02+7  Camlp4 is a system for writing extensible parsers f
cil                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
conf-which                1  Virtual package relying on which
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170712  LR(1) parser generator
mlgmpidl              1.2.4  OCaml interface to the GMP library
num                       0  The Num library for arbitrary-precision integer and
oasis                0.4.10  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.3  A library manager for OCaml
ocamlgraph            1.8.7  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.8  Generate OCaml modules from source files
OCRS               20170905  Recurrence solver based on operational calculus
optcomp                 1.6  Optional compilation with cpp-like directives
ounit                 2.0.0  Unit testing framework loosely based on HUnit. It i
ppx_deriving            3.2  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
Z3                 20161217  Z3 SMT solver

Test Name Output No. of Rounds Result Run Time
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below 1 FAIL0.416
kmp.c below 1 PASS1.361
qsort.c below 4 PASS1.301
speed_pldi09_fig1.c below 1 PASS0.669
speed_pldi09_fig4_2.c below 1 FAIL0.442
speed_pldi09_fig4_4.c below 1 PASS0.613
speed_pldi09_fig4_5.c below 1 PASS0.481
speed_pldi10_ex1.c below 1 PASS1.653
speed_pldi10_ex3.c below 1 PASS0.694
speed_pldi10_ex4.c below 1 PASS0.731
speed_popl10_fig2_1.c below 1 PASS0.626
speed_popl10_fig2_2.c below 1 FAIL0.411
speed_popl10_nested_multiple.c below 1 PASS0.603
speed_popl10_nested_single.c below 1 PASS0.555
speed_popl10_sequential_single.c below 1 PASS0.501
speed_popl10_simple_multiple.c below 1 PASS0.709
speed_popl10_simple_single_2.c below 1 PASS0.93
speed_popl10_simple_single.c below 1 PASS0.421
t07.c below 1 PASS0.567
t08.c below 1 PASS0.488
t09.c below 1 PASS0.452
t10.c below 1 PASS0.425
t11.c below 1 PASS0.624
t13.c below 1 FAIL0.503
t15.c below 1 PASS0.551
t16.c below 1 PASS0.489
t19.c below 1 PASS0.482
t20.c below 1 PASS0.461
t27.c below 1 PASS0.777
t28.c below 1 PASS0.698
t30.c below 1 FAIL0.478
t37.c below 2 PASS0.915
t39.c below 2 PASS0.776
t46.c below 1 PASS0.512
t47.c below 1 PASS0.687
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.002
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.505
qsort_full.c below 4 PASS11.688
rec1-param_safe.c below 2 PASS0.52
rec1-param_unsafe.c below 2 OKAY0.496
rec1_safe.c below 2 PASS0.492
rec1_unsafe.c below 2 OKAY0.468
rec2-param_safe.c below 2 PASS0.499
rec2-param_unsafe.c below 2 OKAY0.457
rec2_safe.c below 2 PASS0.493
rec2_unsafe.c below 2 OKAY0.48
rec-test.c below 2 PASS0.471
sas03_bothbranches.c below 7 PASS1.19
sas03.c below 2 PASS0.888
simulated_lese_recursive.c below 2 PASS0.636
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.283
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.384
count_up_down_unsafe.c below 1 OKAY0.403
divide.c below 1 PASS0.417
factor_unsafe.c below 1 OKAY0.358
for_infinite_loop_1_safe.c below 1 PASS0.341
for_infinite_loop_2_safe.c below 1 PASS0.351
interproc.c below 1 PASS0.326
mult.c below 1 PASS0.362
pointer_arith.c below 1 PASS0.332
quotient.c below 3 PASS0.731
subtract.c below 1 PASS0.37
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.386
sum01_bug02_unsafe.c below 1 OKAY0.693
sum01_real_safe.c below 1 PASS0.384
sum01_safe.c below 1 PASS0.396
sum01_unsafe.c below 1 OKAY0.58
sum02_safe.c below 1 PASS0.426
sum03_safe.c below 1 PASS0.492
sum03_unsafe.c below 1 OKAY0.607
sum04_safe.c below 1 PASS0.407
sum04_unsafe.c below 1 OKAY0.594
terminator_02_safe.c below 1 PASS0.358
terminator_02_unsafe.c below 1 OKAY0.408
terminator_03_safe.c below 1 PASS0.36
terminator_03_unsafe.c below 1 OKAY0.374
token_ring01_safe.c below 4 FAIL126.849
token_ring01_unsafe.c below 4 OKAY207.831
toy_safe.c below EXCEPTION 126.532
trex01_safe.c below 1 PASS0.796
trex01_unsafe.c below 1 OKAY0.459
trex02_safe2.c below 3 PASS0.548
trex02_safe.c below 3 PASS0.54
trex02_unsafe.c below 3 OKAY0.562
trex03_safe.c below 1 PASS0.527
trex03_unsafe.c below 1 OKAY0.521
trex04_safe.c below 1 PASS0.387
while_infinite_loop_1_safe.c below 1 PASS0.343
while_infinite_loop_2_safe.c below 1 PASS0.332
while_infinite_loop_3_safe.c below 1 PASS0.335
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 477.402
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.544
blogger_simplified1.c below 3 PASS1.67
divided_difference2.c below TIMEOUT 300.006
mult-proc.c below 3 PASS0.536
mult-proc-params.c below 3 PASS0.525
popall.c below 1 PASS0.955
simulated_scc.c below 1 PASS0.804
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.04
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.407
degree2_binomial.c below 1 PASS0.917
degree2_monomial.c below 1 PASS0.507
degree3_binomial.c below 1 FAIL4.874
degree3_monomial.c below 1 PASS1.009
degree4_binomial.c below 1 FAIL5.161
degree4_monomial.c below 1 PASS1.644
degree5_binomial.c below 1 FAIL15.85
degree5_monomial.c below 1 PASS3.014
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 33.383
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.518
cubic_with_square_interproc.c below 2 FAIL0.723
cubic_with_square_nonlinear.c below 1 FAIL0.667
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.746
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.632
cubic_with_square_unsafe.c below 1 OKAY0.526
multi-input.c below 1 FAIL10.035
multi-input_unsafe.c below 1 OKAY10.25
nondet_loop_bound.c below 1 FAIL0.57
nondet_loop_bound_quartic.c below 1 FAIL0.756
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.772
nondet_loop_bound_unsafe.c below 1 OKAY0.566
nonlinear_stratified.c below 1 PASS121.687
nonlinear_stratified_unsafe.c below 1 OKAY68.968
quartic_with_cube.c below 1 FAIL0.679
quartic_with_cube_nonlinear.c below 1 FAIL0.989
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.981
quartic_with_cube_unsafe.c below 1 OKAY0.578
quintic_with_quartic.c below 1 PASS1.094
quintic_with_quartic_nonlinear.c below 1 PASS1.195
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.148
quintic_with_quartic_unsafe.c below 1 OKAY1.103
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 225.183
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.074
degree2_FD_AllAux_AllAssm.c below 1 PASS106.208
degree2_FD_AllAux_FewAssm.c below 1 PASS7.093
degree2_FD_FewAux_FewAssm.c below 1 PASS1.373
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.355
degree3.c below 1 PASS1.164
degree3_FD.c below 1 PASS1.27
degree4.c below 1 PASS1.91
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 121.447
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.529
loop_unsafe.c below 1 OKAY0.547
simulated_lese_parser.c below 1 PASS0.398
simulated_lese_sentinel.c below 1 PASS0.408
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.882
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.428
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.428
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.007
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.007
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.4
array_false-unreach-call2.c below 1 OKAY0.418
array_false-unreach-call3.c below 1 OKAY0.378
array_true-unreach-call1.c below 1 FAIL0.392
array_true-unreach-call2.c below 1 FAIL0.42
array_true-unreach-call3.c below 1 PASS0.38
array_true-unreach-call4.c below 1 FAIL0.391
const_false-unreach-call1.c below 1 OKAY0.413
const_true-unreach-call1.c below 1 PASS0.407
diamond_false-unreach-call1.c below 1 OKAY0.393
diamond_true-unreach-call1.c below 1 PASS0.388
diamond_true-unreach-call2.c below 1 PASS0.415
functions_false-unreach-call1.c below 3 OKAY0.511
functions_true-unreach-call1.c below 3 PASS0.518
multivar_false-unreach-call1.c below 1 OKAY0.394
multivar_true-unreach-call1.c below 1 PASS0.401
nested_false-unreach-call1.c below 1 OKAY0.48
nested_true-unreach-call1.c below 1 PASS0.468
overflow_true-unreach-call1.c below 1 PASS0.357
phases_false-unreach-call1.c below 1 OKAY0.496
phases_false-unreach-call2.c below 1 OKAY0.386
phases_true-unreach-call1.c below 1 PASS0.502
phases_true-unreach-call2.c below 1 PASS0.386
simple_false-unreach-call1.c below 1 OKAY0.363
simple_false-unreach-call2.c below 1 OKAY0.369
simple_false-unreach-call3.c below 1 OKAY0.36
simple_false-unreach-call4.c below 1 OKAY0.364
simple_true-unreach-call1.c below 1 PASS0.357
simple_true-unreach-call2.c below 1 PASS0.352
simple_true-unreach-call3.c below 1 PASS0.364
simple_true-unreach-call4.c below 1 PASS0.369
underapprox_false-unreach-call1.c below 1 OKAY0.392
underapprox_false-unreach-call2.c below 1 OKAY0.403
underapprox_true-unreach-call1.c below 1 FAIL0.417
underapprox_true-unreach-call2.c below 1 PASS0.408
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.212
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.52
apache-get-tag_true-unreach-call.c below 1 FAIL0.596
down_true-unreach-call.c below 1 PASS0.469
fragtest_simple_true-unreach-call.c below 1 PASS0.587
half_2_true-unreach-call.c below 1 PASS0.483
heapsort_true-unreach-call.c below 1 PASS2.301
id_build_true-unreach-call.c below 1 PASS0.428
id_trans_false-unreach-call.c below 1 OKAY0.36
id_trans_true-unreach-call.c below 1 PASS0.378
large_const_true-unreach-call.c below 1 PASS0.511
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.466
nested6_true-unreach-call.c below 1 FAIL0.632
nested9_true-unreach-call.c below 1 PASS0.694
nest-if3_true-unreach-call.c below 1 PASS0.574
NetBSD_loop_true-unreach-call.c below 1 PASS0.382
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.469
seq_true-unreach-call.c below 1 PASS0.547
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.602
string_concat-noarr_true-unreach-call.c below 1 PASS0.498
up_true-unreach-call.c below 1 PASS0.458
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 13.955
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.438
bhmr2007_true-unreach-call.c below 1 PASS0.46
cggmp2005b_true-unreach-call.c below 1 PASS0.632
cggmp2005_true-unreach-call.c below 1 PASS0.411
cggmp2005_variant_true-unreach-call.c below 1 PASS0.436
css2003_true-unreach-call.c below 1 PASS1.122
ddlm2013_true-unreach-call.c below 1 PASS0.609
gcnr2008_false-unreach-call.c below 1 OKAY1.11
gj2007b_true-unreach-call.c below 1 FAIL0.44
gj2007_true-unreach-call.c below 1 PASS0.573
gr2006_true-unreach-call.c below 1 PASS0.566
gsv2008_true-unreach-call.c below 1 PASS0.393
hhk2008_true-unreach-call.c below 1 PASS0.381
jm2006_true-unreach-call.c below 1 PASS0.534
jm2006_variant_true-unreach-call.c below 1 PASS0.638
mcmillan2006_true-unreach-call.c below 1 FAIL0.46
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.203
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.363
count_by_1_variant_true-unreach-call.c below 1 PASS0.481
count_by_2_true-unreach-call.c below 1 PASS0.366
count_by_k_true-unreach-call.c below 1 PASS0.362
count_by_nondet_true-unreach-call.c below 1 PASS0.389
gauss_sum_true-unreach-call.c below 1 PASS0.431
half_true-unreach-call.c below 1 FAIL0.44
nested_true-unreach-call.c below 1 PASS0.544
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.376
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.443
array_true-unreach-call.c below 1 FAIL0.435
bubble_sort_false-unreach-call.c below 4 OKAY77.679
bubble_sort_true-unreach-call.c below 1 PASS5.186
compact_false-unreach-call.c below 1 OKAY0.466
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.405
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.392
eureka_01_false-unreach-call.c below 1 OKAY2.637
eureka_01_true-unreach-call.c below 1 FAIL1.59
eureka_05_true-unreach-call.c below 1 FAIL0.852
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.379
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.384
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.369
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.36
heavy_false-unreach-call.c below 1 OKAY0.6
heavy_true-unreach-call.c below 1 PASS0.593
insertion_sort_false-unreach-call.c below 1 OKAY1.52
insertion_sort_true-unreach-call.c below 1 FAIL0.639
invert_string_false-unreach-call.c below 1 OKAY0.612
invert_string_true-unreach-call.c below 1 FAIL0.641
linear_sea.ch_true-unreach-call.c below 1 FAIL0.41
linear_search_false-unreach-call.c below 1 OKAY0.438
lu.cmp_true-unreach-call.c below 3 PASS27.465
ludcmp_false-unreach-call.c below 3 OKAY27.202
matrix_false-unreach-call_true-termination.c below 1 OKAY1.373
matrix_true-unreach-call_true-termination.c below 1 FAIL0.508
n.c11_true-unreach-call.c below 3 FAIL0.573
n.c24_false-unreach-call.c below 3 OKAY5.341
n.c40_true-unreach-call.c below 1 FAIL0.405
nec11_false-unreach-call.c below 1 OKAY0.405
nec20_false-unreach-call.c below 1 OKAY0.438
nec40_true-unreach-call.c below 1 FAIL0.406
string_false-unreach-call.c below 1 OKAY0.762
string_true-unreach-call.c below 1 FAIL0.717
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.748
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.389
sum01_false-unreach-call_true-termination.c below 1 OKAY0.598
sum01_true-unreach-call_true-termination.c below 1 PASS0.401
sum03_false-unreach-call_true-termination.c below 1 OKAY0.628
sum03_true-unreach-call_false-termination.c below 1 PASS0.513
sum04_false-unreach-call_true-termination.c below 1 OKAY0.584
sum04_true-unreach-call_true-termination.c below 1 PASS0.407
sum_array_false-unreach-call.c below 1 OKAY0.663
sum_array_true-unreach-call.c below 1 FAIL0.703
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.36
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.624
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.427
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.363
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.358
trex01_false-unreach-call_true-termination.c below 3 OKAY0.609
trex01_true-unreach-call.c below 3 PASS0.926
trex02_false-unreach-call_true-termination.c below 3 OKAY0.547
trex02_true-unreach-call_true-termination.c below 3 PASS0.548
trex03_false-unreach-call_true-termination.c below 3 OKAY0.841
trex03_true-unreach-call.c below 3 PASS0.844
trex04_true-unreach-call_false-termination.c below 1 PASS0.416
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.396
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.241
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.428
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.415
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.091
vogal_false-unreach-call.c below 1 OKAY0.948
vogal_true-unreach-call.c below 1 FAIL0.907
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.326
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.332
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.349
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.345
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 194.9
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.6
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.553
Ackermann03_true-unreach-call.c below 7 FAIL1.555
Ackermann04_true-unreach-call.c below 7 FAIL1.569
Addition01_true-unreach-call_true-termination.c below 2 PASS0.838
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.834
Addition03_false-no-overflow.c below 2 PASS0.832
Addition03_true-unreach-call.c below 2 PASS0.815
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.606
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.558
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.56
Fibonacci01_true-unreach-call.c below TIMEOUT 300.004
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.005
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.007
gcd01_true-unreach-call_true-termination.c below 2 PASS0.72
gcd02_true-unreach-call.c below 2 FAIL1.437
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.29
McCarthy91_true-unreach-call.c below 7 FAIL1.253
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.768
Primes_true-unreach-call.c below 3 FAIL2.266
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.593
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.493
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.493
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.659
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.576
afterrec_2calls_true-unreach-call.c below 2 PASS0.57
afterrec_false-unreach-call.c below 2 OKAY0.475
afterrec_true-unreach-call.c below 2 PASS0.462
fibo_10_false-unreach-call.c below TIMEOUT 300.004
fibo_10_true-unreach-call.c below TIMEOUT 300.006
fibo_15_false-unreach-call.c below TIMEOUT 300.005
fibo_15_true-unreach-call.c below TIMEOUT 300.004
fibo_20_false-unreach-call.c below TIMEOUT 300.006
fibo_20_true-unreach-call.c below TIMEOUT 300.004
fibo_25_false-unreach-call.c below TIMEOUT 300.006
fibo_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.009
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.005
fibo_5_false-unreach-call.c below TIMEOUT 300.004
fibo_5_true-unreach-call.c below TIMEOUT 300.007
fibo_7_false-unreach-call.c below TIMEOUT 300.005
fibo_7_true-unreach-call.c below TIMEOUT 300.006
id2_b2_o3_true-unreach-call.c below 2 PASS0.93
id2_b3_o2_false-unreach-call.c below 2 OKAY0.962
id2_b3_o5_true-unreach-call.c below 2 PASS0.952
id2_b5_o10_true-unreach-call.c below 2 PASS0.952
id2_i5_o5_false-unreach-call.c below 2 OKAY0.56
id2_i5_o5_true-unreach-call.c below 2 PASS0.562
id_b2_o3_true-unreach-call.c below 2 PASS0.867
id_b3_o2_false-unreach-call.c below 2 OKAY0.826
id_b3_o5_true-unreach-call.c below 2 PASS0.823
id_b5_o10_true-unreach-call.c below 2 PASS0.811
id_i10_o10_false-unreach-call.c below 2 OKAY0.517
id_i10_o10_true-unreach-call.c below 2 PASS0.51
id_i15_o15_false-unreach-call.c below 2 OKAY0.482
id_i15_o15_true-unreach-call.c below 2 PASS0.521
id_i20_o20_false-unreach-call.c below 2 OKAY0.5
id_i20_o20_true-unreach-call.c below 2 PASS0.5
id_i25_o25_false-unreach-call.c below 2 OKAY0.507
id_i25_o25_true-unreach-call.c below 2 PASS0.511
id_i5_o5_false-unreach-call.c below 2 OKAY0.504
id_i5_o5_true-unreach-call.c below 2 PASS0.503
id_o1000_false-unreach-call.c below 2 OKAY0.502
id_o100_false-unreach-call.c below 2 OKAY0.504
id_o10_false-unreach-call.c below 2 OKAY0.523
id_o200_false-unreach-call.c below 2 OKAY0.504
id_o20_false-unreach-call.c below 2 OKAY0.503
id_o3_false-unreach-call.c below 2 OKAY0.501
sum_10x0_false-unreach-call.c below 2 OKAY0.552
sum_10x0_true-unreach-call.c below 2 PASS0.544
sum_15x0_false-unreach-call.c below 2 OKAY0.558
sum_15x0_true-unreach-call.c below 2 PASS0.537
sum_20x0_false-unreach-call.c below 2 OKAY0.592
sum_20x0_true-unreach-call.c below 2 PASS0.556
sum_25x0_false-unreach-call.c below 2 OKAY0.573
sum_25x0_true-unreach-call.c below 2 PASS0.563
sum_2x3_false-unreach-call.c below 2 OKAY0.543
sum_2x3_true-unreach-call.c below 2 PASS0.559
sum_non_eq_false-unreach-call.c below 2 OKAY0.571
sum_non_eq_true-unreach-call.c below 2 PASS0.568
sum_non_false-unreach-call.c below 2 OKAY0.572
sum_non_true-unreach-call.c below 2 PASS0.574
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.44
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-lit
rec-afnp2014_true-unreach-call.c below 2 PASS0.551
rec-bhmr2007_true-unreach-call.c below 2 PASS0.584
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.101
rec-cggmp2005_true-unreach-call.c below 2 PASS0.529
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.539
rec-css2003_true-unreach-call.c below 2 PASS1.494
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.005
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.121
rec-gj2007b_true-unreach-call.c below 2 FAIL0.508
rec-gj2007_true-unreach-call.c below 2 FAIL0.649
rec-gr2006_true-unreach-call.c below 2 FAIL0.689
rec-gsv2008_true-unreach-call.c below 2 PASS0.547
rec-hhk2008_true-unreach-call.c below 2 PASS0.509
rec-jm2006_true-unreach-call.c below 2 PASS0.644
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.735
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.62
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.825
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c below 2 PASS0.467
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.559
rec-count_by_2_true-unreach-call.c below 2 PASS0.461
rec-count_by_k_true-unreach-call.c below 2 PASS0.523
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.527
rec-gauss_sum_true-unreach-call.c below 2 PASS0.549
rec-half_true-unreach-call.c below 2 FAIL0.531
rec-nested_true-unreach-call.c below 3 FAIL0.864
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.481
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.62
cubic_polynomial_unsafe.c below 2 OKAY0.644
edit_distance_bottom_up.c below 3 FAIL184.848
edit_distance_top_down.c below 3 FAIL5.218
log_log_n_solution.c below 3 FAIL0.6
log_log_n_solution_unsafe.c below 3 OKAY0.596
log_n_solution.c below 2 FAIL0.59
log_n_solution_unsafe.c below 2 OKAY0.613
multivariate_1.c below TIMEOUT 300.096
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL3.515
multivariate_higher_order_unsafe.c below 7 OKAY3.453
n_cubed_solution.c below EXCEPTION 99.83
n_cubed_solution_unsafe.c below EXCEPTION 0.025
n_log_n_solution.c below 8 FAIL1.595
n_log_n_solution_unsafe.c below 8 OKAY1.624
n_squared_two_base_case_even.c below 2 PASS0.681
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.707
n_squared_two_base_case_odd.c below 2 PASS0.73
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.703
pascals_dynamic.c below 3 FAIL2.648
pascals_dynamic_unsafe.c below 3 OKAY2.568
pascals_iterative.c below 1 FAIL4.906
pascals_iterative_unsafe.c below 1 OKAY5.008
pascals_recursive.c below 8 FAIL3.635
pascals_recursive_unsafe.c below 8 OKAY3.666
squared_solution.c below 8 FAIL3.053
squared_solution_unsafe.c below 8 OKAY3.146
two_n_even.c below 2 PASS0.53
two_n_even_unsafe.c below 2 OKAY0.517
two_n_odd.c below 2 PASS0.542
two_n_odd_unsafe.c below 2 OKAY0.533
two_to_n_over_two_even.c below 7 FAIL127.825
two_to_n_over_two_even_unsafe.c below 7 OKAY285.149
two_to_n_over_two_odd.c below 7 FAIL245.93
two_to_n_over_two_odd_unsafe.c below 7 OKAY136.426
two_to_n_squared.c below 5 FAIL19.843
two_to_n_squared_unsafe.c below 5 OKAY20.107
two_to_two_to_n.c below 7 FAIL1.446
two_to_two_to_n_unsafe.c below 7 OKAY1.434
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1775.605
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.406
adding_and_mult_unsafe.c below 1 OKAY0.432
binary_search_array_tree.c below 1 FAIL0.816
exp_add_linear.c below 1 PASS0.535
exp_add_linear_unsafe.c below 1 OKAY0.541
exp_add_loop_rec.c below 1 FAIL0.401
exp_add_loop_rec_unsafe.c below 1 OKAY0.421
exp_add_loop_variable.c below 1 PASS0.506
exp_add_loop_variable_unsafe.c below 1 OKAY0.507
exp_with_linear_inner_loop.c below 1 FAIL0.611
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.629
halving_log1.c below 1 FAIL0.686
linear_two_to_n.c below 7 FAIL1.737
linear_two_to_n_unsafe.c below 7 OKAY1.79
loop_five_to_n.c below 1 PASS0.464
loop_five_to_n_unsafe.c below 1 OKAY0.488
non_loop_five_to_n.c below 7 FAIL54.004
non_loop_five_to_n_unsafe.c below 7 OKAY54.331
power_log_modified.c below 1 PASS0.663
simple_exponential.c below 1 PASS0.458
simple_exponential_for.c below 1 PASS0.47
simple_exponential_for_unsafe.c below 1 OKAY0.5
simple_exponential_unsafe.c below 1 OKAY0.466
two_to_n_minus_n.c below 7 FAIL2.392
two_to_n_minus_n_loop.c below TIMEOUT 300.004
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.007
two_to_n_minus_n_unsafe.c below 7 OKAY2.345
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 726.61
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.709
02.c below 3 FAIL0.895
03.c below 1 PASS0.524
04.c below 1 PASS0.375
05.c below 3 PASS1.333
06.c below 3 FAIL10.05
07.c below 3 PASS0.744
08.c below 3 PASS1.56
09.c below 3 PASS1.039
10.c below 3 FAIL1.259
11.c below 1 PASS0.397
12.c below 3 PASS1.616
13.c below 3 PASS0.696
14.c below 3 PASS0.591
15.c below 1 PASS0.376
16.c below 1 PASS0.554
17.c below 1 PASS3.471
18.c below 1 PASS0.47
19.c below 1 PASS0.558
20.c below 3 FAIL0.798
21.c below 3 PASS0.656
22.c below 3 FAIL0.91
23.c below 1 PASS0.419
24.c below 1 PASS0.48
25.c below 3 FAIL1.702
26.c below TIMEOUT 300.004
27.c below 1 PASS0.538
28.c below 3 PASS0.686
29.c below 3 PASS1.152
30.c below 1 PASS0.413
31.c below 3 PASS1.327
32.c below 1 FAIL0.421
33.c below 3 PASS1.359
34.c below 1 FAIL0.445
35.c below 1 PASS0.371
36.c below 3 PASS2.768
37.c below 3 FAIL0.628
38.c below 1 FAIL0.438
39.c below 3 PASS0.552
40.c below 3 PASS0.945
41.c below 1 PASS0.437
42.c below 3 PASS0.983
43.c below 3 PASS0.685
44.c below 1 PASS0.419
45.c below 3 FAIL2.897
46.c below 3 FAIL1.988
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 351.638
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.491
AGHKTW2017_foo.c below 1 PASS0.501
AGHKTW2017_loginSafe.c below 1 PASS1.025
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.565
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.58
BCK2011_gauss.c below 1 PASS0.524
BCK2011_strength_reduction.c below 1 PASS0.836
BCK2011_strength_reduction_linear.c below 1 PASS0.539
CFD17-add-const_product.c below 1 PASS0.386
CFD17-add-const_product-syntax.c below 1 PASS0.5
CFD17-add-const_self-comp.c below 1 FAIL0.447
collatz_product-syntax.c below 1 FAIL17.747
collatz_self-comp.c below 1 FAIL1.886
fibonacci_information_flow.c below 1 PASS0.647
halving_log1_product.c below 1 PASS0.745
halving_log1_product-syntax.c below 1 PASS0.858
halving_log1_self-comp.c below 1 FAIL0.595
loop_splitting_test_safe.c below 1 PASS0.685
TA2005_fib2.c below 1 PASS0.693
TA2005_fib.c below 1 PASS0.555
top-level-if-add-const_product.c below 1 PASS1.02
top-level-if-add-const_self-comp.c below 1 FAIL0.602
ICRA Assertions (True) = 16/21
ICRA Assertions (False) = 1/1
ICRA Time = 32.427
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.851
c3_cleanup_better.c below 3 PASS1.697
c3_cleanup.c below 3 PASS1.721
c3_intermediate.c below 3 PASS1.692
c3_noinv.c below 3 FAIL1.433
doublers.c below 1 FAIL0.67
doublers_easier.c below 3 FAIL1.294
doublers_easy.c below 1 FAIL0.749
exp_mult.c below 1 FAIL0.427
fig1_rotation_unsafe.c below 1 OKAY0.477
guessing_game.c below 3 FAIL0.609
not_P_solvable.c below 1 PASS0.394
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 12.014
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.443
maxequals_linear_1.c below 1 PASS0.664
maxequals_linear_2.c below 1 PASS0.638
maxequals_linear_3.c below 1 FAIL0.423
maxequals_linear_4.c below 1 PASS0.427
maxequals_linear_5.c below 1 PASS0.436
maxequals_linear_6.c below 1 FAIL0.439
maxequals_matrix1.c below 3 FAIL1.677
maxequals_matrix2.c below 3 FAIL1.612
maxequals_quadratic1.c below 1 FAIL0.44
maxequals_quadratic2.c below 1 PASS0.422
maxequals_stratified1.c below 3 PASS4.858
maxequals_stratified2.c below 3 PASS5.07
maxequals_stratified3.c below 3 FAIL5.353
nine.c below 1 FAIL0.438
nine_nondecreasing.c below 1 PASS0.674
sum_interval_1.c below 1 FAIL0.509
sum_interval_2.c below 1 FAIL0.484
sum_interval_3.c below 1 FAIL0.527
TrackingObjectFields.c below 3 PASS10.908
TrackingObjectFields_inlined.c below 1 PASS3.185
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 39.627
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.501
bobble2_varloop.c below 1 PASS0.464
bobble3.c below TIMEOUT 300.005
bobble4.c below 1 FAIL0.455
bobble5.c below 1 FAIL0.466
bobble.c below 1 PASS0.458
inchworm2.c below 1 TIMEOUT300.006
inchworm3.c below 1 PASS0.502
inchworm4.c below 1 PASS0.499
inchworm5.c below 1 PASS0.47
inchworm6_unsafe.c below 1 OKAY0.464
inchworm.c below 1 FAIL0.474
leapdiff2.c below 1 TIMEOUT300.004
leapfrog_annotated.c below 1 FAIL0.481
leapfrog_annotated_disjunction.c below 1 PASS0.49
leapfrog_asymmetric2.c below 1 FAIL0.534
leapfrog_asymmetric3.c below 1 FAIL0.557
leapfrog_asymmetric.c below 1 FAIL0.503
leapfrog.c below 1 FAIL0.449
leapfrog_materialized.c below 1 FAIL0.481
leapfrog_verbose.c below 1 FAIL0.48
leapspin.c below 1 FAIL0.417
leapsum2.c below 1 TIMEOUT300.006
leapthree.c below 1 FAIL0.484
microbobble2.c below 1 PASS0.43
microbobble3.c below 1 PASS0.443
microbobble_asymmetric.c below 1 PASS0.437
microbobble.c below 1 FAIL0.434
simple_bl2.c below 1 FAIL0.469
simple_bl3.c below 1 FAIL0.397
simple_bl.c below 1 FAIL0.48
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1212.74
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.336
binval_example_2_unsafe.c below 1 OKAY0.363
binval_example_3_unsafe.c below 1 OKAY0.343
binval_example_4.c below 1 PASS0.418
binval_example_4_unsafe.c below 1 OKAY0.404
binval_example_5.c below 1 FAIL1.595
binval_example_5_unsafe.c below 1 OKAY3.683
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.142