[Version Information]
WALi-OpenNWA version: f73a8d6dbe21a2004e864fa68f50e0f3de181d25 (2017-12-06 13:06:14 -0600) "Adding guessing_game.c benchmark"
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.425
kmp.c below 1 PASS1.347
qsort.c below 4 PASS1.286
speed_pldi09_fig1.c below 1 PASS0.67
speed_pldi09_fig4_2.c below 1 FAIL0.484
speed_pldi09_fig4_4.c below 1 PASS0.634
speed_pldi09_fig4_5.c below 1 PASS0.471
speed_pldi10_ex1.c below 1 PASS1.657
speed_pldi10_ex3.c below 1 PASS0.691
speed_pldi10_ex4.c below 1 PASS0.764
speed_popl10_fig2_1.c below 1 PASS0.622
speed_popl10_fig2_2.c below 1 FAIL0.437
speed_popl10_nested_multiple.c below 1 PASS0.574
speed_popl10_nested_single.c below 1 PASS0.562
speed_popl10_sequential_single.c below 1 PASS0.496
speed_popl10_simple_multiple.c below 1 PASS0.721
speed_popl10_simple_single_2.c below 1 PASS0.923
speed_popl10_simple_single.c below 1 PASS0.422
t07.c below 1 PASS0.562
t08.c below 1 PASS0.509
t09.c below 1 PASS0.46
t10.c below 1 PASS0.433
t11.c below 1 PASS0.618
t13.c below 1 FAIL0.527
t15.c below 1 PASS0.526
t16.c below 1 PASS0.512
t19.c below 1 PASS0.48
t20.c below 1 PASS0.46
t27.c below 1 PASS0.752
t28.c below 1 PASS0.728
t30.c below 1 FAIL0.497
t37.c below 2 PASS0.901
t39.c below 2 PASS0.786
t46.c below 1 PASS0.515
t47.c below 1 PASS0.675
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.127
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.495
qsort_full.c below 4 PASS11.811
rec1-param_safe.c below 2 PASS0.525
rec1-param_unsafe.c below 2 OKAY0.527
rec1_safe.c below 2 PASS0.49
rec1_unsafe.c below 2 OKAY0.484
rec2-param_safe.c below 2 PASS0.494
rec2-param_unsafe.c below 2 OKAY0.467
rec2_safe.c below 2 PASS0.493
rec2_unsafe.c below 2 OKAY0.471
rec-test.c below 2 PASS0.467
sas03_bothbranches.c below 7 PASS1.2
sas03.c below 2 PASS0.93
simulated_lese_recursive.c below 2 PASS0.65
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.504
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.393
count_up_down_unsafe.c below 1 OKAY0.393
divide.c below 1 PASS0.412
factor_unsafe.c below 1 OKAY0.366
for_infinite_loop_1_safe.c below 1 PASS0.356
for_infinite_loop_2_safe.c below 1 PASS0.364
interproc.c below 1 PASS0.315
mult.c below 1 PASS0.37
pointer_arith.c below 1 PASS0.338
quotient.c below 3 PASS0.726
subtract.c below 1 PASS0.37
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.387
sum01_bug02_unsafe.c below 1 OKAY0.752
sum01_real_safe.c below 1 PASS0.413
sum01_safe.c below 1 PASS0.414
sum01_unsafe.c below 1 OKAY0.591
sum02_safe.c below 1 PASS0.428
sum03_safe.c below 1 PASS0.469
sum03_unsafe.c below 1 OKAY0.604
sum04_safe.c below 1 PASS0.414
sum04_unsafe.c below 1 OKAY0.622
terminator_02_safe.c below 1 PASS0.354
terminator_02_unsafe.c below 1 OKAY0.436
terminator_03_safe.c below 1 PASS0.353
terminator_03_unsafe.c below 1 OKAY0.365
token_ring01_safe.c below 4 FAIL130.23
token_ring01_unsafe.c below 4 OKAY206.053
toy_safe.c below EXCEPTION 132.491
trex01_safe.c below 1 PASS0.825
trex01_unsafe.c below 1 OKAY0.447
trex02_safe2.c below 3 PASS0.559
trex02_safe.c below 3 PASS0.537
trex02_unsafe.c below 3 OKAY0.54
trex03_safe.c below 1 PASS0.514
trex03_unsafe.c below 1 OKAY0.5
trex04_safe.c below 1 PASS0.402
while_infinite_loop_1_safe.c below 1 PASS0.325
while_infinite_loop_2_safe.c below 1 PASS0.337
while_infinite_loop_3_safe.c below 1 PASS0.341
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 485.106
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.555
blogger_simplified1.c below 3 PASS1.626
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.51
mult-proc-params.c below 3 PASS0.546
popall.c below 1 PASS0.959
simulated_scc.c below 1 PASS0.832
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.032
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.419
degree2_binomial.c below 1 PASS0.876
degree2_monomial.c below 1 PASS0.494
degree3_binomial.c below 1 FAIL4.836
degree3_monomial.c below 1 PASS1.009
degree4_binomial.c below 1 FAIL5.083
degree4_monomial.c below 1 PASS1.669
degree5_binomial.c below 1 FAIL16.19
degree5_monomial.c below 1 PASS3.186
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 33.762
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.503
cubic_with_square_interproc.c below 2 FAIL0.805
cubic_with_square_nonlinear.c below 1 FAIL0.674
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.727
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.623
cubic_with_square_unsafe.c below 1 OKAY0.528
multi-input.c below 1 FAIL10.518
multi-input_unsafe.c below 1 OKAY10.565
nondet_loop_bound.c below 1 FAIL0.547
nondet_loop_bound_quartic.c below 1 FAIL0.78
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.794
nondet_loop_bound_unsafe.c below 1 OKAY0.546
nonlinear_stratified.c below 1 PASS123.495
nonlinear_stratified_unsafe.c below 1 OKAY70.253
quartic_with_cube.c below 1 FAIL0.701
quartic_with_cube_nonlinear.c below 1 FAIL1.009
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.961
quartic_with_cube_unsafe.c below 1 OKAY0.57
quintic_with_quartic.c below 1 PASS1.134
quintic_with_quartic_nonlinear.c below 1 PASS1.163
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.201
quintic_with_quartic_unsafe.c below 1 OKAY1.222
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 229.319
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.011
degree2_FD_AllAux_AllAssm.c below 1 PASS109.159
degree2_FD_AllAux_FewAssm.c below 1 PASS7.044
degree2_FD_FewAux_FewAssm.c below 1 PASS1.384
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.378
degree3.c below 1 PASS1.091
degree3_FD.c below 1 PASS1.244
degree4.c below 1 PASS1.953
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 124.264
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.548
loop_unsafe.c below 1 OKAY0.563
simulated_lese_parser.c below 1 PASS0.401
simulated_lese_sentinel.c below 1 PASS0.408
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.92
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.406
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.406
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.009
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.009
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.39
array_false-unreach-call2.c below 1 OKAY0.413
array_false-unreach-call3.c below 1 OKAY0.403
array_true-unreach-call1.c below 1 FAIL0.401
array_true-unreach-call2.c below 1 FAIL0.4
array_true-unreach-call3.c below 1 PASS0.398
array_true-unreach-call4.c below 1 FAIL0.391
const_false-unreach-call1.c below 1 OKAY0.398
const_true-unreach-call1.c below 1 PASS0.4
diamond_false-unreach-call1.c below 1 OKAY0.393
diamond_true-unreach-call1.c below 1 PASS0.402
diamond_true-unreach-call2.c below 1 PASS0.43
functions_false-unreach-call1.c below 3 OKAY0.53
functions_true-unreach-call1.c below 3 PASS0.533
multivar_false-unreach-call1.c below 1 OKAY0.412
multivar_true-unreach-call1.c below 1 PASS0.422
nested_false-unreach-call1.c below 1 OKAY0.467
nested_true-unreach-call1.c below 1 PASS0.458
overflow_true-unreach-call1.c below 1 PASS0.358
phases_false-unreach-call1.c below 1 OKAY0.486
phases_false-unreach-call2.c below 1 OKAY0.402
phases_true-unreach-call1.c below 1 PASS0.503
phases_true-unreach-call2.c below 1 PASS0.396
simple_false-unreach-call1.c below 1 OKAY0.358
simple_false-unreach-call2.c below 1 OKAY0.369
simple_false-unreach-call3.c below 1 OKAY0.368
simple_false-unreach-call4.c below 1 OKAY0.383
simple_true-unreach-call1.c below 1 PASS0.394
simple_true-unreach-call2.c below 1 PASS0.363
simple_true-unreach-call3.c below 1 PASS0.362
simple_true-unreach-call4.c below 1 PASS0.373
underapprox_false-unreach-call1.c below 1 OKAY0.429
underapprox_false-unreach-call2.c below 1 OKAY0.414
underapprox_true-unreach-call1.c below 1 FAIL0.42
underapprox_true-unreach-call2.c below 1 PASS0.409
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.428
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.579
apache-get-tag_true-unreach-call.c below 1 FAIL0.597
down_true-unreach-call.c below 1 PASS0.456
fragtest_simple_true-unreach-call.c below 1 PASS0.61
half_2_true-unreach-call.c below 1 PASS0.49
heapsort_true-unreach-call.c below 1 PASS2.254
id_build_true-unreach-call.c below 1 PASS0.431
id_trans_false-unreach-call.c below 1 OKAY0.362
id_trans_true-unreach-call.c below 1 PASS0.383
large_const_true-unreach-call.c below 1 PASS0.52
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.444
nested6_true-unreach-call.c below 1 FAIL0.634
nested9_true-unreach-call.c below 1 PASS0.721
nest-if3_true-unreach-call.c below 1 PASS0.578
NetBSD_loop_true-unreach-call.c below 1 PASS0.394
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.506
seq_true-unreach-call.c below 1 PASS0.564
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.602
string_concat-noarr_true-unreach-call.c below 1 PASS0.513
up_true-unreach-call.c below 1 PASS0.472
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.11
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.428
bhmr2007_true-unreach-call.c below 1 PASS0.447
cggmp2005b_true-unreach-call.c below 1 PASS0.647
cggmp2005_true-unreach-call.c below 1 PASS0.413
cggmp2005_variant_true-unreach-call.c below 1 PASS0.409
css2003_true-unreach-call.c below 1 PASS1.124
ddlm2013_true-unreach-call.c below 1 PASS0.626
gcnr2008_false-unreach-call.c below 1 OKAY1.099
gj2007b_true-unreach-call.c below 1 FAIL0.437
gj2007_true-unreach-call.c below 1 PASS0.585
gr2006_true-unreach-call.c below 1 PASS0.571
gsv2008_true-unreach-call.c below 1 PASS0.404
hhk2008_true-unreach-call.c below 1 PASS0.392
jm2006_true-unreach-call.c below 1 PASS0.551
jm2006_variant_true-unreach-call.c below 1 PASS0.638
mcmillan2006_true-unreach-call.c below 1 FAIL0.461
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.232
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.37
count_by_1_variant_true-unreach-call.c below 1 PASS0.479
count_by_2_true-unreach-call.c below 1 PASS0.366
count_by_k_true-unreach-call.c below 1 PASS0.369
count_by_nondet_true-unreach-call.c below 1 PASS0.395
gauss_sum_true-unreach-call.c below 1 PASS0.422
half_true-unreach-call.c below 1 FAIL0.428
nested_true-unreach-call.c below 1 PASS0.541
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.37
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.448
array_true-unreach-call.c below 1 FAIL0.436
bubble_sort_false-unreach-call.c below 4 OKAY78.174
bubble_sort_true-unreach-call.c below 1 PASS5.167
compact_false-unreach-call.c below 1 OKAY0.478
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.397
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.391
eureka_01_false-unreach-call.c below 1 OKAY2.665
eureka_01_true-unreach-call.c below 1 FAIL1.607
eureka_05_true-unreach-call.c below 1 FAIL0.876
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.403
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.388
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.359
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.363
heavy_false-unreach-call.c below 1 OKAY0.615
heavy_true-unreach-call.c below 1 PASS0.583
insertion_sort_false-unreach-call.c below 1 OKAY1.509
insertion_sort_true-unreach-call.c below 1 FAIL0.63
invert_string_false-unreach-call.c below 1 OKAY0.616
invert_string_true-unreach-call.c below 1 FAIL0.62
linear_sea.ch_true-unreach-call.c below 1 FAIL0.433
linear_search_false-unreach-call.c below 1 OKAY0.426
lu.cmp_true-unreach-call.c below 3 PASS27.759
ludcmp_false-unreach-call.c below 3 OKAY27.627
matrix_false-unreach-call_true-termination.c below 1 OKAY1.331
matrix_true-unreach-call_true-termination.c below 1 FAIL0.531
n.c11_true-unreach-call.c below 3 FAIL0.602
n.c24_false-unreach-call.c below 3 OKAY5.292
n.c40_true-unreach-call.c below 1 FAIL0.4
nec11_false-unreach-call.c below 1 OKAY0.398
nec20_false-unreach-call.c below 1 OKAY0.432
nec40_true-unreach-call.c below 1 FAIL0.408
string_false-unreach-call.c below 1 OKAY0.777
string_true-unreach-call.c below 1 FAIL0.751
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.754
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.378
sum01_false-unreach-call_true-termination.c below 1 OKAY0.625
sum01_true-unreach-call_true-termination.c below 1 PASS0.406
sum03_false-unreach-call_true-termination.c below 1 OKAY0.657
sum03_true-unreach-call_false-termination.c below 1 PASS0.529
sum04_false-unreach-call_true-termination.c below 1 OKAY0.58
sum04_true-unreach-call_true-termination.c below 1 PASS0.399
sum_array_false-unreach-call.c below 1 OKAY0.661
sum_array_true-unreach-call.c below 1 FAIL0.718
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.365
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.635
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.426
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.374
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.377
trex01_false-unreach-call_true-termination.c below 3 OKAY0.623
trex01_true-unreach-call.c below 3 PASS0.923
trex02_false-unreach-call_true-termination.c below 3 OKAY0.567
trex02_true-unreach-call_true-termination.c below 3 PASS0.585
trex03_false-unreach-call_true-termination.c below 3 OKAY0.875
trex03_true-unreach-call.c below 3 PASS0.858
trex04_true-unreach-call_false-termination.c below 1 PASS0.423
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.389
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.457
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.425
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.419
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.094
vogal_false-unreach-call.c below 1 OKAY0.958
vogal_true-unreach-call.c below 1 FAIL0.949
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.362
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.333
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.341
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.355
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 196.712
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.607
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.636
Ackermann03_true-unreach-call.c below 7 FAIL1.593
Ackermann04_true-unreach-call.c below 7 FAIL1.568
Addition01_true-unreach-call_true-termination.c below 2 PASS0.824
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.847
Addition03_false-no-overflow.c below 2 PASS0.863
Addition03_true-unreach-call.c below 2 PASS0.854
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.632
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.581
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.581
Fibonacci01_true-unreach-call.c below TIMEOUT 300.005
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.006
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.007
gcd01_true-unreach-call_true-termination.c below 2 PASS0.747
gcd02_true-unreach-call.c below 2 FAIL1.405
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.304
McCarthy91_true-unreach-call.c below 7 FAIL1.258
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.78
Primes_true-unreach-call.c below 3 FAIL2.246
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.636
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.511
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.509
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1524.01
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.592
afterrec_2calls_true-unreach-call.c below 2 PASS0.543
afterrec_false-unreach-call.c below 2 OKAY0.501
afterrec_true-unreach-call.c below 2 PASS0.474
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.004
fibo_15_true-unreach-call.c below TIMEOUT 300.006
fibo_20_false-unreach-call.c below TIMEOUT 300.005
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.004
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.017
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.017
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.004
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.006
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.006
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.005
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.006
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.006
fibo_7_false-unreach-call.c below TIMEOUT 300.004
fibo_7_true-unreach-call.c below TIMEOUT 300.006
id2_b2_o3_true-unreach-call.c below 2 PASS0.951
id2_b3_o2_false-unreach-call.c below 2 OKAY1.005
id2_b3_o5_true-unreach-call.c below 2 PASS0.952
id2_b5_o10_true-unreach-call.c below 2 PASS0.981
id2_i5_o5_false-unreach-call.c below 2 OKAY0.562
id2_i5_o5_true-unreach-call.c below 2 PASS0.567
id_b2_o3_true-unreach-call.c below 2 PASS0.868
id_b3_o2_false-unreach-call.c below 2 OKAY0.846
id_b3_o5_true-unreach-call.c below 2 PASS0.838
id_b5_o10_true-unreach-call.c below 2 PASS0.829
id_i10_o10_false-unreach-call.c below 2 OKAY0.517
id_i10_o10_true-unreach-call.c below 2 PASS0.497
id_i15_o15_false-unreach-call.c below 2 OKAY0.532
id_i15_o15_true-unreach-call.c below 2 PASS0.497
id_i20_o20_false-unreach-call.c below 2 OKAY0.511
id_i20_o20_true-unreach-call.c below 2 PASS0.511
id_i25_o25_false-unreach-call.c below 2 OKAY0.523
id_i25_o25_true-unreach-call.c below 2 PASS0.52
id_i5_o5_false-unreach-call.c below 2 OKAY0.513
id_i5_o5_true-unreach-call.c below 2 PASS0.513
id_o1000_false-unreach-call.c below 2 OKAY0.515
id_o100_false-unreach-call.c below 2 OKAY0.537
id_o10_false-unreach-call.c below 2 OKAY0.589
id_o200_false-unreach-call.c below 2 OKAY0.502
id_o20_false-unreach-call.c below 2 OKAY0.524
id_o3_false-unreach-call.c below 2 OKAY0.51
sum_10x0_false-unreach-call.c below 2 OKAY0.584
sum_10x0_true-unreach-call.c below 2 PASS0.543
sum_15x0_false-unreach-call.c below 2 OKAY0.565
sum_15x0_true-unreach-call.c below 2 PASS0.56
sum_20x0_false-unreach-call.c below 2 OKAY0.567
sum_20x0_true-unreach-call.c below 2 PASS0.551
sum_25x0_false-unreach-call.c below 2 OKAY0.588
sum_25x0_true-unreach-call.c below 2 PASS0.567
sum_2x3_false-unreach-call.c below 2 OKAY0.59
sum_2x3_true-unreach-call.c below 2 PASS0.555
sum_non_eq_false-unreach-call.c below 2 OKAY0.592
sum_non_eq_true-unreach-call.c below 2 PASS0.566
sum_non_false-unreach-call.c below 2 OKAY0.552
sum_non_true-unreach-call.c below 2 PASS0.575
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.956
/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.567
rec-bhmr2007_true-unreach-call.c below 2 PASS0.591
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.136
rec-cggmp2005_true-unreach-call.c below 2 PASS0.518
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.553
rec-css2003_true-unreach-call.c below 2 PASS1.494
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.165
rec-gj2007b_true-unreach-call.c below 2 FAIL0.505
rec-gj2007_true-unreach-call.c below 2 FAIL0.738
rec-gr2006_true-unreach-call.c below 2 FAIL0.679
rec-gsv2008_true-unreach-call.c below 2 PASS0.518
rec-hhk2008_true-unreach-call.c below 2 PASS0.513
rec-jm2006_true-unreach-call.c below 2 PASS0.65
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.737
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.628
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.996
/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.47
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.559
rec-count_by_2_true-unreach-call.c below 2 PASS0.467
rec-count_by_k_true-unreach-call.c below 2 PASS0.504
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.537
rec-gauss_sum_true-unreach-call.c below 2 PASS0.568
rec-half_true-unreach-call.c below 2 FAIL0.549
rec-nested_true-unreach-call.c below 3 FAIL0.865
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.519
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.646
cubic_polynomial_unsafe.c below 2 OKAY0.67
edit_distance_bottom_up.c below 3 FAIL186.622
edit_distance_top_down.c below 3 FAIL5.282
log_log_n_solution.c below 3 FAIL0.61
log_log_n_solution_unsafe.c below 3 OKAY0.607
log_n_solution.c below 2 FAIL0.594
log_n_solution_unsafe.c below 2 OKAY0.613
multivariate_1.c below TIMEOUT 300.094
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL3.592
multivariate_higher_order_unsafe.c below 7 OKAY3.666
n_cubed_solution.c below EXCEPTION 106.552
n_cubed_solution_unsafe.c below EXCEPTION 0.031
n_log_n_solution.c below 8 FAIL1.846
n_log_n_solution_unsafe.c below 8 OKAY1.858
n_squared_two_base_case_even.c below 2 PASS0.758
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.782
n_squared_two_base_case_odd.c below 2 PASS0.781
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.773
pascals_dynamic.c below 3 FAIL2.944
pascals_dynamic_unsafe.c below 3 OKAY2.897
pascals_iterative.c below 1 FAIL5.544
pascals_iterative_unsafe.c below 1 OKAY5.333
pascals_recursive.c below 8 FAIL3.786
pascals_recursive_unsafe.c below 8 OKAY3.828
squared_solution.c below 8 FAIL3.296
squared_solution_unsafe.c below 8 OKAY3.224
two_n_even.c below 2 PASS0.537
two_n_even_unsafe.c below 2 OKAY0.539
two_n_odd.c below 2 PASS0.543
two_n_odd_unsafe.c below 2 OKAY0.546
two_to_n_over_two_even.c below 7 FAIL194.163
two_to_n_over_two_even_unsafe.c below TIMEOUT 300.008
two_to_n_over_two_odd.c below 7 FAIL253.022
two_to_n_over_two_odd_unsafe.c below 7 OKAY121.896
two_to_n_squared.c below 5 FAIL21.409
two_to_n_squared_unsafe.c below 5 OKAY20.917
two_to_two_to_n.c below 7 FAIL1.524
two_to_two_to_n_unsafe.c below 7 OKAY1.549
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 16/19
ICRA Time = 1863.888
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.438
adding_and_mult_unsafe.c below 1 OKAY0.463
binary_search_array_tree.c below 1 FAIL0.9
exp_add_linear.c below 1 PASS0.574
exp_add_linear_unsafe.c below 1 OKAY0.57
exp_add_loop_rec.c below 1 FAIL0.48
exp_add_loop_rec_unsafe.c below 1 OKAY0.971
exp_add_loop_variable.c below 1 PASS1.135
exp_add_loop_variable_unsafe.c below 1 OKAY1.204
exp_with_linear_inner_loop.c below 1 FAIL1.231
exp_with_linear_inner_loop_unsafe.c below 1 OKAY1.093
halving_log1.c below 1 FAIL1.0
linear_two_to_n.c below 7 FAIL2.08
linear_two_to_n_unsafe.c below 7 OKAY2.434
loop_five_to_n.c below 1 PASS0.719
loop_five_to_n_unsafe.c below 1 OKAY0.461
non_loop_five_to_n.c below 7 FAIL58.251
non_loop_five_to_n_unsafe.c below 7 OKAY57.14
power_log_modified.c below 1 PASS0.934
simple_exponential.c below 1 PASS0.784
simple_exponential_for.c below 1 PASS0.712
simple_exponential_for_unsafe.c below 1 OKAY0.619
simple_exponential_unsafe.c below 1 OKAY0.618
two_to_n_minus_n.c below 7 FAIL2.525
two_to_n_minus_n_loop.c below TIMEOUT 300.008
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.004
two_to_n_minus_n_unsafe.c below 7 OKAY2.585
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 739.933
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.734
02.c below 3 FAIL0.973
03.c below 1 PASS0.577
04.c below 1 PASS0.402
05.c below 3 PASS1.333
06.c below 3 FAIL10.589
07.c below 3 PASS0.707
08.c below 3 PASS1.625
09.c below 3 PASS1.095
10.c below 3 FAIL1.364
11.c below 1 PASS0.407
12.c below 3 PASS1.698
13.c below 3 PASS0.713
14.c below 3 PASS0.587
15.c below 1 PASS0.381
16.c below 1 PASS0.549
17.c below 1 PASS3.634
18.c below 1 PASS0.488
19.c below 1 PASS0.586
20.c below 3 FAIL0.825
21.c below 3 PASS0.69
22.c below 3 FAIL0.902
23.c below 1 PASS0.435
24.c below 1 PASS0.488
25.c below 3 FAIL1.766
26.c below TIMEOUT 300.007
27.c below 1 PASS0.529
28.c below 3 PASS0.722
29.c below 3 PASS1.221
30.c below 1 PASS0.416
31.c below 3 PASS1.345
32.c below 1 FAIL0.44
33.c below 3 PASS1.46
34.c below 1 FAIL0.451
35.c below 1 PASS0.376
36.c below 3 PASS2.977
37.c below 3 FAIL0.673
38.c below 1 FAIL0.457
39.c below 3 PASS0.568
40.c below 3 PASS0.967
41.c below 1 PASS0.45
42.c below 3 PASS1.073
43.c below 3 PASS0.678
44.c below 1 PASS0.424
45.c below 3 FAIL3.075
46.c below 3 FAIL2.111
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 353.968
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.506
AGHKTW2017_foo.c below 1 PASS0.505
AGHKTW2017_loginSafe.c below 1 PASS1.054
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.583
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.581
BCK2011_gauss.c below 1 PASS0.546
BCK2011_strength_reduction.c below 1 PASS0.88
BCK2011_strength_reduction_linear.c below 1 PASS0.562
fibonacci_information_flow.c below 1 PASS0.68
loop_splitting_test_safe.c below 1 PASS0.738
TA2005_fib2.c below 1 PASS0.678
TA2005_fib.c below 1 PASS0.55
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.863
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.836
c3_cleanup_better.c below 3 PASS1.698
c3_cleanup.c below 3 PASS1.813
c3_intermediate.c below 3 PASS1.727
c3_noinv.c below 3 FAIL1.523
doublers.c below 1 FAIL0.692
doublers_easier.c below 3 FAIL1.336
doublers_easy.c below 1 FAIL0.769
exp_mult.c below 1 FAIL0.42
fig1_rotation_unsafe.c below 1 OKAY0.483
guessing_game.c below 3 FAIL0.655
not_P_solvable.c below 1 PASS0.409
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 12.361
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.467
maxequals_linear_1.c below 1 PASS0.656
maxequals_linear_2.c below 1 PASS0.698
maxequals_linear_3.c below 1 FAIL0.418
maxequals_linear_4.c below 1 PASS0.433
maxequals_linear_5.c below 1 PASS0.44
maxequals_linear_6.c below 1 FAIL0.447
maxequals_matrix1.c below 3 FAIL1.764
maxequals_matrix2.c below 3 FAIL1.685
maxequals_quadratic1.c below 1 FAIL0.443
maxequals_quadratic2.c below 1 PASS0.44
maxequals_stratified1.c below 3 PASS5.012
maxequals_stratified2.c below 3 PASS5.526
maxequals_stratified3.c below 3 FAIL5.727
nine.c below 1 FAIL0.528
nine_nondecreasing.c below 1 PASS0.689
sum_interval_1.c below 1 FAIL0.576
sum_interval_2.c below 1 FAIL0.544
sum_interval_3.c below 1 FAIL0.563
TrackingObjectFields.c below 3 PASS12.047
TrackingObjectFields_inlined.c below 1 PASS3.487
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 42.59
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.52
bobble2_varloop.c below 1 PASS0.504
bobble3.c below TIMEOUT 300.004
bobble4.c below 1 FAIL0.471
bobble5.c below 1 FAIL0.49
bobble.c below 1 PASS0.485
inchworm2.c below 1 TIMEOUT300.006
inchworm3.c below 1 PASS0.487
inchworm4.c below 1 PASS0.514
inchworm5.c below 1 PASS0.495
inchworm6_unsafe.c below 1 OKAY0.495
inchworm.c below 1 FAIL0.489
leapdiff2.c below 1 TIMEOUT300.007
leapfrog_annotated.c below 1 FAIL0.473
leapfrog_annotated_disjunction.c below 1 PASS0.524
leapfrog_asymmetric2.c below 1 FAIL0.569
leapfrog_asymmetric3.c below 1 FAIL0.545
leapfrog_asymmetric.c below 1 FAIL0.508
leapfrog.c below 1 FAIL0.431
leapfrog_materialized.c below 1 FAIL0.487
leapfrog_verbose.c below 1 FAIL0.515
leapspin.c below 1 FAIL0.437
leapsum2.c below 1 TIMEOUT300.004
leapthree.c below 1 FAIL0.477
microbobble2.c below 1 PASS0.455
microbobble3.c below 1 PASS0.477
microbobble_asymmetric.c below 1 PASS0.462
microbobble.c below 1 FAIL0.45
simple_bl2.c below 1 FAIL0.489
simple_bl3.c below 1 FAIL0.405
simple_bl.c below 1 FAIL0.487
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1213.162
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.347
binval_example_2_unsafe.c below 1 OKAY0.374
binval_example_3_unsafe.c below 1 OKAY0.344
binval_example_4.c below 1 PASS0.418
binval_example_4_unsafe.c below 1 OKAY0.428
binval_example_5.c below 1 FAIL1.638
binval_example_5_unsafe.c below 1 OKAY3.799
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.348