[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.414
kmp.c below 1 PASS1.333
qsort.c below 4 PASS1.297
speed_pldi09_fig1.c below 1 PASS0.649
speed_pldi09_fig4_2.c below 1 FAIL0.466
speed_pldi09_fig4_4.c below 1 PASS0.601
speed_pldi09_fig4_5.c below 1 PASS0.476
speed_pldi10_ex1.c below 1 PASS1.666
speed_pldi10_ex3.c below 1 PASS0.68
speed_pldi10_ex4.c below 1 PASS0.733
speed_popl10_fig2_1.c below 1 PASS0.647
speed_popl10_fig2_2.c below 1 FAIL0.44
speed_popl10_nested_multiple.c below 1 PASS0.58
speed_popl10_nested_single.c below 1 PASS0.551
speed_popl10_sequential_single.c below 1 PASS0.497
speed_popl10_simple_multiple.c below 1 PASS0.687
speed_popl10_simple_single_2.c below 1 PASS0.899
speed_popl10_simple_single.c below 1 PASS0.41
t07.c below 1 PASS0.57
t08.c below 1 PASS0.47
t09.c below 1 PASS0.464
t10.c below 1 PASS0.432
t11.c below 1 PASS0.654
t13.c below 1 FAIL0.512
t15.c below 1 PASS0.531
t16.c below 1 PASS0.487
t19.c below 1 PASS0.5
t20.c below 1 PASS0.456
t27.c below 1 PASS0.775
t28.c below 1 PASS0.701
t30.c below 1 FAIL0.483
t37.c below 2 PASS0.893
t39.c below 2 PASS0.755
t46.c below 1 PASS0.528
t47.c below 1 PASS0.708
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.945
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.501
qsort_full.c below 4 PASS11.674
rec1-param_safe.c below 2 PASS0.525
rec1-param_unsafe.c below 2 OKAY0.537
rec1_safe.c below 2 PASS0.474
rec1_unsafe.c below 2 OKAY0.488
rec2-param_safe.c below 2 PASS0.491
rec2-param_unsafe.c below 2 OKAY0.482
rec2_safe.c below 2 PASS0.481
rec2_unsafe.c below 2 OKAY0.472
rec-test.c below 2 PASS0.467
sas03_bothbranches.c below 7 PASS1.22
sas03.c below 2 PASS0.89
simulated_lese_recursive.c below 2 PASS0.626
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.328
/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.401
divide.c below 1 PASS0.394
factor_unsafe.c below 1 OKAY0.36
for_infinite_loop_1_safe.c below 1 PASS0.352
for_infinite_loop_2_safe.c below 1 PASS0.357
interproc.c below 1 PASS0.315
mult.c below 1 PASS0.393
pointer_arith.c below 1 PASS0.338
quotient.c below 3 PASS0.698
subtract.c below 1 PASS0.359
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.374
sum01_bug02_unsafe.c below 1 OKAY0.694
sum01_real_safe.c below 1 PASS0.392
sum01_safe.c below 1 PASS0.405
sum01_unsafe.c below 1 OKAY0.597
sum02_safe.c below 1 PASS0.414
sum03_safe.c below 1 PASS0.478
sum03_unsafe.c below 1 OKAY0.586
sum04_safe.c below 1 PASS0.402
sum04_unsafe.c below 1 OKAY0.587
terminator_02_safe.c below 1 PASS0.357
terminator_02_unsafe.c below 1 OKAY0.404
terminator_03_safe.c below 1 PASS0.355
terminator_03_unsafe.c below 1 OKAY0.368
token_ring01_safe.c below 4 FAIL128.156
token_ring01_unsafe.c below 4 OKAY205.096
toy_safe.c below EXCEPTION 129.115
trex01_safe.c below 1 PASS0.794
trex01_unsafe.c below 1 OKAY0.465
trex02_safe2.c below 3 PASS0.558
trex02_safe.c below 3 PASS0.558
trex02_unsafe.c below 3 OKAY0.544
trex03_safe.c below 1 PASS0.504
trex03_unsafe.c below 1 OKAY0.516
trex04_safe.c below 1 PASS0.378
while_infinite_loop_1_safe.c below 1 PASS0.331
while_infinite_loop_2_safe.c below 1 PASS0.333
while_infinite_loop_3_safe.c below 1 PASS0.335
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 478.447
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.522
blogger_simplified1.c below 3 PASS1.659
divided_difference2.c below TIMEOUT 300.007
mult-proc.c below 3 PASS0.525
mult-proc-params.c below 3 PASS0.528
popall.c below 1 PASS0.912
simulated_scc.c below 1 PASS0.829
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 304.982
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.401
degree2_binomial.c below 1 PASS0.889
degree2_monomial.c below 1 PASS0.475
degree3_binomial.c below 1 FAIL4.814
degree3_monomial.c below 1 PASS1.013
degree4_binomial.c below 1 FAIL5.084
degree4_monomial.c below 1 PASS1.645
degree5_binomial.c below 1 FAIL16.13
degree5_monomial.c below 1 PASS3.144
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 33.595
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.517
cubic_with_square_interproc.c below 2 FAIL0.748
cubic_with_square_nonlinear.c below 1 FAIL0.637
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.729
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.673
cubic_with_square_unsafe.c below 1 OKAY0.501
multi-input.c below 1 FAIL10.526
multi-input_unsafe.c below 1 OKAY10.323
nondet_loop_bound.c below 1 FAIL0.567
nondet_loop_bound_quartic.c below 1 FAIL0.76
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.822
nondet_loop_bound_unsafe.c below 1 OKAY0.554
nonlinear_stratified.c below 1 PASS126.899
nonlinear_stratified_unsafe.c below 1 OKAY68.312
quartic_with_cube.c below 1 FAIL0.724
quartic_with_cube_nonlinear.c below 1 FAIL0.992
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.997
quartic_with_cube_unsafe.c below 1 OKAY0.568
quintic_with_quartic.c below 1 PASS1.092
quintic_with_quartic_nonlinear.c below 1 PASS1.128
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.135
quintic_with_quartic_unsafe.c below 1 OKAY1.118
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 230.322
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.997
degree2_FD_AllAux_AllAssm.c below 1 PASS110.309
degree2_FD_AllAux_FewAssm.c below 1 PASS7.018
degree2_FD_FewAux_FewAssm.c below 1 PASS1.333
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.358
degree3.c below 1 PASS1.129
degree3_FD.c below 1 PASS1.255
degree4.c below 1 PASS1.93
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 125.329
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.539
loop_unsafe.c below 1 OKAY0.56
simulated_lese_parser.c below 1 PASS0.407
simulated_lese_sentinel.c below 1 PASS0.394
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.9
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.409
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.409
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.005
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.005
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.394
array_false-unreach-call2.c below 1 OKAY0.402
array_false-unreach-call3.c below 1 OKAY0.386
array_true-unreach-call1.c below 1 FAIL0.371
array_true-unreach-call2.c below 1 FAIL0.417
array_true-unreach-call3.c below 1 PASS0.395
array_true-unreach-call4.c below 1 FAIL0.376
const_false-unreach-call1.c below 1 OKAY0.402
const_true-unreach-call1.c below 1 PASS0.395
diamond_false-unreach-call1.c below 1 OKAY0.394
diamond_true-unreach-call1.c below 1 PASS0.402
diamond_true-unreach-call2.c below 1 PASS0.42
functions_false-unreach-call1.c below 3 OKAY0.562
functions_true-unreach-call1.c below 3 PASS0.497
multivar_false-unreach-call1.c below 1 OKAY0.452
multivar_true-unreach-call1.c below 1 PASS0.399
nested_false-unreach-call1.c below 1 OKAY0.47
nested_true-unreach-call1.c below 1 PASS0.463
overflow_true-unreach-call1.c below 1 PASS0.353
phases_false-unreach-call1.c below 1 OKAY0.507
phases_false-unreach-call2.c below 1 OKAY0.379
phases_true-unreach-call1.c below 1 PASS0.5
phases_true-unreach-call2.c below 1 PASS0.372
simple_false-unreach-call1.c below 1 OKAY0.377
simple_false-unreach-call2.c below 1 OKAY0.348
simple_false-unreach-call3.c below 1 OKAY0.366
simple_false-unreach-call4.c below 1 OKAY0.368
simple_true-unreach-call1.c below 1 PASS0.36
simple_true-unreach-call2.c below 1 PASS0.355
simple_true-unreach-call3.c below 1 PASS0.351
simple_true-unreach-call4.c below 1 PASS0.368
underapprox_false-unreach-call1.c below 1 OKAY0.399
underapprox_false-unreach-call2.c below 1 OKAY0.404
underapprox_true-unreach-call1.c below 1 FAIL0.417
underapprox_true-unreach-call2.c below 1 PASS0.393
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.214
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.588
apache-get-tag_true-unreach-call.c below 1 FAIL0.614
down_true-unreach-call.c below 1 PASS0.465
fragtest_simple_true-unreach-call.c below 1 PASS0.574
half_2_true-unreach-call.c below 1 PASS0.492
heapsort_true-unreach-call.c below 1 PASS2.219
id_build_true-unreach-call.c below 1 PASS0.457
id_trans_false-unreach-call.c below 1 OKAY0.367
id_trans_true-unreach-call.c below 1 PASS0.393
large_const_true-unreach-call.c below 1 PASS0.532
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.438
nested6_true-unreach-call.c below 1 FAIL0.626
nested9_true-unreach-call.c below 1 PASS0.696
nest-if3_true-unreach-call.c below 1 PASS0.543
NetBSD_loop_true-unreach-call.c below 1 PASS0.394
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.503
seq_true-unreach-call.c below 1 PASS0.537
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.626
string_concat-noarr_true-unreach-call.c below 1 PASS0.507
up_true-unreach-call.c below 1 PASS0.471
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.042
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.43
bhmr2007_true-unreach-call.c below 1 PASS0.458
cggmp2005b_true-unreach-call.c below 1 PASS0.639
cggmp2005_true-unreach-call.c below 1 PASS0.397
cggmp2005_variant_true-unreach-call.c below 1 PASS0.423
css2003_true-unreach-call.c below 1 PASS1.135
ddlm2013_true-unreach-call.c below 1 PASS0.606
gcnr2008_false-unreach-call.c below 1 OKAY1.116
gj2007b_true-unreach-call.c below 1 FAIL0.444
gj2007_true-unreach-call.c below 1 PASS0.577
gr2006_true-unreach-call.c below 1 PASS0.589
gsv2008_true-unreach-call.c below 1 PASS0.395
hhk2008_true-unreach-call.c below 1 PASS0.38
jm2006_true-unreach-call.c below 1 PASS0.525
jm2006_variant_true-unreach-call.c below 1 PASS0.601
mcmillan2006_true-unreach-call.c below 1 FAIL0.456
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.171
/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.489
count_by_2_true-unreach-call.c below 1 PASS0.374
count_by_k_true-unreach-call.c below 1 PASS0.369
count_by_nondet_true-unreach-call.c below 1 PASS0.41
gauss_sum_true-unreach-call.c below 1 PASS0.413
half_true-unreach-call.c below 1 FAIL0.432
nested_true-unreach-call.c below 1 PASS0.526
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.383
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.427
array_true-unreach-call.c below 1 FAIL0.437
bubble_sort_false-unreach-call.c below 4 OKAY77.871
bubble_sort_true-unreach-call.c below 1 PASS5.252
compact_false-unreach-call.c below 1 OKAY0.456
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.432
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.4
eureka_01_false-unreach-call.c below 1 OKAY2.646
eureka_01_true-unreach-call.c below 1 FAIL1.611
eureka_05_true-unreach-call.c below 1 FAIL0.877
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.388
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.399
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.356
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.353
heavy_false-unreach-call.c below 1 OKAY0.603
heavy_true-unreach-call.c below 1 PASS0.584
insertion_sort_false-unreach-call.c below 1 OKAY1.488
insertion_sort_true-unreach-call.c below 1 FAIL0.621
invert_string_false-unreach-call.c below 1 OKAY0.603
invert_string_true-unreach-call.c below 1 FAIL0.632
linear_sea.ch_true-unreach-call.c below 1 FAIL0.42
linear_search_false-unreach-call.c below 1 OKAY0.434
lu.cmp_true-unreach-call.c below 3 PASS27.577
ludcmp_false-unreach-call.c below 3 OKAY27.605
matrix_false-unreach-call_true-termination.c below 1 OKAY1.33
matrix_true-unreach-call_true-termination.c below 1 FAIL0.505
n.c11_true-unreach-call.c below 3 FAIL0.569
n.c24_false-unreach-call.c below 3 OKAY5.362
n.c40_true-unreach-call.c below 1 FAIL0.399
nec11_false-unreach-call.c below 1 OKAY0.405
nec20_false-unreach-call.c below 1 OKAY0.456
nec40_true-unreach-call.c below 1 FAIL0.415
string_false-unreach-call.c below 1 OKAY0.752
string_true-unreach-call.c below 1 FAIL0.738
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.716
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.383
sum01_false-unreach-call_true-termination.c below 1 OKAY0.581
sum01_true-unreach-call_true-termination.c below 1 PASS0.407
sum03_false-unreach-call_true-termination.c below 1 OKAY0.651
sum03_true-unreach-call_false-termination.c below 1 PASS0.527
sum04_false-unreach-call_true-termination.c below 1 OKAY0.588
sum04_true-unreach-call_true-termination.c below 1 PASS0.417
sum_array_false-unreach-call.c below 1 OKAY0.662
sum_array_true-unreach-call.c below 1 FAIL0.698
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.353
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.62
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.43
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.35
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.378
trex01_false-unreach-call_true-termination.c below 3 OKAY0.605
trex01_true-unreach-call.c below 3 PASS0.886
trex02_false-unreach-call_true-termination.c below 3 OKAY0.565
trex02_true-unreach-call_true-termination.c below 3 PASS0.551
trex03_false-unreach-call_true-termination.c below 3 OKAY0.88
trex03_true-unreach-call.c below 3 PASS0.88
trex04_true-unreach-call_false-termination.c below 1 PASS0.417
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.402
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.334
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.43
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.422
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.175
vogal_false-unreach-call.c below 1 OKAY0.934
vogal_true-unreach-call.c below 1 FAIL0.941
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.338
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.341
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.343
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.332
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 195.94
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.569
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.554
Ackermann03_true-unreach-call.c below 7 FAIL1.598
Ackermann04_true-unreach-call.c below 7 FAIL1.594
Addition01_true-unreach-call_true-termination.c below 2 PASS0.786
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.816
Addition03_false-no-overflow.c below 2 PASS0.839
Addition03_true-unreach-call.c below 2 PASS0.818
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.61
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.545
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.552
Fibonacci01_true-unreach-call.c below TIMEOUT 300.004
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.006
gcd01_true-unreach-call_true-termination.c below 2 PASS0.703
gcd02_true-unreach-call.c below 2 FAIL1.401
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.223
McCarthy91_true-unreach-call.c below 7 FAIL1.235
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.747
Primes_true-unreach-call.c below 3 FAIL2.222
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.543
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.513
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.515
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.407
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.577
afterrec_2calls_true-unreach-call.c below 2 PASS0.567
afterrec_false-unreach-call.c below 2 OKAY0.47
afterrec_true-unreach-call.c below 2 PASS0.472
fibo_10_false-unreach-call.c below TIMEOUT 300.004
fibo_10_true-unreach-call.c below TIMEOUT 300.005
fibo_15_false-unreach-call.c below TIMEOUT 300.006
fibo_15_true-unreach-call.c below TIMEOUT 300.004
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.005
fibo_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.005
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.006
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.004
fibo_5_false-unreach-call.c below TIMEOUT 300.005
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.005
id2_b2_o3_true-unreach-call.c below 2 PASS0.947
id2_b3_o2_false-unreach-call.c below 2 OKAY0.988
id2_b3_o5_true-unreach-call.c below 2 PASS0.946
id2_b5_o10_true-unreach-call.c below 2 PASS0.959
id2_i5_o5_false-unreach-call.c below 2 OKAY0.558
id2_i5_o5_true-unreach-call.c below 2 PASS0.603
id_b2_o3_true-unreach-call.c below 2 PASS0.85
id_b3_o2_false-unreach-call.c below 2 OKAY0.866
id_b3_o5_true-unreach-call.c below 2 PASS0.861
id_b5_o10_true-unreach-call.c below 2 PASS0.848
id_i10_o10_false-unreach-call.c below 2 OKAY0.517
id_i10_o10_true-unreach-call.c below 2 PASS0.526
id_i15_o15_false-unreach-call.c below 2 OKAY0.52
id_i15_o15_true-unreach-call.c below 2 PASS0.506
id_i20_o20_false-unreach-call.c below 2 OKAY0.529
id_i20_o20_true-unreach-call.c below 2 PASS0.529
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.536
id_i5_o5_true-unreach-call.c below 2 PASS0.518
id_o1000_false-unreach-call.c below 2 OKAY0.515
id_o100_false-unreach-call.c below 2 OKAY0.523
id_o10_false-unreach-call.c below 2 OKAY0.526
id_o200_false-unreach-call.c below 2 OKAY0.531
id_o20_false-unreach-call.c below 2 OKAY0.514
id_o3_false-unreach-call.c below 2 OKAY0.521
sum_10x0_false-unreach-call.c below 2 OKAY0.566
sum_10x0_true-unreach-call.c below 2 PASS0.586
sum_15x0_false-unreach-call.c below 2 OKAY0.585
sum_15x0_true-unreach-call.c below 2 PASS0.567
sum_20x0_false-unreach-call.c below 2 OKAY0.583
sum_20x0_true-unreach-call.c below 2 PASS0.578
sum_25x0_false-unreach-call.c below 2 OKAY0.595
sum_25x0_true-unreach-call.c below 2 PASS0.569
sum_2x3_false-unreach-call.c below 2 OKAY0.602
sum_2x3_true-unreach-call.c below 2 PASS0.576
sum_non_eq_false-unreach-call.c below 2 OKAY0.588
sum_non_eq_true-unreach-call.c below 2 PASS0.584
sum_non_false-unreach-call.c below 2 OKAY0.574
sum_non_true-unreach-call.c below 2 PASS0.593
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9027.139
/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.586
rec-bhmr2007_true-unreach-call.c below 2 PASS0.571
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.096
rec-cggmp2005_true-unreach-call.c below 2 PASS0.507
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.554
rec-css2003_true-unreach-call.c below 2 PASS1.492
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.125
rec-gj2007b_true-unreach-call.c below 2 FAIL0.517
rec-gj2007_true-unreach-call.c below 2 FAIL0.691
rec-gr2006_true-unreach-call.c below 2 FAIL0.669
rec-gsv2008_true-unreach-call.c below 2 PASS0.544
rec-hhk2008_true-unreach-call.c below 2 PASS0.528
rec-jm2006_true-unreach-call.c below 2 PASS0.673
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.761
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.637
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.955
/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.486
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.551
rec-count_by_2_true-unreach-call.c below 2 PASS0.477
rec-count_by_k_true-unreach-call.c below 2 PASS0.516
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.52
rec-gauss_sum_true-unreach-call.c below 2 PASS0.554
rec-half_true-unreach-call.c below 2 FAIL0.542
rec-nested_true-unreach-call.c below 3 FAIL0.849
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.495
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.636
cubic_polynomial_unsafe.c below 2 OKAY0.657
edit_distance_bottom_up.c below 3 FAIL204.8
edit_distance_top_down.c below 3 FAIL5.481
log_log_n_solution.c below 3 FAIL0.631
log_log_n_solution_unsafe.c below 3 OKAY0.636
log_n_solution.c below 2 FAIL0.618
log_n_solution_unsafe.c below 2 OKAY0.614
multivariate_1.c below TIMEOUT 300.098
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL3.617
multivariate_higher_order_unsafe.c below 7 OKAY3.555
n_cubed_solution.c below EXCEPTION 102.847
n_cubed_solution_unsafe.c below EXCEPTION 0.027
n_log_n_solution.c below 8 FAIL1.713
n_log_n_solution_unsafe.c below 8 OKAY1.707
n_squared_two_base_case_even.c below 2 PASS0.714
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.676
n_squared_two_base_case_odd.c below 2 PASS0.685
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.711
pascals_dynamic.c below 3 FAIL2.656
pascals_dynamic_unsafe.c below 3 OKAY2.682
pascals_iterative.c below 1 FAIL4.948
pascals_iterative_unsafe.c below 1 OKAY4.963
pascals_recursive.c below 8 FAIL3.753
pascals_recursive_unsafe.c below 8 OKAY3.809
squared_solution.c below 8 FAIL3.275
squared_solution_unsafe.c below 8 OKAY3.166
two_n_even.c below 2 PASS0.535
two_n_even_unsafe.c below 2 OKAY0.544
two_n_odd.c below 2 PASS0.554
two_n_odd_unsafe.c below 2 OKAY0.538
two_to_n_over_two_even.c below 7 FAIL292.626
two_to_n_over_two_even_unsafe.c below 7 OKAY286.954
two_to_n_over_two_odd.c below 7 FAIL246.325
two_to_n_over_two_odd_unsafe.c below 7 OKAY116.291
two_to_n_squared.c below 5 FAIL20.317
two_to_n_squared_unsafe.c below 5 OKAY20.427
two_to_two_to_n.c below 7 FAIL1.475
two_to_two_to_n_unsafe.c below 7 OKAY1.471
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1947.737
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.415
adding_and_mult_unsafe.c below 1 OKAY0.419
binary_search_array_tree.c below 1 FAIL0.791
exp_add_linear.c below 1 PASS0.501
exp_add_linear_unsafe.c below 1 OKAY0.522
exp_add_loop_rec.c below 1 FAIL0.418
exp_add_loop_rec_unsafe.c below 1 OKAY0.409
exp_add_loop_variable.c below 1 PASS0.501
exp_add_loop_variable_unsafe.c below 1 OKAY0.521
exp_with_linear_inner_loop.c below 1 FAIL0.624
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.627
halving_log1.c below 1 FAIL0.677
linear_two_to_n.c below 7 FAIL1.748
linear_two_to_n_unsafe.c below 7 OKAY1.759
loop_five_to_n.c below 1 PASS0.474
loop_five_to_n_unsafe.c below 1 OKAY0.491
non_loop_five_to_n.c below 7 FAIL54.342
non_loop_five_to_n_unsafe.c below 7 OKAY55.026
power_log_modified.c below 1 PASS0.666
simple_exponential.c below 1 PASS0.471
simple_exponential_for.c below 1 PASS0.475
simple_exponential_for_unsafe.c below 1 OKAY0.473
simple_exponential_unsafe.c below 1 OKAY0.464
two_to_n_minus_n.c below 7 FAIL2.366
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.406
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 727.597
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.713
02.c below 3 FAIL0.913
03.c below 1 PASS0.53
04.c below 1 PASS0.391
05.c below 3 PASS1.292
06.c below 3 FAIL10.45
07.c below 3 PASS0.716
08.c below 3 PASS1.606
09.c below 3 PASS1.114
10.c below 3 FAIL1.351
11.c below 1 PASS0.419
12.c below 3 PASS1.632
13.c below 3 PASS0.702
14.c below 3 PASS0.618
15.c below 1 PASS0.409
16.c below 1 PASS0.559
17.c below 1 PASS3.757
18.c below 1 PASS0.508
19.c below 1 PASS0.568
20.c below 3 FAIL0.813
21.c below 3 PASS0.682
22.c below 3 FAIL0.942
23.c below 1 PASS0.418
24.c below 1 PASS0.519
25.c below 3 FAIL1.751
26.c below TIMEOUT 300.005
27.c below 1 PASS0.567
28.c below 3 PASS0.722
29.c below 3 PASS1.194
30.c below 1 PASS0.425
31.c below 3 PASS1.389
32.c below 1 FAIL0.442
33.c below 3 PASS1.425
34.c below 1 FAIL0.449
35.c below 1 PASS0.378
36.c below 3 PASS2.922
37.c below 3 FAIL0.66
38.c below 1 FAIL0.447
39.c below 3 PASS0.544
40.c below 3 PASS0.962
41.c below 1 PASS0.437
42.c below 3 PASS1.005
43.c below 3 PASS0.681
44.c below 1 PASS0.399
45.c below 3 FAIL3.001
46.c below 3 FAIL2.074
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 353.501
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.504
AGHKTW2017_foo.c below 1 PASS0.478
AGHKTW2017_loginSafe.c below 1 PASS1.015
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.571
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.574
BCK2011_gauss.c below 1 PASS0.545
BCK2011_strength_reduction.c below 1 PASS0.847
BCK2011_strength_reduction_linear.c below 1 PASS0.552
fibonacci_information_flow.c below 1 PASS0.675
loop_splitting_test_safe.c below 1 PASS0.706
TA2005_fib2.c below 1 PASS0.691
TA2005_fib.c below 1 PASS0.558
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.716
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.854
c3_cleanup_better.c below 3 PASS1.724
c3_cleanup.c below 3 PASS1.782
c3_intermediate.c below 3 PASS1.717
c3_noinv.c below 3 FAIL1.432
doublers.c below 1 FAIL0.664
doublers_easier.c below 3 FAIL1.31
doublers_easy.c below 1 FAIL0.717
exp_mult.c below 1 FAIL0.414
fig1_rotation_unsafe.c below 1 OKAY0.473
guessing_game.c below 3 FAIL0.635
not_P_solvable.c below 1 PASS0.398
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 12.12
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.454
maxequals_linear_1.c below 1 PASS0.667
maxequals_linear_2.c below 1 PASS0.664
maxequals_linear_3.c below 1 FAIL0.438
maxequals_linear_4.c below 1 PASS0.429
maxequals_linear_5.c below 1 PASS0.457
maxequals_linear_6.c below 1 FAIL0.455
maxequals_matrix1.c below 3 FAIL1.691
maxequals_matrix2.c below 3 FAIL1.593
maxequals_quadratic1.c below 1 FAIL0.418
maxequals_quadratic2.c below 1 PASS0.43
maxequals_stratified1.c below 3 PASS5.119
maxequals_stratified2.c below 3 PASS5.404
maxequals_stratified3.c below 3 FAIL5.775
nine.c below 1 FAIL0.442
nine_nondecreasing.c below 1 PASS0.693
sum_interval_1.c below 1 FAIL0.522
sum_interval_2.c below 1 FAIL0.494
sum_interval_3.c below 1 FAIL0.502
TrackingObjectFields.c below 3 PASS11.273
TrackingObjectFields_inlined.c below 1 PASS3.25
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 41.17
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.496
bobble2_varloop.c below 1 PASS0.496
bobble3.c below TIMEOUT 300.005
bobble4.c below 1 FAIL0.499
bobble5.c below 1 FAIL0.496
bobble.c below 1 PASS0.479
inchworm2.c below 1 TIMEOUT300.005
inchworm3.c below 1 PASS0.543
inchworm4.c below 1 PASS0.536
inchworm5.c below 1 PASS0.538
inchworm6_unsafe.c below 1 OKAY0.469
inchworm.c below 1 FAIL0.483
leapdiff2.c below 1 TIMEOUT300.007
leapfrog_annotated.c below 1 FAIL0.457
leapfrog_annotated_disjunction.c below 1 PASS0.479
leapfrog_asymmetric2.c below 1 FAIL0.55
leapfrog_asymmetric3.c below 1 FAIL0.58
leapfrog_asymmetric.c below 1 FAIL0.486
leapfrog.c below 1 FAIL0.444
leapfrog_materialized.c below 1 FAIL0.498
leapfrog_verbose.c below 1 FAIL0.481
leapspin.c below 1 FAIL0.425
leapsum2.c below 1 TIMEOUT300.004
leapthree.c below 1 FAIL0.497
microbobble2.c below 1 PASS0.447
microbobble3.c below 1 PASS0.438
microbobble_asymmetric.c below 1 PASS0.453
microbobble.c below 1 FAIL0.435
simple_bl2.c below 1 FAIL0.486
simple_bl3.c below 1 FAIL0.392
simple_bl.c below 1 FAIL0.505
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1213.109
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.357
binval_example_2_unsafe.c below 1 OKAY0.357
binval_example_3_unsafe.c below 1 OKAY0.361
binval_example_4.c below 1 PASS0.427
binval_example_4_unsafe.c below 1 OKAY0.422
binval_example_5.c below 1 FAIL1.611
binval_example_5_unsafe.c below 1 OKAY3.749
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.284