[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.417
kmp.c below 1 PASS1.307
qsort.c below 4 PASS1.283
speed_pldi09_fig1.c below 1 PASS0.68
speed_pldi09_fig4_2.c below 1 FAIL0.468
speed_pldi09_fig4_4.c below 1 PASS0.606
speed_pldi09_fig4_5.c below 1 PASS0.504
speed_pldi10_ex1.c below 1 PASS1.74
speed_pldi10_ex3.c below 1 PASS0.705
speed_pldi10_ex4.c below 1 PASS0.704
speed_popl10_fig2_1.c below 1 PASS0.616
speed_popl10_fig2_2.c below 1 FAIL0.439
speed_popl10_nested_multiple.c below 1 PASS0.578
speed_popl10_nested_single.c below 1 PASS0.543
speed_popl10_sequential_single.c below 1 PASS0.489
speed_popl10_simple_multiple.c below 1 PASS0.735
speed_popl10_simple_single_2.c below 1 PASS0.904
speed_popl10_simple_single.c below 1 PASS0.404
t07.c below 1 PASS0.556
t08.c below 1 PASS0.484
t09.c below 1 PASS0.456
t10.c below 1 PASS0.414
t11.c below 1 PASS0.64
t13.c below 1 FAIL0.515
t15.c below 1 PASS0.51
t16.c below 1 PASS0.489
t19.c below 1 PASS0.501
t20.c below 1 PASS0.461
t27.c below 1 PASS0.759
t28.c below 1 PASS0.72
t30.c below 1 FAIL0.461
t37.c below 2 PASS0.897
t39.c below 2 PASS0.765
t46.c below 1 PASS0.526
t47.c below 1 PASS0.669
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.502
qsort_full.c below 4 PASS11.848
rec1-param_safe.c below 2 PASS0.511
rec1-param_unsafe.c below 2 OKAY0.521
rec1_safe.c below 2 PASS0.484
rec1_unsafe.c below 2 OKAY0.473
rec2-param_safe.c below 2 PASS0.488
rec2-param_unsafe.c below 2 OKAY0.481
rec2_safe.c below 2 PASS0.498
rec2_unsafe.c below 2 OKAY0.461
rec-test.c below 2 PASS0.473
sas03_bothbranches.c below 7 PASS1.211
sas03.c below 2 PASS0.914
simulated_lese_recursive.c below 2 PASS0.614
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.479
/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.41
divide.c below 1 PASS0.406
factor_unsafe.c below 1 OKAY0.373
for_infinite_loop_1_safe.c below 1 PASS0.357
for_infinite_loop_2_safe.c below 1 PASS0.382
interproc.c below 1 PASS0.336
mult.c below 1 PASS0.376
pointer_arith.c below 1 PASS0.334
quotient.c below 3 PASS0.72
subtract.c below 1 PASS0.373
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.384
sum01_bug02_unsafe.c below 1 OKAY0.716
sum01_real_safe.c below 1 PASS0.389
sum01_safe.c below 1 PASS0.394
sum01_unsafe.c below 1 OKAY0.594
sum02_safe.c below 1 PASS0.411
sum03_safe.c below 1 PASS0.489
sum03_unsafe.c below 1 OKAY0.565
sum04_safe.c below 1 PASS0.417
sum04_unsafe.c below 1 OKAY0.573
terminator_02_safe.c below 1 PASS0.343
terminator_02_unsafe.c below 1 OKAY0.41
terminator_03_safe.c below 1 PASS0.353
terminator_03_unsafe.c below 1 OKAY0.368
token_ring01_safe.c below 4 FAIL126.393
token_ring01_unsafe.c below 4 OKAY202.199
toy_safe.c below EXCEPTION 126.436
trex01_safe.c below 1 PASS0.799
trex01_unsafe.c below 1 OKAY0.457
trex02_safe2.c below 3 PASS0.538
trex02_safe.c below 3 PASS0.558
trex02_unsafe.c below 3 OKAY0.55
trex03_safe.c below 1 PASS0.507
trex03_unsafe.c below 1 OKAY0.477
trex04_safe.c below 1 PASS0.4
while_infinite_loop_1_safe.c below 1 PASS0.334
while_infinite_loop_2_safe.c below 1 PASS0.33
while_infinite_loop_3_safe.c below 1 PASS0.338
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 471.182
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.562
blogger_simplified1.c below 3 PASS1.635
divided_difference2.c below TIMEOUT 300.009
mult-proc.c below 3 PASS0.536
mult-proc-params.c below 3 PASS0.552
popall.c below 1 PASS0.954
simulated_scc.c below 1 PASS0.839
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.087
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.417
degree2_binomial.c below 1 PASS0.921
degree2_monomial.c below 1 PASS0.514
degree3_binomial.c below 1 FAIL4.857
degree3_monomial.c below 1 PASS1.006
degree4_binomial.c below 1 FAIL5.076
degree4_monomial.c below 1 PASS1.622
degree5_binomial.c below 1 FAIL16.522
degree5_monomial.c below 1 PASS3.146
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 34.081
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.513
cubic_with_square_interproc.c below 2 FAIL0.722
cubic_with_square_nonlinear.c below 1 FAIL0.649
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.695
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.656
cubic_with_square_unsafe.c below 1 OKAY0.52
multi-input.c below 1 FAIL10.638
multi-input_unsafe.c below 1 OKAY10.531
nondet_loop_bound.c below 1 FAIL0.595
nondet_loop_bound_quartic.c below 1 FAIL0.756
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.798
nondet_loop_bound_unsafe.c below 1 OKAY0.55
nonlinear_stratified.c below 1 PASS122.73
nonlinear_stratified_unsafe.c below 1 OKAY71.206
quartic_with_cube.c below 1 FAIL0.69
quartic_with_cube_nonlinear.c below 1 FAIL1.003
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY1.025
quartic_with_cube_unsafe.c below 1 OKAY0.566
quintic_with_quartic.c below 1 PASS1.115
quintic_with_quartic_nonlinear.c below 1 PASS1.186
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.114
quintic_with_quartic_unsafe.c below 1 OKAY1.145
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 229.403
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.026
degree2_FD_AllAux_AllAssm.c below 1 PASS106.948
degree2_FD_AllAux_FewAssm.c below 1 PASS7.014
degree2_FD_FewAux_FewAssm.c below 1 PASS1.346
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.366
degree3.c below 1 PASS1.162
degree3_FD.c below 1 PASS1.277
degree4.c below 1 PASS1.899
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 122.038
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.526
loop_unsafe.c below 1 OKAY0.546
simulated_lese_parser.c below 1 PASS0.397
simulated_lese_sentinel.c below 1 PASS0.402
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.871
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.423
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.423
/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.384
array_false-unreach-call2.c below 1 OKAY0.402
array_false-unreach-call3.c below 1 OKAY0.387
array_true-unreach-call1.c below 1 FAIL0.399
array_true-unreach-call2.c below 1 FAIL0.383
array_true-unreach-call3.c below 1 PASS0.389
array_true-unreach-call4.c below 1 FAIL0.388
const_false-unreach-call1.c below 1 OKAY0.397
const_true-unreach-call1.c below 1 PASS0.402
diamond_false-unreach-call1.c below 1 OKAY0.4
diamond_true-unreach-call1.c below 1 PASS0.395
diamond_true-unreach-call2.c below 1 PASS0.435
functions_false-unreach-call1.c below 3 OKAY0.526
functions_true-unreach-call1.c below 3 PASS0.514
multivar_false-unreach-call1.c below 1 OKAY0.399
multivar_true-unreach-call1.c below 1 PASS0.401
nested_false-unreach-call1.c below 1 OKAY0.453
nested_true-unreach-call1.c below 1 PASS0.442
overflow_true-unreach-call1.c below 1 PASS0.358
phases_false-unreach-call1.c below 1 OKAY0.487
phases_false-unreach-call2.c below 1 OKAY0.375
phases_true-unreach-call1.c below 1 PASS0.496
phases_true-unreach-call2.c below 1 PASS0.381
simple_false-unreach-call1.c below 1 OKAY0.369
simple_false-unreach-call2.c below 1 OKAY0.348
simple_false-unreach-call3.c below 1 OKAY0.354
simple_false-unreach-call4.c below 1 OKAY0.364
simple_true-unreach-call1.c below 1 PASS0.354
simple_true-unreach-call2.c below 1 PASS0.351
simple_true-unreach-call3.c below 1 PASS0.345
simple_true-unreach-call4.c below 1 PASS0.357
underapprox_false-unreach-call1.c below 1 OKAY0.425
underapprox_false-unreach-call2.c below 1 OKAY0.395
underapprox_true-unreach-call1.c below 1 FAIL0.4
underapprox_true-unreach-call2.c below 1 PASS0.399
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.054
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.521
apache-get-tag_true-unreach-call.c below 1 FAIL0.588
down_true-unreach-call.c below 1 PASS0.459
fragtest_simple_true-unreach-call.c below 1 PASS0.574
half_2_true-unreach-call.c below 1 PASS0.468
heapsort_true-unreach-call.c below 1 PASS2.194
id_build_true-unreach-call.c below 1 PASS0.429
id_trans_false-unreach-call.c below 1 OKAY0.374
id_trans_true-unreach-call.c below 1 PASS0.39
large_const_true-unreach-call.c below 1 PASS0.524
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.456
nested6_true-unreach-call.c below 1 FAIL0.661
nested9_true-unreach-call.c below 1 PASS0.715
nest-if3_true-unreach-call.c below 1 PASS0.542
NetBSD_loop_true-unreach-call.c below 1 PASS0.385
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.477
seq_true-unreach-call.c below 1 PASS0.555
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.598
string_concat-noarr_true-unreach-call.c below 1 PASS0.492
up_true-unreach-call.c below 1 PASS0.461
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 13.863
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.445
bhmr2007_true-unreach-call.c below 1 PASS0.457
cggmp2005b_true-unreach-call.c below 1 PASS0.661
cggmp2005_true-unreach-call.c below 1 PASS0.406
cggmp2005_variant_true-unreach-call.c below 1 PASS0.415
css2003_true-unreach-call.c below 1 PASS1.093
ddlm2013_true-unreach-call.c below 1 PASS0.599
gcnr2008_false-unreach-call.c below 1 OKAY1.117
gj2007b_true-unreach-call.c below 1 FAIL0.436
gj2007_true-unreach-call.c below 1 PASS0.58
gr2006_true-unreach-call.c below 1 PASS0.564
gsv2008_true-unreach-call.c below 1 PASS0.403
hhk2008_true-unreach-call.c below 1 PASS0.405
jm2006_true-unreach-call.c below 1 PASS0.552
jm2006_variant_true-unreach-call.c below 1 PASS0.625
mcmillan2006_true-unreach-call.c below 1 FAIL0.473
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.231
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.361
count_by_1_variant_true-unreach-call.c below 1 PASS0.479
count_by_2_true-unreach-call.c below 1 PASS0.373
count_by_k_true-unreach-call.c below 1 PASS0.368
count_by_nondet_true-unreach-call.c below 1 PASS0.389
gauss_sum_true-unreach-call.c below 1 PASS0.421
half_true-unreach-call.c below 1 FAIL0.394
nested_true-unreach-call.c below 1 PASS0.529
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.314
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.439
array_true-unreach-call.c below 1 FAIL0.426
bubble_sort_false-unreach-call.c below 4 OKAY79.247
bubble_sort_true-unreach-call.c below 1 PASS5.357
compact_false-unreach-call.c below 1 OKAY0.455
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.376
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.395
eureka_01_false-unreach-call.c below 1 OKAY2.683
eureka_01_true-unreach-call.c below 1 FAIL1.623
eureka_05_true-unreach-call.c below 1 FAIL0.87
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.38
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.382
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.348
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.343
heavy_false-unreach-call.c below 1 OKAY0.616
heavy_true-unreach-call.c below 1 PASS0.593
insertion_sort_false-unreach-call.c below 1 OKAY1.558
insertion_sort_true-unreach-call.c below 1 FAIL0.653
invert_string_false-unreach-call.c below 1 OKAY0.591
invert_string_true-unreach-call.c below 1 FAIL0.642
linear_sea.ch_true-unreach-call.c below 1 FAIL0.395
linear_search_false-unreach-call.c below 1 OKAY0.436
lu.cmp_true-unreach-call.c below 3 PASS27.654
ludcmp_false-unreach-call.c below 3 OKAY27.987
matrix_false-unreach-call_true-termination.c below 1 OKAY1.36
matrix_true-unreach-call_true-termination.c below 1 FAIL0.528
n.c11_true-unreach-call.c below 3 FAIL0.58
n.c24_false-unreach-call.c below 3 OKAY5.245
n.c40_true-unreach-call.c below 1 FAIL0.392
nec11_false-unreach-call.c below 1 OKAY0.401
nec20_false-unreach-call.c below 1 OKAY0.421
nec40_true-unreach-call.c below 1 FAIL0.408
string_false-unreach-call.c below 1 OKAY0.75
string_true-unreach-call.c below 1 FAIL0.74
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.73
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.382
sum01_false-unreach-call_true-termination.c below 1 OKAY0.588
sum01_true-unreach-call_true-termination.c below 1 PASS0.422
sum03_false-unreach-call_true-termination.c below 1 OKAY0.617
sum03_true-unreach-call_false-termination.c below 1 PASS0.504
sum04_false-unreach-call_true-termination.c below 1 OKAY0.592
sum04_true-unreach-call_true-termination.c below 1 PASS0.404
sum_array_false-unreach-call.c below 1 OKAY0.679
sum_array_true-unreach-call.c below 1 FAIL0.685
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.358
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.618
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.449
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.378
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.357
trex01_false-unreach-call_true-termination.c below 3 OKAY0.631
trex01_true-unreach-call.c below 3 PASS0.914
trex02_false-unreach-call_true-termination.c below 3 OKAY0.551
trex02_true-unreach-call_true-termination.c below 3 PASS0.549
trex03_false-unreach-call_true-termination.c below 3 OKAY0.844
trex03_true-unreach-call.c below 3 PASS0.851
trex04_true-unreach-call_false-termination.c below 1 PASS0.441
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.383
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.892
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.419
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.403
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.657
vogal_false-unreach-call.c below 1 OKAY0.971
vogal_true-unreach-call.c below 1 FAIL1.056
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.333
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.323
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.332
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.342
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 198.929
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.595
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.569
Ackermann03_true-unreach-call.c below 7 FAIL1.612
Ackermann04_true-unreach-call.c below 7 FAIL1.608
Addition01_true-unreach-call_true-termination.c below 2 PASS0.808
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.796
Addition03_false-no-overflow.c below 2 PASS0.989
Addition03_true-unreach-call.c below 2 PASS1.192
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.715
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.686
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.863
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.004
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.006
gcd01_true-unreach-call_true-termination.c below 2 PASS0.732
gcd02_true-unreach-call.c below 2 FAIL1.407
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.262
McCarthy91_true-unreach-call.c below 7 FAIL1.248
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.762
Primes_true-unreach-call.c below 3 FAIL2.287
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.451
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.51
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.504
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1524.62
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.582
afterrec_2calls_true-unreach-call.c below 2 PASS0.56
afterrec_false-unreach-call.c below 2 OKAY0.465
afterrec_true-unreach-call.c below 2 PASS0.461
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.005
fibo_20_false-unreach-call.c below TIMEOUT 300.005
fibo_20_true-unreach-call.c below TIMEOUT 300.006
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.016
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.007
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.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.004
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.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.005
fibo_5_true-unreach-call.c below TIMEOUT 300.005
fibo_7_false-unreach-call.c below TIMEOUT 300.005
fibo_7_true-unreach-call.c below TIMEOUT 300.004
id2_b2_o3_true-unreach-call.c below 2 PASS0.953
id2_b3_o2_false-unreach-call.c below 2 OKAY0.98
id2_b3_o5_true-unreach-call.c below 2 PASS0.959
id2_b5_o10_true-unreach-call.c below 2 PASS0.952
id2_i5_o5_false-unreach-call.c below 2 OKAY0.575
id2_i5_o5_true-unreach-call.c below 2 PASS0.529
id_b2_o3_true-unreach-call.c below 2 PASS0.823
id_b3_o2_false-unreach-call.c below 2 OKAY0.823
id_b3_o5_true-unreach-call.c below 2 PASS0.852
id_b5_o10_true-unreach-call.c below 2 PASS0.828
id_i10_o10_false-unreach-call.c below 2 OKAY0.524
id_i10_o10_true-unreach-call.c below 2 PASS0.516
id_i15_o15_false-unreach-call.c below 2 OKAY0.496
id_i15_o15_true-unreach-call.c below 2 PASS0.505
id_i20_o20_false-unreach-call.c below 2 OKAY0.496
id_i20_o20_true-unreach-call.c below 2 PASS0.485
id_i25_o25_false-unreach-call.c below 2 OKAY0.504
id_i25_o25_true-unreach-call.c below 2 PASS0.495
id_i5_o5_false-unreach-call.c below 2 OKAY0.518
id_i5_o5_true-unreach-call.c below 2 PASS0.507
id_o1000_false-unreach-call.c below 2 OKAY0.549
id_o100_false-unreach-call.c below 2 OKAY0.505
id_o10_false-unreach-call.c below 2 OKAY0.509
id_o200_false-unreach-call.c below 2 OKAY0.507
id_o20_false-unreach-call.c below 2 OKAY0.509
id_o3_false-unreach-call.c below 2 OKAY0.504
sum_10x0_false-unreach-call.c below 2 OKAY0.565
sum_10x0_true-unreach-call.c below 2 PASS0.572
sum_15x0_false-unreach-call.c below 2 OKAY0.588
sum_15x0_true-unreach-call.c below 2 PASS0.539
sum_20x0_false-unreach-call.c below 2 OKAY0.57
sum_20x0_true-unreach-call.c below 2 PASS0.565
sum_25x0_false-unreach-call.c below 2 OKAY0.571
sum_25x0_true-unreach-call.c below 2 PASS0.568
sum_2x3_false-unreach-call.c below 2 OKAY0.57
sum_2x3_true-unreach-call.c below 2 PASS0.541
sum_non_eq_false-unreach-call.c below 2 OKAY0.573
sum_non_eq_true-unreach-call.c below 2 PASS0.576
sum_non_false-unreach-call.c below 2 OKAY0.563
sum_non_true-unreach-call.c below 2 PASS0.55
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.548
/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.587
rec-bhmr2007_true-unreach-call.c below 2 PASS0.553
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.094
rec-cggmp2005_true-unreach-call.c below 2 PASS0.508
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.547
rec-css2003_true-unreach-call.c below 2 PASS1.497
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.076
rec-gj2007b_true-unreach-call.c below 2 FAIL0.542
rec-gj2007_true-unreach-call.c below 2 FAIL0.661
rec-gr2006_true-unreach-call.c below 2 FAIL0.675
rec-gsv2008_true-unreach-call.c below 2 PASS0.575
rec-hhk2008_true-unreach-call.c below 2 PASS0.525
rec-jm2006_true-unreach-call.c below 2 PASS0.682
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.715
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.632
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.873
/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.483
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.577
rec-count_by_2_true-unreach-call.c below 2 PASS0.469
rec-count_by_k_true-unreach-call.c below 2 PASS0.5
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.528
rec-gauss_sum_true-unreach-call.c below 2 PASS0.53
rec-half_true-unreach-call.c below 2 FAIL0.536
rec-nested_true-unreach-call.c below 3 FAIL0.848
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.471
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.611
cubic_polynomial_unsafe.c below 2 OKAY0.629
edit_distance_bottom_up.c below 3 FAIL194.208
edit_distance_top_down.c below 3 FAIL5.297
log_log_n_solution.c below 3 FAIL0.608
log_log_n_solution_unsafe.c below 3 OKAY0.602
log_n_solution.c below 2 FAIL0.603
log_n_solution_unsafe.c below 2 OKAY0.624
multivariate_1.c below TIMEOUT 300.094
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL3.571
multivariate_higher_order_unsafe.c below 7 OKAY3.546
n_cubed_solution.c below EXCEPTION 101.352
n_cubed_solution_unsafe.c below EXCEPTION 0.027
n_log_n_solution.c below 8 FAIL1.683
n_log_n_solution_unsafe.c below 8 OKAY1.65
n_squared_two_base_case_even.c below 2 PASS0.677
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.704
n_squared_two_base_case_odd.c below 2 PASS0.699
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.708
pascals_dynamic.c below 3 FAIL2.646
pascals_dynamic_unsafe.c below 3 OKAY2.63
pascals_iterative.c below 1 FAIL5.13
pascals_iterative_unsafe.c below 1 OKAY4.861
pascals_recursive.c below 8 FAIL3.612
pascals_recursive_unsafe.c below 8 OKAY3.643
squared_solution.c below 8 FAIL3.106
squared_solution_unsafe.c below 8 OKAY3.118
two_n_even.c below 2 PASS0.532
two_n_even_unsafe.c below 2 OKAY0.525
two_n_odd.c below 2 PASS0.536
two_n_odd_unsafe.c below 2 OKAY0.548
two_to_n_over_two_even.c below 7 FAIL295.076
two_to_n_over_two_even_unsafe.c below 7 OKAY134.696
two_to_n_over_two_odd.c below 7 FAIL244.211
two_to_n_over_two_odd_unsafe.c below 7 OKAY149.94
two_to_n_squared.c below 5 FAIL20.233
two_to_n_squared_unsafe.c below 5 OKAY20.196
two_to_two_to_n.c below 7 FAIL1.405
two_to_two_to_n_unsafe.c below 7 OKAY1.423
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1815.966
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.421
adding_and_mult_unsafe.c below 1 OKAY0.405
binary_search_array_tree.c below 1 FAIL0.794
exp_add_linear.c below 1 PASS0.519
exp_add_linear_unsafe.c below 1 OKAY0.54
exp_add_loop_rec.c below 1 FAIL0.406
exp_add_loop_rec_unsafe.c below 1 OKAY0.422
exp_add_loop_variable.c below 1 PASS0.513
exp_add_loop_variable_unsafe.c below 1 OKAY0.502
exp_with_linear_inner_loop.c below 1 FAIL0.605
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.642
halving_log1.c below 1 FAIL0.65
linear_two_to_n.c below 7 FAIL1.719
linear_two_to_n_unsafe.c below 7 OKAY1.75
loop_five_to_n.c below 1 PASS0.465
loop_five_to_n_unsafe.c below 1 OKAY0.467
non_loop_five_to_n.c below 7 FAIL54.709
non_loop_five_to_n_unsafe.c below 7 OKAY54.553
power_log_modified.c below 1 PASS0.696
simple_exponential.c below 1 PASS0.449
simple_exponential_for.c below 1 PASS0.477
simple_exponential_for_unsafe.c below 1 OKAY0.478
simple_exponential_unsafe.c below 1 OKAY0.468
two_to_n_minus_n.c below 7 FAIL2.323
two_to_n_minus_n_loop.c below TIMEOUT 300.004
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.008
two_to_n_minus_n_unsafe.c below 7 OKAY2.345
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 727.33
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.699
02.c below 3 FAIL0.934
03.c below 1 PASS0.549
04.c below 1 PASS0.395
05.c below 3 PASS1.306
06.c below 3 FAIL10.505
07.c below 3 PASS0.695
08.c below 3 PASS1.548
09.c below 3 PASS1.097
10.c below 3 FAIL1.28
11.c below 1 PASS0.396
12.c below 3 PASS1.601
13.c below 3 PASS0.699
14.c below 3 PASS0.619
15.c below 1 PASS0.371
16.c below 1 PASS0.52
17.c below 1 PASS3.391
18.c below 1 PASS0.461
19.c below 1 PASS0.552
20.c below 3 FAIL0.783
21.c below 3 PASS0.657
22.c below 3 FAIL0.885
23.c below 1 PASS0.426
24.c below 1 PASS0.489
25.c below 3 FAIL1.676
26.c below TIMEOUT 300.004
27.c below 1 PASS0.53
28.c below 3 PASS0.678
29.c below 3 PASS1.179
30.c below 1 PASS0.431
31.c below 3 PASS1.343
32.c below 1 FAIL0.436
33.c below 3 PASS1.404
34.c below 1 FAIL0.434
35.c below 1 PASS0.367
36.c below 3 PASS2.895
37.c below 3 FAIL0.645
38.c below 1 FAIL0.452
39.c below 3 PASS0.563
40.c below 3 PASS0.944
41.c below 1 PASS0.431
42.c below 3 PASS0.996
43.c below 3 PASS0.654
44.c below 1 PASS0.413
45.c below 3 FAIL2.921
46.c below 3 FAIL2.039
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 352.293
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.478
AGHKTW2017_foo.c below 1 PASS0.473
AGHKTW2017_loginSafe.c below 1 PASS1.014
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.6
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.562
BCK2011_gauss.c below 1 PASS0.543
BCK2011_strength_reduction.c below 1 PASS0.828
BCK2011_strength_reduction_linear.c below 1 PASS0.529
fibonacci_information_flow.c below 1 PASS0.657
loop_splitting_test_safe.c below 1 PASS0.692
TA2005_fib2.c below 1 PASS0.711
TA2005_fib.c below 1 PASS0.583
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.67
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.85
c3_cleanup_better.c below 3 PASS1.699
c3_cleanup.c below 3 PASS1.704
c3_intermediate.c below 3 PASS1.764
c3_noinv.c below 3 FAIL1.454
doublers.c below 1 FAIL0.645
doublers_easier.c below 3 FAIL1.286
doublers_easy.c below 1 FAIL0.712
exp_mult.c below 1 FAIL0.419
fig1_rotation_unsafe.c below 1 OKAY0.471
guessing_game.c below 3 FAIL0.596
not_P_solvable.c below 1 PASS0.394
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 11.994
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.444
maxequals_linear_1.c below 1 PASS0.64
maxequals_linear_2.c below 1 PASS0.673
maxequals_linear_3.c below 1 FAIL0.421
maxequals_linear_4.c below 1 PASS0.425
maxequals_linear_5.c below 1 PASS0.42
maxequals_linear_6.c below 1 FAIL0.425
maxequals_matrix1.c below 3 FAIL1.624
maxequals_matrix2.c below 3 FAIL1.613
maxequals_quadratic1.c below 1 FAIL0.431
maxequals_quadratic2.c below 1 PASS0.425
maxequals_stratified1.c below 3 PASS4.951
maxequals_stratified2.c below 3 PASS5.127
maxequals_stratified3.c below 3 FAIL5.279
nine.c below 1 FAIL0.422
nine_nondecreasing.c below 1 PASS0.664
sum_interval_1.c below 1 FAIL0.497
sum_interval_2.c below 1 FAIL0.505
sum_interval_3.c below 1 FAIL0.515
TrackingObjectFields.c below 3 PASS10.873
TrackingObjectFields_inlined.c below 1 PASS3.295
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 39.669
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.491
bobble2_varloop.c below 1 PASS0.487
bobble3.c below TIMEOUT 300.005
bobble4.c below 1 FAIL0.465
bobble5.c below 1 FAIL0.485
bobble.c below 1 PASS0.439
inchworm2.c below 1 TIMEOUT300.005
inchworm3.c below 1 PASS0.499
inchworm4.c below 1 PASS0.495
inchworm5.c below 1 PASS0.48
inchworm6_unsafe.c below 1 OKAY0.46
inchworm.c below 1 FAIL0.482
leapdiff2.c below 1 TIMEOUT300.004
leapfrog_annotated.c below 1 FAIL0.463
leapfrog_annotated_disjunction.c below 1 PASS0.482
leapfrog_asymmetric2.c below 1 FAIL0.538
leapfrog_asymmetric3.c below 1 FAIL0.546
leapfrog_asymmetric.c below 1 FAIL0.488
leapfrog.c below 1 FAIL0.433
leapfrog_materialized.c below 1 FAIL0.489
leapfrog_verbose.c below 1 FAIL0.488
leapspin.c below 1 FAIL0.407
leapsum2.c below 1 TIMEOUT300.006
leapthree.c below 1 FAIL0.501
microbobble2.c below 1 PASS0.446
microbobble3.c below 1 PASS0.439
microbobble_asymmetric.c below 1 PASS0.447
microbobble.c below 1 FAIL0.419
simple_bl2.c below 1 FAIL0.479
simple_bl3.c below 1 FAIL0.414
simple_bl.c below 1 FAIL0.488
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1212.77
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.337
binval_example_2_unsafe.c below 1 OKAY0.345
binval_example_3_unsafe.c below 1 OKAY0.343
binval_example_4.c below 1 PASS0.411
binval_example_4_unsafe.c below 1 OKAY0.423
binval_example_5.c below 1 FAIL1.606
binval_example_5_unsafe.c below 1 OKAY3.739
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.204