[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.418
kmp.c below 1 PASS1.368
qsort.c below 4 PASS1.265
speed_pldi09_fig1.c below 1 PASS0.697
speed_pldi09_fig4_2.c below 1 FAIL0.456
speed_pldi09_fig4_4.c below 1 PASS0.604
speed_pldi09_fig4_5.c below 1 PASS0.495
speed_pldi10_ex1.c below 1 PASS1.704
speed_pldi10_ex3.c below 1 PASS0.71
speed_pldi10_ex4.c below 1 PASS0.752
speed_popl10_fig2_1.c below 1 PASS0.633
speed_popl10_fig2_2.c below 1 FAIL0.444
speed_popl10_nested_multiple.c below 1 PASS0.588
speed_popl10_nested_single.c below 1 PASS0.521
speed_popl10_sequential_single.c below 1 PASS0.502
speed_popl10_simple_multiple.c below 1 PASS0.691
speed_popl10_simple_single_2.c below 1 PASS0.896
speed_popl10_simple_single.c below 1 PASS0.414
t07.c below 1 PASS0.568
t08.c below 1 PASS0.509
t09.c below 1 PASS0.434
t10.c below 1 PASS0.439
t11.c below 1 PASS0.652
t13.c below 1 FAIL0.553
t15.c below 1 PASS0.524
t16.c below 1 PASS0.488
t19.c below 1 PASS0.488
t20.c below 1 PASS0.458
t27.c below 1 PASS0.767
t28.c below 1 PASS0.702
t30.c below 1 FAIL0.491
t37.c below 2 PASS0.897
t39.c below 2 PASS0.793
t46.c below 1 PASS0.53
t47.c below 1 PASS0.715
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.166
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.483
qsort_full.c below 4 PASS11.465
rec1-param_safe.c below 2 PASS0.503
rec1-param_unsafe.c below 2 OKAY0.522
rec1_safe.c below 2 PASS0.452
rec1_unsafe.c below 2 OKAY0.473
rec2-param_safe.c below 2 PASS0.489
rec2-param_unsafe.c below 2 OKAY0.481
rec2_safe.c below 2 PASS0.474
rec2_unsafe.c below 2 OKAY0.474
rec-test.c below 2 PASS0.459
sas03_bothbranches.c below 7 PASS1.196
sas03.c below 2 PASS0.895
simulated_lese_recursive.c below 2 PASS0.655
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.021
/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.419
divide.c below 1 PASS0.39
factor_unsafe.c below 1 OKAY0.367
for_infinite_loop_1_safe.c below 1 PASS0.364
for_infinite_loop_2_safe.c below 1 PASS0.354
interproc.c below 1 PASS0.319
mult.c below 1 PASS0.368
pointer_arith.c below 1 PASS0.334
quotient.c below 3 PASS0.748
subtract.c below 1 PASS0.37
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.37
sum01_bug02_unsafe.c below 1 OKAY0.706
sum01_real_safe.c below 1 PASS0.388
sum01_safe.c below 1 PASS0.402
sum01_unsafe.c below 1 OKAY0.584
sum02_safe.c below 1 PASS0.425
sum03_safe.c below 1 PASS0.475
sum03_unsafe.c below 1 OKAY0.577
sum04_safe.c below 1 PASS0.405
sum04_unsafe.c below 1 OKAY0.596
terminator_02_safe.c below 1 PASS0.365
terminator_02_unsafe.c below 1 OKAY0.421
terminator_03_safe.c below 1 PASS0.359
terminator_03_unsafe.c below 1 OKAY0.373
token_ring01_safe.c below 4 FAIL127.074
token_ring01_unsafe.c below 4 OKAY202.489
toy_safe.c below EXCEPTION 129.152
trex01_safe.c below 1 PASS0.817
trex01_unsafe.c below 1 OKAY0.471
trex02_safe2.c below 3 PASS0.536
trex02_safe.c below 3 PASS0.534
trex02_unsafe.c below 3 OKAY0.541
trex03_safe.c below 1 PASS0.516
trex03_unsafe.c below 1 OKAY0.503
trex04_safe.c below 1 PASS0.416
while_infinite_loop_1_safe.c below 1 PASS0.336
while_infinite_loop_2_safe.c below 1 PASS0.335
while_infinite_loop_3_safe.c below 1 PASS0.339
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 474.922
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.542
blogger_simplified1.c below 3 PASS1.6
divided_difference2.c below TIMEOUT 300.006
mult-proc.c below 3 PASS0.532
mult-proc-params.c below 3 PASS0.523
popall.c below 1 PASS0.955
simulated_scc.c below 1 PASS0.843
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.001
/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.904
degree2_monomial.c below 1 PASS0.5
degree3_binomial.c below 1 FAIL4.856
degree3_monomial.c below 1 PASS0.994
degree4_binomial.c below 1 FAIL5.141
degree4_monomial.c below 1 PASS1.695
degree5_binomial.c below 1 FAIL16.173
degree5_monomial.c below 1 PASS3.097
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 33.777
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.522
cubic_with_square_interproc.c below 2 FAIL0.72
cubic_with_square_nonlinear.c below 1 FAIL0.642
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.765
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.652
cubic_with_square_unsafe.c below 1 OKAY0.49
multi-input.c below 1 FAIL10.254
multi-input_unsafe.c below 1 OKAY10.345
nondet_loop_bound.c below 1 FAIL0.554
nondet_loop_bound_quartic.c below 1 FAIL0.765
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.759
nondet_loop_bound_unsafe.c below 1 OKAY0.559
nonlinear_stratified.c below 1 PASS123.543
nonlinear_stratified_unsafe.c below 1 OKAY71.105
quartic_with_cube.c below 1 FAIL0.691
quartic_with_cube_nonlinear.c below 1 FAIL0.972
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.973
quartic_with_cube_unsafe.c below 1 OKAY0.596
quintic_with_quartic.c below 1 PASS1.092
quintic_with_quartic_nonlinear.c below 1 PASS1.195
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.141
quintic_with_quartic_unsafe.c below 1 OKAY1.104
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 229.439
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.979
degree2_FD_AllAux_AllAssm.c below 1 PASS105.026
degree2_FD_AllAux_FewAssm.c below 1 PASS7.201
degree2_FD_FewAux_FewAssm.c below 1 PASS1.351
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.369
degree3.c below 1 PASS1.172
degree3_FD.c below 1 PASS1.239
degree4.c below 1 PASS1.964
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 120.301
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.536
loop_unsafe.c below 1 OKAY0.547
simulated_lese_parser.c below 1 PASS0.4
simulated_lese_sentinel.c below 1 PASS0.391
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.874
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.393
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.393
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.008
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.008
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.397
array_false-unreach-call2.c below 1 OKAY0.404
array_false-unreach-call3.c below 1 OKAY0.378
array_true-unreach-call1.c below 1 FAIL0.393
array_true-unreach-call2.c below 1 FAIL0.405
array_true-unreach-call3.c below 1 PASS0.379
array_true-unreach-call4.c below 1 FAIL0.369
const_false-unreach-call1.c below 1 OKAY0.389
const_true-unreach-call1.c below 1 PASS0.399
diamond_false-unreach-call1.c below 1 OKAY0.395
diamond_true-unreach-call1.c below 1 PASS0.397
diamond_true-unreach-call2.c below 1 PASS0.406
functions_false-unreach-call1.c below 3 OKAY0.526
functions_true-unreach-call1.c below 3 PASS0.519
multivar_false-unreach-call1.c below 1 OKAY0.413
multivar_true-unreach-call1.c below 1 PASS0.407
nested_false-unreach-call1.c below 1 OKAY0.447
nested_true-unreach-call1.c below 1 PASS0.471
overflow_true-unreach-call1.c below 1 PASS0.36
phases_false-unreach-call1.c below 1 OKAY0.487
phases_false-unreach-call2.c below 1 OKAY0.383
phases_true-unreach-call1.c below 1 PASS0.5
phases_true-unreach-call2.c below 1 PASS0.375
simple_false-unreach-call1.c below 1 OKAY0.379
simple_false-unreach-call2.c below 1 OKAY0.36
simple_false-unreach-call3.c below 1 OKAY0.367
simple_false-unreach-call4.c below 1 OKAY0.365
simple_true-unreach-call1.c below 1 PASS0.365
simple_true-unreach-call2.c below 1 PASS0.357
simple_true-unreach-call3.c below 1 PASS0.364
simple_true-unreach-call4.c below 1 PASS0.366
underapprox_false-unreach-call1.c below 1 OKAY0.416
underapprox_false-unreach-call2.c below 1 OKAY0.423
underapprox_true-unreach-call1.c below 1 FAIL0.401
underapprox_true-unreach-call2.c below 1 PASS0.389
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.151
/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.607
down_true-unreach-call.c below 1 PASS0.455
fragtest_simple_true-unreach-call.c below 1 PASS0.598
half_2_true-unreach-call.c below 1 PASS0.5
heapsort_true-unreach-call.c below 1 PASS2.281
id_build_true-unreach-call.c below 1 PASS0.424
id_trans_false-unreach-call.c below 1 OKAY0.362
id_trans_true-unreach-call.c below 1 PASS0.386
large_const_true-unreach-call.c below 1 PASS0.516
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.447
nested6_true-unreach-call.c below 1 FAIL0.626
nested9_true-unreach-call.c below 1 PASS0.705
nest-if3_true-unreach-call.c below 1 PASS0.569
NetBSD_loop_true-unreach-call.c below 1 PASS0.377
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.506
seq_true-unreach-call.c below 1 PASS0.537
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.618
string_concat-noarr_true-unreach-call.c below 1 PASS0.502
up_true-unreach-call.c below 1 PASS0.459
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.054
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.416
bhmr2007_true-unreach-call.c below 1 PASS0.444
cggmp2005b_true-unreach-call.c below 1 PASS0.644
cggmp2005_true-unreach-call.c below 1 PASS0.406
cggmp2005_variant_true-unreach-call.c below 1 PASS0.408
css2003_true-unreach-call.c below 1 PASS1.104
ddlm2013_true-unreach-call.c below 1 PASS0.623
gcnr2008_false-unreach-call.c below 1 OKAY1.141
gj2007b_true-unreach-call.c below 1 FAIL0.457
gj2007_true-unreach-call.c below 1 PASS0.565
gr2006_true-unreach-call.c below 1 PASS0.597
gsv2008_true-unreach-call.c below 1 PASS0.39
hhk2008_true-unreach-call.c below 1 PASS0.389
jm2006_true-unreach-call.c below 1 PASS0.52
jm2006_variant_true-unreach-call.c below 1 PASS0.629
mcmillan2006_true-unreach-call.c below 1 FAIL0.464
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.197
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.354
count_by_1_variant_true-unreach-call.c below 1 PASS0.481
count_by_2_true-unreach-call.c below 1 PASS0.359
count_by_k_true-unreach-call.c below 1 PASS0.388
count_by_nondet_true-unreach-call.c below 1 PASS0.392
gauss_sum_true-unreach-call.c below 1 PASS0.439
half_true-unreach-call.c below 1 FAIL0.411
nested_true-unreach-call.c below 1 PASS0.53
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.354
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.44
array_true-unreach-call.c below 1 FAIL0.422
bubble_sort_false-unreach-call.c below 4 OKAY78.205
bubble_sort_true-unreach-call.c below 1 PASS5.159
compact_false-unreach-call.c below 1 OKAY0.459
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.4
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.401
eureka_01_false-unreach-call.c below 1 OKAY2.678
eureka_01_true-unreach-call.c below 1 FAIL1.626
eureka_05_true-unreach-call.c below 1 FAIL0.857
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.386
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.387
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.358
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.35
heavy_false-unreach-call.c below 1 OKAY0.595
heavy_true-unreach-call.c below 1 PASS0.595
insertion_sort_false-unreach-call.c below 1 OKAY1.54
insertion_sort_true-unreach-call.c below 1 FAIL0.614
invert_string_false-unreach-call.c below 1 OKAY0.565
invert_string_true-unreach-call.c below 1 FAIL0.636
linear_sea.ch_true-unreach-call.c below 1 FAIL0.417
linear_search_false-unreach-call.c below 1 OKAY0.419
lu.cmp_true-unreach-call.c below 3 PASS27.895
ludcmp_false-unreach-call.c below 3 OKAY27.211
matrix_false-unreach-call_true-termination.c below 1 OKAY1.353
matrix_true-unreach-call_true-termination.c below 1 FAIL0.522
n.c11_true-unreach-call.c below 3 FAIL0.588
n.c24_false-unreach-call.c below 3 OKAY5.28
n.c40_true-unreach-call.c below 1 FAIL0.398
nec11_false-unreach-call.c below 1 OKAY0.399
nec20_false-unreach-call.c below 1 OKAY0.436
nec40_true-unreach-call.c below 1 FAIL0.4
string_false-unreach-call.c below 1 OKAY0.735
string_true-unreach-call.c below 1 FAIL0.745
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.744
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.388
sum01_false-unreach-call_true-termination.c below 1 OKAY0.585
sum01_true-unreach-call_true-termination.c below 1 PASS0.395
sum03_false-unreach-call_true-termination.c below 1 OKAY0.633
sum03_true-unreach-call_false-termination.c below 1 PASS0.489
sum04_false-unreach-call_true-termination.c below 1 OKAY0.608
sum04_true-unreach-call_true-termination.c below 1 PASS0.407
sum_array_false-unreach-call.c below 1 OKAY0.649
sum_array_true-unreach-call.c below 1 FAIL0.702
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.349
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.613
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.414
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.368
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.377
trex01_false-unreach-call_true-termination.c below 3 OKAY0.616
trex01_true-unreach-call.c below 3 PASS0.92
trex02_false-unreach-call_true-termination.c below 3 OKAY0.551
trex02_true-unreach-call_true-termination.c below 3 PASS0.564
trex03_false-unreach-call_true-termination.c below 3 OKAY0.852
trex03_true-unreach-call.c below 3 PASS0.861
trex04_true-unreach-call_false-termination.c below 1 PASS0.421
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.413
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.208
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.416
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.397
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.18
vogal_false-unreach-call.c below 1 OKAY0.945
vogal_true-unreach-call.c below 1 FAIL0.936
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.331
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.327
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.335
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.344
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 195.809
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.603
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.53
Ackermann03_true-unreach-call.c below 7 FAIL1.605
Ackermann04_true-unreach-call.c below 7 FAIL1.628
Addition01_true-unreach-call_true-termination.c below 2 PASS0.787
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.82
Addition03_false-no-overflow.c below 2 PASS0.839
Addition03_true-unreach-call.c below 2 PASS0.803
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.612
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.556
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.553
Fibonacci01_true-unreach-call.c below TIMEOUT 300.004
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.005
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.005
gcd01_true-unreach-call_true-termination.c below 2 PASS0.729
gcd02_true-unreach-call.c below 2 FAIL1.436
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.241
McCarthy91_true-unreach-call.c below 7 FAIL1.24
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.754
Primes_true-unreach-call.c below 3 FAIL2.287
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.447
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.496
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.517
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.507
/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.557
afterrec_false-unreach-call.c below 2 OKAY0.483
afterrec_true-unreach-call.c below 2 PASS0.458
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.004
fibo_15_true-unreach-call.c below TIMEOUT 300.004
fibo_20_false-unreach-call.c below TIMEOUT 300.007
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.006
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.007
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.006
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.006
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.005
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.006
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.005
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.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.005
fibo_7_true-unreach-call.c below TIMEOUT 300.006
id2_b2_o3_true-unreach-call.c below 2 PASS0.976
id2_b3_o2_false-unreach-call.c below 2 OKAY0.955
id2_b3_o5_true-unreach-call.c below 2 PASS0.966
id2_b5_o10_true-unreach-call.c below 2 PASS0.951
id2_i5_o5_false-unreach-call.c below 2 OKAY0.573
id2_i5_o5_true-unreach-call.c below 2 PASS0.575
id_b2_o3_true-unreach-call.c below 2 PASS0.934
id_b3_o2_false-unreach-call.c below 2 OKAY0.893
id_b3_o5_true-unreach-call.c below 2 PASS0.837
id_b5_o10_true-unreach-call.c below 2 PASS0.83
id_i10_o10_false-unreach-call.c below 2 OKAY0.501
id_i10_o10_true-unreach-call.c below 2 PASS0.541
id_i15_o15_false-unreach-call.c below 2 OKAY0.512
id_i15_o15_true-unreach-call.c below 2 PASS0.527
id_i20_o20_false-unreach-call.c below 2 OKAY0.506
id_i20_o20_true-unreach-call.c below 2 PASS0.517
id_i25_o25_false-unreach-call.c below 2 OKAY0.514
id_i25_o25_true-unreach-call.c below 2 PASS0.524
id_i5_o5_false-unreach-call.c below 2 OKAY0.511
id_i5_o5_true-unreach-call.c below 2 PASS0.501
id_o1000_false-unreach-call.c below 2 OKAY0.521
id_o100_false-unreach-call.c below 2 OKAY0.546
id_o10_false-unreach-call.c below 2 OKAY0.512
id_o200_false-unreach-call.c below 2 OKAY0.52
id_o20_false-unreach-call.c below 2 OKAY0.51
id_o3_false-unreach-call.c below 2 OKAY0.52
sum_10x0_false-unreach-call.c below 2 OKAY0.573
sum_10x0_true-unreach-call.c below 2 PASS0.57
sum_15x0_false-unreach-call.c below 2 OKAY0.573
sum_15x0_true-unreach-call.c below 2 PASS0.552
sum_20x0_false-unreach-call.c below 2 OKAY0.599
sum_20x0_true-unreach-call.c below 2 PASS0.556
sum_25x0_false-unreach-call.c below 2 OKAY0.599
sum_25x0_true-unreach-call.c below 2 PASS0.57
sum_2x3_false-unreach-call.c below 2 OKAY0.555
sum_2x3_true-unreach-call.c below 2 PASS0.589
sum_non_eq_false-unreach-call.c below 2 OKAY0.558
sum_non_eq_true-unreach-call.c below 2 PASS0.574
sum_non_false-unreach-call.c below 2 OKAY0.563
sum_non_true-unreach-call.c below 2 PASS0.54
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.985
/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.565
rec-bhmr2007_true-unreach-call.c below 2 PASS0.561
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.083
rec-cggmp2005_true-unreach-call.c below 2 PASS0.511
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.542
rec-css2003_true-unreach-call.c below 2 PASS1.492
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.005
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.108
rec-gj2007b_true-unreach-call.c below 2 FAIL0.518
rec-gj2007_true-unreach-call.c below 2 FAIL0.661
rec-gr2006_true-unreach-call.c below 2 FAIL0.682
rec-gsv2008_true-unreach-call.c below 2 PASS0.548
rec-hhk2008_true-unreach-call.c below 2 PASS0.511
rec-jm2006_true-unreach-call.c below 2 PASS0.659
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.723
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.632
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.801
/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.462
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.559
rec-count_by_2_true-unreach-call.c below 2 PASS0.458
rec-count_by_k_true-unreach-call.c below 2 PASS0.485
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.509
rec-gauss_sum_true-unreach-call.c below 2 PASS0.554
rec-half_true-unreach-call.c below 2 FAIL0.54
rec-nested_true-unreach-call.c below 3 FAIL0.89
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.457
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.632
cubic_polynomial_unsafe.c below 2 OKAY0.63
edit_distance_bottom_up.c below 3 FAIL187.467
edit_distance_top_down.c below 3 FAIL5.296
log_log_n_solution.c below 3 FAIL0.603
log_log_n_solution_unsafe.c below 3 OKAY0.601
log_n_solution.c below 2 FAIL0.596
log_n_solution_unsafe.c below 2 OKAY0.605
multivariate_1.c below TIMEOUT 300.095
multivariate_1_unsafe.c below TIMEOUT 300.094
multivariate_higher_order.c below 7 FAIL3.48
multivariate_higher_order_unsafe.c below 7 OKAY3.512
n_cubed_solution.c below EXCEPTION 102.48
n_cubed_solution_unsafe.c below EXCEPTION 0.026
n_log_n_solution.c below 8 FAIL1.667
n_log_n_solution_unsafe.c below 8 OKAY1.651
n_squared_two_base_case_even.c below 2 PASS0.707
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.7
n_squared_two_base_case_odd.c below 2 PASS0.709
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.706
pascals_dynamic.c below 3 FAIL2.768
pascals_dynamic_unsafe.c below 3 OKAY2.624
pascals_iterative.c below 1 FAIL4.96
pascals_iterative_unsafe.c below 1 OKAY5.079
pascals_recursive.c below 8 FAIL3.765
pascals_recursive_unsafe.c below 8 OKAY3.708
squared_solution.c below 8 FAIL3.202
squared_solution_unsafe.c below 8 OKAY3.243
two_n_even.c below 2 PASS0.536
two_n_even_unsafe.c below 2 OKAY0.546
two_n_odd.c below 2 PASS0.535
two_n_odd_unsafe.c below 2 OKAY0.542
two_to_n_over_two_even.c below 7 FAIL293.683
two_to_n_over_two_even_unsafe.c below 7 OKAY293.031
two_to_n_over_two_odd.c below 7 FAIL245.977
two_to_n_over_two_odd_unsafe.c below 7 OKAY148.078
two_to_n_squared.c below 5 FAIL20.16
two_to_n_squared_unsafe.c below 5 OKAY20.465
two_to_two_to_n.c below 7 FAIL1.482
two_to_two_to_n_unsafe.c below 7 OKAY1.47
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1968.111
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.418
adding_and_mult_unsafe.c below 1 OKAY0.431
binary_search_array_tree.c below 1 FAIL0.85
exp_add_linear.c below 1 PASS0.555
exp_add_linear_unsafe.c below 1 OKAY0.53
exp_add_loop_rec.c below 1 FAIL0.417
exp_add_loop_rec_unsafe.c below 1 OKAY0.426
exp_add_loop_variable.c below 1 PASS0.533
exp_add_loop_variable_unsafe.c below 1 OKAY0.509
exp_with_linear_inner_loop.c below 1 FAIL0.635
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.633
halving_log1.c below 1 FAIL0.662
linear_two_to_n.c below 7 FAIL1.764
linear_two_to_n_unsafe.c below 7 OKAY1.764
loop_five_to_n.c below 1 PASS0.475
loop_five_to_n_unsafe.c below 1 OKAY0.462
non_loop_five_to_n.c below 7 FAIL55.412
non_loop_five_to_n_unsafe.c below 7 OKAY55.01
power_log_modified.c below 1 PASS0.666
simple_exponential.c below 1 PASS0.472
simple_exponential_for.c below 1 PASS0.479
simple_exponential_for_unsafe.c below 1 OKAY0.484
simple_exponential_unsafe.c below 1 OKAY0.461
two_to_n_minus_n.c below 7 FAIL2.354
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.382
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 728.796
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.737
02.c below 3 FAIL0.934
03.c below 1 PASS0.527
04.c below 1 PASS0.417
05.c below 3 PASS1.271
06.c below 3 FAIL10.37
07.c below 3 PASS0.707
08.c below 3 PASS1.603
09.c below 3 PASS1.116
10.c below 3 FAIL1.327
11.c below 1 PASS0.418
12.c below 3 PASS1.589
13.c below 3 PASS0.708
14.c below 3 PASS0.587
15.c below 1 PASS0.398
16.c below 1 PASS0.534
17.c below 1 PASS3.668
18.c below 1 PASS0.479
19.c below 1 PASS0.563
20.c below 3 FAIL0.82
21.c below 3 PASS0.704
22.c below 3 FAIL0.9
23.c below 1 PASS0.417
24.c below 1 PASS0.513
25.c below 3 FAIL1.65
26.c below TIMEOUT 300.007
27.c below 1 PASS0.544
28.c below 3 PASS0.694
29.c below 3 PASS1.176
30.c below 1 PASS0.418
31.c below 3 PASS1.394
32.c below 1 FAIL0.432
33.c below 3 PASS1.397
34.c below 1 FAIL0.451
35.c below 1 PASS0.369
36.c below 3 PASS2.856
37.c below 3 FAIL0.672
38.c below 1 FAIL0.442
39.c below 3 PASS0.55
40.c below 3 PASS0.965
41.c below 1 PASS0.43
42.c below 3 PASS1.008
43.c below 3 PASS0.671
44.c below 1 PASS0.414
45.c below 3 FAIL2.962
46.c below 3 FAIL2.018
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 352.827
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.499
AGHKTW2017_foo.c below 1 PASS0.485
AGHKTW2017_loginSafe.c below 1 PASS1.019
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.56
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.558
BCK2011_gauss.c below 1 PASS0.54
BCK2011_strength_reduction.c below 1 PASS0.884
BCK2011_strength_reduction_linear.c below 1 PASS0.528
fibonacci_information_flow.c below 1 PASS0.672
loop_splitting_test_safe.c below 1 PASS0.704
TA2005_fib2.c below 1 PASS0.725
TA2005_fib.c below 1 PASS0.573
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.747
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.864
c3_cleanup_better.c below 3 PASS1.687
c3_cleanup.c below 3 PASS1.704
c3_intermediate.c below 3 PASS1.736
c3_noinv.c below 3 FAIL1.442
doublers.c below 1 FAIL0.648
doublers_easier.c below 3 FAIL1.27
doublers_easy.c below 1 FAIL0.719
exp_mult.c below 1 FAIL0.428
fig1_rotation_unsafe.c below 1 OKAY0.479
guessing_game.c below 3 FAIL0.632
not_P_solvable.c below 1 PASS0.387
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 11.996
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.446
maxequals_linear_1.c below 1 PASS0.645
maxequals_linear_2.c below 1 PASS0.644
maxequals_linear_3.c below 1 FAIL0.447
maxequals_linear_4.c below 1 PASS0.434
maxequals_linear_5.c below 1 PASS0.417
maxequals_linear_6.c below 1 FAIL0.451
maxequals_matrix1.c below 3 FAIL1.657
maxequals_matrix2.c below 3 FAIL1.702
maxequals_quadratic1.c below 1 FAIL0.443
maxequals_quadratic2.c below 1 PASS0.443
maxequals_stratified1.c below 3 PASS5.063
maxequals_stratified2.c below 3 PASS5.186
maxequals_stratified3.c below 3 FAIL5.257
nine.c below 1 FAIL0.443
nine_nondecreasing.c below 1 PASS0.659
sum_interval_1.c below 1 FAIL0.514
sum_interval_2.c below 1 FAIL0.494
sum_interval_3.c below 1 FAIL0.518
TrackingObjectFields.c below 3 PASS11.088
TrackingObjectFields_inlined.c below 1 PASS3.159
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 40.11
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.516
bobble2_varloop.c below 1 PASS0.487
bobble3.c below TIMEOUT 300.003
bobble4.c below 1 FAIL0.468
bobble5.c below 1 FAIL0.457
bobble.c below 1 PASS0.458
inchworm2.c below 1 TIMEOUT300.004
inchworm3.c below 1 PASS0.47
inchworm4.c below 1 PASS0.485
inchworm5.c below 1 PASS0.478
inchworm6_unsafe.c below 1 OKAY0.444
inchworm.c below 1 FAIL0.462
leapdiff2.c below 1 TIMEOUT300.006
leapfrog_annotated.c below 1 FAIL0.467
leapfrog_annotated_disjunction.c below 1 PASS0.469
leapfrog_asymmetric2.c below 1 FAIL0.545
leapfrog_asymmetric3.c below 1 FAIL0.544
leapfrog_asymmetric.c below 1 FAIL0.502
leapfrog.c below 1 FAIL0.427
leapfrog_materialized.c below 1 FAIL0.476
leapfrog_verbose.c below 1 FAIL0.482
leapspin.c below 1 FAIL0.419
leapsum2.c below 1 TIMEOUT300.004
leapthree.c below 1 FAIL0.482
microbobble2.c below 1 PASS0.455
microbobble3.c below 1 PASS0.441
microbobble_asymmetric.c below 1 PASS0.443
microbobble.c below 1 FAIL0.437
simple_bl2.c below 1 FAIL0.485
simple_bl3.c below 1 FAIL0.409
simple_bl.c below 1 FAIL0.479
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1212.704
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.348
binval_example_2_unsafe.c below 1 OKAY0.348
binval_example_3_unsafe.c below 1 OKAY0.356
binval_example_4.c below 1 PASS0.429
binval_example_4_unsafe.c below 1 OKAY0.416
binval_example_5.c below 1 FAIL1.6
binval_example_5_unsafe.c below 1 OKAY3.768
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.265