[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.435
qsort.c below 4 PASS1.255
speed_pldi09_fig1.c below 1 PASS0.673
speed_pldi09_fig4_2.c below 1 FAIL0.461
speed_pldi09_fig4_4.c below 1 PASS0.598
speed_pldi09_fig4_5.c below 1 PASS0.481
speed_pldi10_ex1.c below 1 PASS1.683
speed_pldi10_ex3.c below 1 PASS0.702
speed_pldi10_ex4.c below 1 PASS0.713
speed_popl10_fig2_1.c below 1 PASS0.619
speed_popl10_fig2_2.c below 1 FAIL0.421
speed_popl10_nested_multiple.c below 1 PASS0.593
speed_popl10_nested_single.c below 1 PASS0.538
speed_popl10_sequential_single.c below 1 PASS0.506
speed_popl10_simple_multiple.c below 1 PASS0.724
speed_popl10_simple_single_2.c below 1 PASS0.889
speed_popl10_simple_single.c below 1 PASS0.399
t07.c below 1 PASS0.576
t08.c below 1 PASS0.493
t09.c below 1 PASS0.475
t10.c below 1 PASS0.44
t11.c below 1 PASS0.617
t13.c below 1 FAIL0.525
t15.c below 1 PASS0.57
t16.c below 1 PASS0.486
t19.c below 1 PASS0.508
t20.c below 1 PASS0.454
t27.c below 1 PASS0.773
t28.c below 1 PASS0.728
t30.c below 1 FAIL0.465
t37.c below 2 PASS0.928
t39.c below 2 PASS0.771
t46.c below 1 PASS0.513
t47.c below 1 PASS0.688
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.118
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.49
qsort_full.c below 4 PASS11.696
rec1-param_safe.c below 2 PASS0.539
rec1-param_unsafe.c below 2 OKAY0.514
rec1_safe.c below 2 PASS0.463
rec1_unsafe.c below 2 OKAY0.459
rec2-param_safe.c below 2 PASS0.477
rec2-param_unsafe.c below 2 OKAY0.451
rec2_safe.c below 2 PASS0.474
rec2_unsafe.c below 2 OKAY0.45
rec-test.c below 2 PASS0.462
sas03_bothbranches.c below 7 PASS1.183
sas03.c below 2 PASS0.943
simulated_lese_recursive.c below 2 PASS0.672
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.273
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.39
count_up_down_unsafe.c below 1 OKAY0.394
divide.c below 1 PASS0.401
factor_unsafe.c below 1 OKAY0.361
for_infinite_loop_1_safe.c below 1 PASS0.36
for_infinite_loop_2_safe.c below 1 PASS0.353
interproc.c below 1 PASS0.316
mult.c below 1 PASS0.395
pointer_arith.c below 1 PASS0.334
quotient.c below 3 PASS0.729
subtract.c below 1 PASS0.369
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.379
sum01_bug02_unsafe.c below 1 OKAY0.729
sum01_real_safe.c below 1 PASS0.393
sum01_safe.c below 1 PASS0.402
sum01_unsafe.c below 1 OKAY0.607
sum02_safe.c below 1 PASS0.42
sum03_safe.c below 1 PASS0.481
sum03_unsafe.c below 1 OKAY0.588
sum04_safe.c below 1 PASS0.416
sum04_unsafe.c below 1 OKAY0.626
terminator_02_safe.c below 1 PASS0.352
terminator_02_unsafe.c below 1 OKAY0.404
terminator_03_safe.c below 1 PASS0.37
terminator_03_unsafe.c below 1 OKAY0.374
token_ring01_safe.c below 4 FAIL127.156
token_ring01_unsafe.c below 4 OKAY206.485
toy_safe.c below EXCEPTION 131.331
trex01_safe.c below 1 PASS0.819
trex01_unsafe.c below 1 OKAY0.455
trex02_safe2.c below 3 PASS0.548
trex02_safe.c below 3 PASS0.552
trex02_unsafe.c below 3 OKAY0.536
trex03_safe.c below 1 PASS0.517
trex03_unsafe.c below 1 OKAY0.503
trex04_safe.c below 1 PASS0.396
while_infinite_loop_1_safe.c below 1 PASS0.329
while_infinite_loop_2_safe.c below 1 PASS0.341
while_infinite_loop_3_safe.c below 1 PASS0.337
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 481.248
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.558
blogger_simplified1.c below 3 PASS1.61
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.55
mult-proc-params.c below 3 PASS0.539
popall.c below 1 PASS0.95
simulated_scc.c below 1 PASS0.845
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.056
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.438
degree2_binomial.c below 1 PASS0.886
degree2_monomial.c below 1 PASS0.486
degree3_binomial.c below 1 FAIL4.894
degree3_monomial.c below 1 PASS0.993
degree4_binomial.c below 1 FAIL5.149
degree4_monomial.c below 1 PASS1.651
degree5_binomial.c below 1 FAIL16.291
degree5_monomial.c below 1 PASS3.085
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 33.873
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.529
cubic_with_square_interproc.c below 2 FAIL0.746
cubic_with_square_nonlinear.c below 1 FAIL0.621
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.724
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.639
cubic_with_square_unsafe.c below 1 OKAY0.503
multi-input.c below 1 FAIL10.327
multi-input_unsafe.c below 1 OKAY10.516
nondet_loop_bound.c below 1 FAIL0.569
nondet_loop_bound_quartic.c below 1 FAIL0.762
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.777
nondet_loop_bound_unsafe.c below 1 OKAY0.573
nonlinear_stratified.c below 1 PASS125.423
nonlinear_stratified_unsafe.c below 1 OKAY68.049
quartic_with_cube.c below 1 FAIL0.727
quartic_with_cube_nonlinear.c below 1 FAIL0.966
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.966
quartic_with_cube_unsafe.c below 1 OKAY0.568
quintic_with_quartic.c below 1 PASS1.119
quintic_with_quartic_nonlinear.c below 1 PASS1.182
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.152
quintic_with_quartic_unsafe.c below 1 OKAY1.097
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 228.535
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.008
degree2_FD_AllAux_AllAssm.c below 1 PASS106.065
degree2_FD_AllAux_FewAssm.c below 1 PASS7.036
degree2_FD_FewAux_FewAssm.c below 1 PASS1.346
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.392
degree3.c below 1 PASS1.142
degree3_FD.c below 1 PASS1.287
degree4.c below 1 PASS1.917
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 121.193
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.553
loop_unsafe.c below 1 OKAY0.551
simulated_lese_parser.c below 1 PASS0.414
simulated_lese_sentinel.c below 1 PASS0.394
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.912
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.401
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.401
/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.387
array_false-unreach-call2.c below 1 OKAY0.414
array_false-unreach-call3.c below 1 OKAY0.396
array_true-unreach-call1.c below 1 FAIL0.404
array_true-unreach-call2.c below 1 FAIL0.423
array_true-unreach-call3.c below 1 PASS0.383
array_true-unreach-call4.c below 1 FAIL0.374
const_false-unreach-call1.c below 1 OKAY0.425
const_true-unreach-call1.c below 1 PASS0.401
diamond_false-unreach-call1.c below 1 OKAY0.396
diamond_true-unreach-call1.c below 1 PASS0.381
diamond_true-unreach-call2.c below 1 PASS0.408
functions_false-unreach-call1.c below 3 OKAY0.52
functions_true-unreach-call1.c below 3 PASS0.517
multivar_false-unreach-call1.c below 1 OKAY0.41
multivar_true-unreach-call1.c below 1 PASS0.394
nested_false-unreach-call1.c below 1 OKAY0.462
nested_true-unreach-call1.c below 1 PASS0.444
overflow_true-unreach-call1.c below 1 PASS0.346
phases_false-unreach-call1.c below 1 OKAY0.493
phases_false-unreach-call2.c below 1 OKAY0.391
phases_true-unreach-call1.c below 1 PASS0.495
phases_true-unreach-call2.c below 1 PASS0.376
simple_false-unreach-call1.c below 1 OKAY0.372
simple_false-unreach-call2.c below 1 OKAY0.358
simple_false-unreach-call3.c below 1 OKAY0.356
simple_false-unreach-call4.c below 1 OKAY0.376
simple_true-unreach-call1.c below 1 PASS0.374
simple_true-unreach-call2.c below 1 PASS0.342
simple_true-unreach-call3.c below 1 PASS0.356
simple_true-unreach-call4.c below 1 PASS0.376
underapprox_false-unreach-call1.c below 1 OKAY0.412
underapprox_false-unreach-call2.c below 1 OKAY0.404
underapprox_true-unreach-call1.c below 1 FAIL0.413
underapprox_true-unreach-call2.c below 1 PASS0.399
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.178
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.586
apache-get-tag_true-unreach-call.c below 1 FAIL0.598
down_true-unreach-call.c below 1 PASS0.46
fragtest_simple_true-unreach-call.c below 1 PASS0.581
half_2_true-unreach-call.c below 1 PASS0.531
heapsort_true-unreach-call.c below 1 PASS2.396
id_build_true-unreach-call.c below 1 PASS0.428
id_trans_false-unreach-call.c below 1 OKAY0.368
id_trans_true-unreach-call.c below 1 PASS0.384
large_const_true-unreach-call.c below 1 PASS0.515
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.465
nested6_true-unreach-call.c below 1 FAIL0.615
nested9_true-unreach-call.c below 1 PASS0.729
nest-if3_true-unreach-call.c below 1 PASS0.568
NetBSD_loop_true-unreach-call.c below 1 PASS0.399
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.483
seq_true-unreach-call.c below 1 PASS0.551
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.603
string_concat-noarr_true-unreach-call.c below 1 PASS0.504
up_true-unreach-call.c below 1 PASS0.48
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.244
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.442
bhmr2007_true-unreach-call.c below 1 PASS0.428
cggmp2005b_true-unreach-call.c below 1 PASS0.633
cggmp2005_true-unreach-call.c below 1 PASS0.41
cggmp2005_variant_true-unreach-call.c below 1 PASS0.416
css2003_true-unreach-call.c below 1 PASS1.124
ddlm2013_true-unreach-call.c below 1 PASS0.613
gcnr2008_false-unreach-call.c below 1 OKAY1.145
gj2007b_true-unreach-call.c below 1 FAIL0.453
gj2007_true-unreach-call.c below 1 PASS0.558
gr2006_true-unreach-call.c below 1 PASS0.563
gsv2008_true-unreach-call.c below 1 PASS0.402
hhk2008_true-unreach-call.c below 1 PASS0.391
jm2006_true-unreach-call.c below 1 PASS0.526
jm2006_variant_true-unreach-call.c below 1 PASS0.612
mcmillan2006_true-unreach-call.c below 1 FAIL0.475
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.191
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.36
count_by_1_variant_true-unreach-call.c below 1 PASS0.488
count_by_2_true-unreach-call.c below 1 PASS0.361
count_by_k_true-unreach-call.c below 1 PASS0.364
count_by_nondet_true-unreach-call.c below 1 PASS0.404
gauss_sum_true-unreach-call.c below 1 PASS0.436
half_true-unreach-call.c below 1 FAIL0.434
nested_true-unreach-call.c below 1 PASS0.513
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.36
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.421
array_true-unreach-call.c below 1 FAIL0.46
bubble_sort_false-unreach-call.c below 4 OKAY77.816
bubble_sort_true-unreach-call.c below 1 PASS5.292
compact_false-unreach-call.c below 1 OKAY0.474
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.395
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.388
eureka_01_false-unreach-call.c below 1 OKAY2.731
eureka_01_true-unreach-call.c below 1 FAIL1.634
eureka_05_true-unreach-call.c below 1 FAIL0.876
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.377
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.393
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.363
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.334
heavy_false-unreach-call.c below 1 OKAY0.597
heavy_true-unreach-call.c below 1 PASS0.575
insertion_sort_false-unreach-call.c below 1 OKAY1.488
insertion_sort_true-unreach-call.c below 1 FAIL0.624
invert_string_false-unreach-call.c below 1 OKAY0.59
invert_string_true-unreach-call.c below 1 FAIL0.669
linear_sea.ch_true-unreach-call.c below 1 FAIL0.416
linear_search_false-unreach-call.c below 1 OKAY0.45
lu.cmp_true-unreach-call.c below 3 PASS27.391
ludcmp_false-unreach-call.c below 3 OKAY27.22
matrix_false-unreach-call_true-termination.c below 1 OKAY1.386
matrix_true-unreach-call_true-termination.c below 1 FAIL0.529
n.c11_true-unreach-call.c below 3 FAIL0.578
n.c24_false-unreach-call.c below 3 OKAY5.351
n.c40_true-unreach-call.c below 1 FAIL0.397
nec11_false-unreach-call.c below 1 OKAY0.4
nec20_false-unreach-call.c below 1 OKAY0.445
nec40_true-unreach-call.c below 1 FAIL0.412
string_false-unreach-call.c below 1 OKAY0.736
string_true-unreach-call.c below 1 FAIL0.75
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.388
sum01_false-unreach-call_true-termination.c below 1 OKAY0.577
sum01_true-unreach-call_true-termination.c below 1 PASS0.4
sum03_false-unreach-call_true-termination.c below 1 OKAY0.629
sum03_true-unreach-call_false-termination.c below 1 PASS0.497
sum04_false-unreach-call_true-termination.c below 1 OKAY0.585
sum04_true-unreach-call_true-termination.c below 1 PASS0.404
sum_array_false-unreach-call.c below 1 OKAY0.649
sum_array_true-unreach-call.c below 1 FAIL0.685
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.368
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.619
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.454
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.365
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.379
trex01_false-unreach-call_true-termination.c below 3 OKAY0.618
trex01_true-unreach-call.c below 3 PASS0.928
trex02_false-unreach-call_true-termination.c below 3 OKAY0.528
trex02_true-unreach-call_true-termination.c below 3 PASS0.557
trex03_false-unreach-call_true-termination.c below 3 OKAY0.861
trex03_true-unreach-call.c below 3 PASS0.88
trex04_true-unreach-call_false-termination.c below 1 PASS0.442
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.4
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.206
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.407
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.422
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.176
vogal_false-unreach-call.c below 1 OKAY0.969
vogal_true-unreach-call.c below 1 FAIL0.963
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.336
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.322
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.333
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.331
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 195.366
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.545
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.564
Ackermann03_true-unreach-call.c below 7 FAIL1.595
Ackermann04_true-unreach-call.c below 7 FAIL1.618
Addition01_true-unreach-call_true-termination.c below 2 PASS0.811
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.809
Addition03_false-no-overflow.c below 2 PASS0.836
Addition03_true-unreach-call.c below 2 PASS0.831
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.621
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.555
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.561
Fibonacci01_true-unreach-call.c below TIMEOUT 300.006
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.005
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.726
gcd02_true-unreach-call.c below 2 FAIL1.366
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.256
McCarthy91_true-unreach-call.c below 7 FAIL1.264
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.755
Primes_true-unreach-call.c below 3 FAIL2.307
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.553
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.499
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.513
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.612
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.565
afterrec_2calls_true-unreach-call.c below 2 PASS0.547
afterrec_false-unreach-call.c below 2 OKAY0.47
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.006
fibo_15_false-unreach-call.c below TIMEOUT 300.004
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.005
fibo_25_false-unreach-call.c below TIMEOUT 300.006
fibo_25_true-unreach-call.c below TIMEOUT 300.004
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.005
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.006
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.005
fibo_5_false-unreach-call.c below TIMEOUT 300.004
fibo_5_true-unreach-call.c below TIMEOUT 300.005
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.983
id2_b3_o2_false-unreach-call.c below 2 OKAY0.975
id2_b3_o5_true-unreach-call.c below 2 PASS0.95
id2_b5_o10_true-unreach-call.c below 2 PASS0.928
id2_i5_o5_false-unreach-call.c below 2 OKAY0.576
id2_i5_o5_true-unreach-call.c below 2 PASS0.575
id_b2_o3_true-unreach-call.c below 2 PASS0.834
id_b3_o2_false-unreach-call.c below 2 OKAY0.853
id_b3_o5_true-unreach-call.c below 2 PASS0.869
id_b5_o10_true-unreach-call.c below 2 PASS0.83
id_i10_o10_false-unreach-call.c below 2 OKAY0.513
id_i10_o10_true-unreach-call.c below 2 PASS0.509
id_i15_o15_false-unreach-call.c below 2 OKAY0.519
id_i15_o15_true-unreach-call.c below 2 PASS0.521
id_i20_o20_false-unreach-call.c below 2 OKAY0.506
id_i20_o20_true-unreach-call.c below 2 PASS0.495
id_i25_o25_false-unreach-call.c below 2 OKAY0.499
id_i25_o25_true-unreach-call.c below 2 PASS0.526
id_i5_o5_false-unreach-call.c below 2 OKAY0.523
id_i5_o5_true-unreach-call.c below 2 PASS0.512
id_o1000_false-unreach-call.c below 2 OKAY0.507
id_o100_false-unreach-call.c below 2 OKAY0.532
id_o10_false-unreach-call.c below 2 OKAY0.509
id_o200_false-unreach-call.c below 2 OKAY0.543
id_o20_false-unreach-call.c below 2 OKAY0.487
id_o3_false-unreach-call.c below 2 OKAY0.517
sum_10x0_false-unreach-call.c below 2 OKAY0.551
sum_10x0_true-unreach-call.c below 2 PASS0.523
sum_15x0_false-unreach-call.c below 2 OKAY0.584
sum_15x0_true-unreach-call.c below 2 PASS0.603
sum_20x0_false-unreach-call.c below 2 OKAY0.565
sum_20x0_true-unreach-call.c below 2 PASS0.571
sum_25x0_false-unreach-call.c below 2 OKAY0.58
sum_25x0_true-unreach-call.c below 2 PASS0.556
sum_2x3_false-unreach-call.c below 2 OKAY0.571
sum_2x3_true-unreach-call.c below 2 PASS0.567
sum_non_eq_false-unreach-call.c below 2 OKAY0.571
sum_non_eq_true-unreach-call.c below 2 PASS0.572
sum_non_false-unreach-call.c below 2 OKAY0.577
sum_non_true-unreach-call.c below 2 PASS0.564
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.737
/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.553
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.544
rec-css2003_true-unreach-call.c below 2 PASS1.505
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.005
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.147
rec-gj2007b_true-unreach-call.c below 2 FAIL0.547
rec-gj2007_true-unreach-call.c below 2 FAIL0.698
rec-gr2006_true-unreach-call.c below 2 FAIL0.667
rec-gsv2008_true-unreach-call.c below 2 PASS0.592
rec-hhk2008_true-unreach-call.c below 2 PASS0.533
rec-jm2006_true-unreach-call.c below 2 PASS0.658
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.752
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.632
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 311.007
/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.477
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.567
rec-count_by_2_true-unreach-call.c below 2 PASS0.487
rec-count_by_k_true-unreach-call.c below 2 PASS0.515
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.54
rec-gauss_sum_true-unreach-call.c below 2 PASS0.566
rec-half_true-unreach-call.c below 2 FAIL0.543
rec-nested_true-unreach-call.c below 3 FAIL0.886
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.581
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.653
cubic_polynomial_unsafe.c below 2 OKAY0.638
edit_distance_bottom_up.c below 3 FAIL193.284
edit_distance_top_down.c below 3 FAIL5.203
log_log_n_solution.c below 3 FAIL0.582
log_log_n_solution_unsafe.c below 3 OKAY0.618
log_n_solution.c below 2 FAIL0.616
log_n_solution_unsafe.c below 2 OKAY0.601
multivariate_1.c below TIMEOUT 300.094
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL3.504
multivariate_higher_order_unsafe.c below 7 OKAY3.597
n_cubed_solution.c below EXCEPTION 103.564
n_cubed_solution_unsafe.c below EXCEPTION 0.028
n_log_n_solution.c below 8 FAIL1.782
n_log_n_solution_unsafe.c below 8 OKAY1.751
n_squared_two_base_case_even.c below 2 PASS0.709
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.693
n_squared_two_base_case_odd.c below 2 PASS0.747
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.725
pascals_dynamic.c below 3 FAIL2.729
pascals_dynamic_unsafe.c below 3 OKAY2.734
pascals_iterative.c below 1 FAIL5.153
pascals_iterative_unsafe.c below 1 OKAY5.12
pascals_recursive.c below 8 FAIL3.766
pascals_recursive_unsafe.c below 8 OKAY3.815
squared_solution.c below 8 FAIL3.202
squared_solution_unsafe.c below 8 OKAY3.278
two_n_even.c below 2 PASS0.533
two_n_even_unsafe.c below 2 OKAY0.561
two_n_odd.c below 2 PASS0.555
two_n_odd_unsafe.c below 2 OKAY0.547
two_to_n_over_two_even.c below 7 FAIL294.065
two_to_n_over_two_even_unsafe.c below 7 OKAY286.528
two_to_n_over_two_odd.c below 7 FAIL245.406
two_to_n_over_two_odd_unsafe.c below 7 OKAY136.376
two_to_n_squared.c below 5 FAIL19.991
two_to_n_squared_unsafe.c below 5 OKAY20.473
two_to_two_to_n.c below 7 FAIL1.517
two_to_two_to_n_unsafe.c below 7 OKAY1.423
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1957.166
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.441
adding_and_mult_unsafe.c below 1 OKAY0.428
binary_search_array_tree.c below 1 FAIL0.805
exp_add_linear.c below 1 PASS0.551
exp_add_linear_unsafe.c below 1 OKAY0.536
exp_add_loop_rec.c below 1 FAIL0.41
exp_add_loop_rec_unsafe.c below 1 OKAY0.414
exp_add_loop_variable.c below 1 PASS0.52
exp_add_loop_variable_unsafe.c below 1 OKAY0.523
exp_with_linear_inner_loop.c below 1 FAIL0.646
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.611
halving_log1.c below 1 FAIL0.672
linear_two_to_n.c below 7 FAIL1.773
linear_two_to_n_unsafe.c below 7 OKAY1.706
loop_five_to_n.c below 1 PASS0.476
loop_five_to_n_unsafe.c below 1 OKAY0.465
non_loop_five_to_n.c below 7 FAIL55.532
non_loop_five_to_n_unsafe.c below 7 OKAY55.305
power_log_modified.c below 1 PASS0.664
simple_exponential.c below 1 PASS0.467
simple_exponential_for.c below 1 PASS0.474
simple_exponential_for_unsafe.c below 1 OKAY0.47
simple_exponential_unsafe.c below 1 OKAY0.48
two_to_n_minus_n.c below 7 FAIL2.35
two_to_n_minus_n_loop.c below TIMEOUT 300.007
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.004
two_to_n_minus_n_unsafe.c below 7 OKAY2.373
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 729.103
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.705
02.c below 3 FAIL0.902
03.c below 1 PASS0.557
04.c below 1 PASS0.396
05.c below 3 PASS1.323
06.c below 3 FAIL10.621
07.c below 3 PASS0.717
08.c below 3 PASS1.615
09.c below 3 PASS1.084
10.c below 3 FAIL1.331
11.c below 1 PASS0.4
12.c below 3 PASS1.667
13.c below 3 PASS0.691
14.c below 3 PASS0.597
15.c below 1 PASS0.404
16.c below 1 PASS0.543
17.c below 1 PASS3.588
18.c below 1 PASS0.492
19.c below 1 PASS0.647
20.c below 3 FAIL0.851
21.c below 3 PASS0.688
22.c below 3 FAIL0.908
23.c below 1 PASS0.434
24.c below 1 PASS0.503
25.c below 3 FAIL1.693
26.c below TIMEOUT 300.007
27.c below 1 PASS0.517
28.c below 3 PASS0.686
29.c below 3 PASS1.244
30.c below 1 PASS0.424
31.c below 3 PASS1.34
32.c below 1 FAIL0.441
33.c below 3 PASS1.46
34.c below 1 FAIL0.451
35.c below 1 PASS0.364
36.c below 3 PASS2.859
37.c below 3 FAIL0.637
38.c below 1 FAIL0.451
39.c below 3 PASS0.56
40.c below 3 PASS0.936
41.c below 1 PASS0.438
42.c below 3 PASS0.989
43.c below 3 PASS0.675
44.c below 1 PASS0.421
45.c below 3 FAIL2.939
46.c below 3 FAIL2.029
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 353.225
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.5
AGHKTW2017_foo.c below 1 PASS0.495
AGHKTW2017_loginSafe.c below 1 PASS1.01
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.557
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.58
BCK2011_gauss.c below 1 PASS0.535
BCK2011_strength_reduction.c below 1 PASS0.835
BCK2011_strength_reduction_linear.c below 1 PASS0.552
fibonacci_information_flow.c below 1 PASS0.671
loop_splitting_test_safe.c below 1 PASS0.694
TA2005_fib2.c below 1 PASS0.714
TA2005_fib.c below 1 PASS0.567
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.71
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.843
c3_cleanup_better.c below 3 PASS1.692
c3_cleanup.c below 3 PASS1.722
c3_intermediate.c below 3 PASS1.731
c3_noinv.c below 3 FAIL1.482
doublers.c below 1 FAIL0.667
doublers_easier.c below 3 FAIL1.265
doublers_easy.c below 1 FAIL0.748
exp_mult.c below 1 FAIL0.412
fig1_rotation_unsafe.c below 1 OKAY0.442
guessing_game.c below 3 FAIL0.623
not_P_solvable.c below 1 PASS0.375
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 12.002
/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.658
maxequals_linear_2.c below 1 PASS0.669
maxequals_linear_3.c below 1 FAIL0.423
maxequals_linear_4.c below 1 PASS0.419
maxequals_linear_5.c below 1 PASS0.433
maxequals_linear_6.c below 1 FAIL0.454
maxequals_matrix1.c below 3 FAIL1.635
maxequals_matrix2.c below 3 FAIL1.647
maxequals_quadratic1.c below 1 FAIL0.413
maxequals_quadratic2.c below 1 PASS0.421
maxequals_stratified1.c below 3 PASS4.982
maxequals_stratified2.c below 3 PASS5.285
maxequals_stratified3.c below 3 FAIL5.412
nine.c below 1 FAIL0.435
nine_nondecreasing.c below 1 PASS0.699
sum_interval_1.c below 1 FAIL0.518
sum_interval_2.c below 1 FAIL0.505
sum_interval_3.c below 1 FAIL0.523
TrackingObjectFields.c below 3 PASS10.983
TrackingObjectFields_inlined.c below 1 PASS3.172
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 40.132
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.494
bobble2_varloop.c below 1 PASS0.494
bobble3.c below TIMEOUT 300.004
bobble4.c below 1 FAIL0.461
bobble5.c below 1 FAIL0.479
bobble.c below 1 PASS0.471
inchworm2.c below 1 TIMEOUT300.005
inchworm3.c below 1 PASS0.486
inchworm4.c below 1 PASS0.497
inchworm5.c below 1 PASS0.474
inchworm6_unsafe.c below 1 OKAY0.459
inchworm.c below 1 FAIL0.464
leapdiff2.c below 1 TIMEOUT300.006
leapfrog_annotated.c below 1 FAIL0.533
leapfrog_annotated_disjunction.c below 1 PASS0.495
leapfrog_asymmetric2.c below 1 FAIL0.552
leapfrog_asymmetric3.c below 1 FAIL0.553
leapfrog_asymmetric.c below 1 FAIL0.484
leapfrog.c below 1 FAIL0.437
leapfrog_materialized.c below 1 FAIL0.497
leapfrog_verbose.c below 1 FAIL0.486
leapspin.c below 1 FAIL0.402
leapsum2.c below 1 TIMEOUT300.004
leapthree.c below 1 FAIL0.47
microbobble2.c below 1 PASS0.451
microbobble3.c below 1 PASS0.45
microbobble_asymmetric.c below 1 PASS0.456
microbobble.c below 1 FAIL0.426
simple_bl2.c below 1 FAIL0.464
simple_bl3.c below 1 FAIL0.399
simple_bl.c below 1 FAIL0.479
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1212.832
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.356
binval_example_2_unsafe.c below 1 OKAY0.351
binval_example_3_unsafe.c below 1 OKAY0.351
binval_example_4.c below 1 PASS0.423
binval_example_4_unsafe.c below 1 OKAY0.428
binval_example_5.c below 1 FAIL1.62
binval_example_5_unsafe.c below 1 OKAY3.735
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.264