[Version Information]
WALi-OpenNWA version: f73a8d6dbe21a2004e864fa68f50e0f3de181d25 (2017-12-06 13:06:14 -0600) "Adding guessing_game.c benchmark"
duet version: e0a1b1e22f1b8f755b70e388abf4b098326cd3c9 (2017-12-11 14:36:14 -0500) "Symbolic bounds always include constant bounds if they exist"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.7.0  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
camlp4               4.02+7  Camlp4 is a system for writing extensible parsers f
cil                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
conf-which                1  Virtual package relying on which
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170712  LR(1) parser generator
mlgmpidl              1.2.4  OCaml interface to the GMP library
num                       0  The Num library for arbitrary-precision integer and
oasis                0.4.10  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.3  A library manager for OCaml
ocamlgraph            1.8.7  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.8  Generate OCaml modules from source files
OCRS               20170905  Recurrence solver based on operational calculus
optcomp                 1.6  Optional compilation with cpp-like directives
ounit                 2.0.0  Unit testing framework loosely based on HUnit. It i
ppx_deriving            3.2  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
Z3                 20161217  Z3 SMT solver

Test Name Output No. of Rounds Result Run Time
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below 1 FAIL0.425
kmp.c below 1 PASS1.378
qsort.c below 4 PASS1.308
speed_pldi09_fig1.c below 1 PASS0.685
speed_pldi09_fig4_2.c below 1 FAIL0.45
speed_pldi09_fig4_4.c below 1 PASS0.612
speed_pldi09_fig4_5.c below 1 PASS0.5
speed_pldi10_ex1.c below 1 PASS1.72
speed_pldi10_ex3.c below 1 PASS0.691
speed_pldi10_ex4.c below 1 PASS0.748
speed_popl10_fig2_1.c below 1 PASS0.635
speed_popl10_fig2_2.c below 1 FAIL0.432
speed_popl10_nested_multiple.c below 1 PASS0.584
speed_popl10_nested_single.c below 1 PASS0.539
speed_popl10_sequential_single.c below 1 PASS0.5
speed_popl10_simple_multiple.c below 1 PASS0.715
speed_popl10_simple_single_2.c below 1 PASS0.911
speed_popl10_simple_single.c below 1 PASS0.424
t07.c below 1 PASS0.57
t08.c below 1 PASS0.496
t09.c below 1 PASS0.463
t10.c below 1 PASS0.437
t11.c below 1 PASS0.635
t13.c below 1 FAIL0.525
t15.c below 1 PASS0.518
t16.c below 1 PASS0.506
t19.c below 1 PASS0.488
t20.c below 1 PASS0.483
t27.c below 1 PASS0.777
t28.c below 1 PASS0.722
t30.c below 1 FAIL0.484
t37.c below 2 PASS0.929
t39.c below 2 PASS0.791
t46.c below 1 PASS0.531
t47.c below 1 PASS0.684
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.296
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.489
qsort_full.c below 4 PASS12.049
rec1-param_safe.c below 2 PASS0.527
rec1-param_unsafe.c below 2 OKAY0.507
rec1_safe.c below 2 PASS0.479
rec1_unsafe.c below 2 OKAY0.467
rec2-param_safe.c below 2 PASS0.489
rec2-param_unsafe.c below 2 OKAY0.466
rec2_safe.c below 2 PASS0.493
rec2_unsafe.c below 2 OKAY0.479
rec-test.c below 2 PASS0.468
sas03_bothbranches.c below 7 PASS1.24
sas03.c below 2 PASS0.901
simulated_lese_recursive.c below 2 PASS0.665
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.719
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.399
count_up_down_unsafe.c below 1 OKAY0.405
divide.c below 1 PASS0.399
factor_unsafe.c below 1 OKAY0.364
for_infinite_loop_1_safe.c below 1 PASS0.38
for_infinite_loop_2_safe.c below 1 PASS0.355
interproc.c below 1 PASS0.34
mult.c below 1 PASS0.39
pointer_arith.c below 1 PASS0.341
quotient.c below 3 PASS0.73
subtract.c below 1 PASS0.377
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.384
sum01_bug02_unsafe.c below 1 OKAY0.722
sum01_real_safe.c below 1 PASS0.37
sum01_safe.c below 1 PASS0.411
sum01_unsafe.c below 1 OKAY0.584
sum02_safe.c below 1 PASS0.424
sum03_safe.c below 1 PASS0.481
sum03_unsafe.c below 1 OKAY0.586
sum04_safe.c below 1 PASS0.421
sum04_unsafe.c below 1 OKAY0.588
terminator_02_safe.c below 1 PASS0.359
terminator_02_unsafe.c below 1 OKAY0.423
terminator_03_safe.c below 1 PASS0.363
terminator_03_unsafe.c below 1 OKAY0.363
token_ring01_safe.c below 4 FAIL130.005
token_ring01_unsafe.c below 4 OKAY207.566
toy_safe.c below EXCEPTION 131.095
trex01_safe.c below 1 PASS0.821
trex01_unsafe.c below 1 OKAY0.46
trex02_safe2.c below 3 PASS0.55
trex02_safe.c below 3 PASS0.555
trex02_unsafe.c below 3 OKAY0.565
trex03_safe.c below 1 PASS0.494
trex03_unsafe.c below 1 OKAY0.5
trex04_safe.c below 1 PASS0.387
while_infinite_loop_1_safe.c below 1 PASS0.341
while_infinite_loop_2_safe.c below 1 PASS0.352
while_infinite_loop_3_safe.c below 1 PASS0.357
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 485.007
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.562
blogger_simplified1.c below 3 PASS1.649
divided_difference2.c below TIMEOUT 300.007
mult-proc.c below 3 PASS0.54
mult-proc-params.c below 3 PASS0.526
popall.c below 1 PASS0.958
simulated_scc.c below 1 PASS0.834
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.076
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.426
degree2_binomial.c below 1 PASS0.899
degree2_monomial.c below 1 PASS0.483
degree3_binomial.c below 1 FAIL4.888
degree3_monomial.c below 1 PASS0.984
degree4_binomial.c below 1 FAIL5.266
degree4_monomial.c below 1 PASS1.663
degree5_binomial.c below 1 FAIL16.346
degree5_monomial.c below 1 PASS3.174
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 34.129
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.508
cubic_with_square_interproc.c below 2 FAIL0.72
cubic_with_square_nonlinear.c below 1 FAIL0.654
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.726
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.673
cubic_with_square_unsafe.c below 1 OKAY0.512
multi-input.c below 1 FAIL10.91
multi-input_unsafe.c below 1 OKAY10.762
nondet_loop_bound.c below 1 FAIL0.573
nondet_loop_bound_quartic.c below 1 FAIL0.768
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.812
nondet_loop_bound_unsafe.c below 1 OKAY0.569
nonlinear_stratified.c below 1 PASS129.294
nonlinear_stratified_unsafe.c below 1 OKAY70.295
quartic_with_cube.c below 1 FAIL0.707
quartic_with_cube_nonlinear.c below 1 FAIL1.019
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY1.036
quartic_with_cube_unsafe.c below 1 OKAY0.568
quintic_with_quartic.c below 1 PASS1.103
quintic_with_quartic_nonlinear.c below 1 PASS1.169
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.201
quintic_with_quartic_unsafe.c below 1 OKAY1.106
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 235.685
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.031
degree2_FD_AllAux_AllAssm.c below 1 PASS107.021
degree2_FD_AllAux_FewAssm.c below 1 PASS7.348
degree2_FD_FewAux_FewAssm.c below 1 PASS1.395
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.377
degree3.c below 1 PASS1.13
degree3_FD.c below 1 PASS1.322
degree4.c below 1 PASS1.979
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 122.603
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.543
loop_unsafe.c below 1 OKAY0.539
simulated_lese_parser.c below 1 PASS0.395
simulated_lese_sentinel.c below 1 PASS0.409
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.886
/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.005
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.005
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.386
array_false-unreach-call2.c below 1 OKAY0.423
array_false-unreach-call3.c below 1 OKAY0.385
array_true-unreach-call1.c below 1 FAIL0.397
array_true-unreach-call2.c below 1 FAIL0.407
array_true-unreach-call3.c below 1 PASS0.39
array_true-unreach-call4.c below 1 FAIL0.382
const_false-unreach-call1.c below 1 OKAY0.408
const_true-unreach-call1.c below 1 PASS0.415
diamond_false-unreach-call1.c below 1 OKAY0.393
diamond_true-unreach-call1.c below 1 PASS0.413
diamond_true-unreach-call2.c below 1 PASS0.409
functions_false-unreach-call1.c below 3 OKAY0.506
functions_true-unreach-call1.c below 3 PASS0.52
multivar_false-unreach-call1.c below 1 OKAY0.396
multivar_true-unreach-call1.c below 1 PASS0.409
nested_false-unreach-call1.c below 1 OKAY0.464
nested_true-unreach-call1.c below 1 PASS0.456
overflow_true-unreach-call1.c below 1 PASS0.344
phases_false-unreach-call1.c below 1 OKAY0.52
phases_false-unreach-call2.c below 1 OKAY0.377
phases_true-unreach-call1.c below 1 PASS0.492
phases_true-unreach-call2.c below 1 PASS0.392
simple_false-unreach-call1.c below 1 OKAY0.39
simple_false-unreach-call2.c below 1 OKAY0.363
simple_false-unreach-call3.c below 1 OKAY0.36
simple_false-unreach-call4.c below 1 OKAY0.378
simple_true-unreach-call1.c below 1 PASS0.362
simple_true-unreach-call2.c below 1 PASS0.355
simple_true-unreach-call3.c below 1 PASS0.36
simple_true-unreach-call4.c below 1 PASS0.377
underapprox_false-unreach-call1.c below 1 OKAY0.413
underapprox_false-unreach-call2.c below 1 OKAY0.414
underapprox_true-unreach-call1.c below 1 FAIL0.404
underapprox_true-unreach-call2.c below 1 PASS0.394
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.254
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.534
apache-get-tag_true-unreach-call.c below 1 FAIL0.606
down_true-unreach-call.c below 1 PASS0.474
fragtest_simple_true-unreach-call.c below 1 PASS0.591
half_2_true-unreach-call.c below 1 PASS0.498
heapsort_true-unreach-call.c below 1 PASS2.279
id_build_true-unreach-call.c below 1 PASS0.435
id_trans_false-unreach-call.c below 1 OKAY0.371
id_trans_true-unreach-call.c below 1 PASS0.399
large_const_true-unreach-call.c below 1 PASS0.506
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.462
nested6_true-unreach-call.c below 1 FAIL0.651
nested9_true-unreach-call.c below 1 PASS0.714
nest-if3_true-unreach-call.c below 1 PASS0.573
NetBSD_loop_true-unreach-call.c below 1 PASS0.387
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.507
seq_true-unreach-call.c below 1 PASS0.553
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.605
string_concat-noarr_true-unreach-call.c below 1 PASS0.497
up_true-unreach-call.c below 1 PASS0.492
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.134
/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.436
cggmp2005b_true-unreach-call.c below 1 PASS0.672
cggmp2005_true-unreach-call.c below 1 PASS0.415
cggmp2005_variant_true-unreach-call.c below 1 PASS0.409
css2003_true-unreach-call.c below 1 PASS1.093
ddlm2013_true-unreach-call.c below 1 PASS0.626
gcnr2008_false-unreach-call.c below 1 OKAY1.115
gj2007b_true-unreach-call.c below 1 FAIL0.445
gj2007_true-unreach-call.c below 1 PASS0.561
gr2006_true-unreach-call.c below 1 PASS0.59
gsv2008_true-unreach-call.c below 1 PASS0.414
hhk2008_true-unreach-call.c below 1 PASS0.391
jm2006_true-unreach-call.c below 1 PASS0.527
jm2006_variant_true-unreach-call.c below 1 PASS0.621
mcmillan2006_true-unreach-call.c below 1 FAIL0.447
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.204
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.374
count_by_1_variant_true-unreach-call.c below 1 PASS0.472
count_by_2_true-unreach-call.c below 1 PASS0.375
count_by_k_true-unreach-call.c below 1 PASS0.377
count_by_nondet_true-unreach-call.c below 1 PASS0.4
gauss_sum_true-unreach-call.c below 1 PASS0.43
half_true-unreach-call.c below 1 FAIL0.419
nested_true-unreach-call.c below 1 PASS0.531
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.378
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.429
array_true-unreach-call.c below 1 FAIL0.447
bubble_sort_false-unreach-call.c below 4 OKAY78.876
bubble_sort_true-unreach-call.c below 1 PASS5.218
compact_false-unreach-call.c below 1 OKAY0.478
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.401
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.391
eureka_01_false-unreach-call.c below 1 OKAY2.668
eureka_01_true-unreach-call.c below 1 FAIL1.58
eureka_05_true-unreach-call.c below 1 FAIL0.866
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.365
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.378
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.366
heavy_false-unreach-call.c below 1 OKAY0.595
heavy_true-unreach-call.c below 1 PASS0.597
insertion_sort_false-unreach-call.c below 1 OKAY1.539
insertion_sort_true-unreach-call.c below 1 FAIL0.634
invert_string_false-unreach-call.c below 1 OKAY0.591
invert_string_true-unreach-call.c below 1 FAIL0.65
linear_sea.ch_true-unreach-call.c below 1 FAIL0.421
linear_search_false-unreach-call.c below 1 OKAY0.445
lu.cmp_true-unreach-call.c below 3 PASS28.289
ludcmp_false-unreach-call.c below 3 OKAY28.293
matrix_false-unreach-call_true-termination.c below 1 OKAY1.377
matrix_true-unreach-call_true-termination.c below 1 FAIL0.525
n.c11_true-unreach-call.c below 3 FAIL0.574
n.c24_false-unreach-call.c below 3 OKAY5.278
n.c40_true-unreach-call.c below 1 FAIL0.397
nec11_false-unreach-call.c below 1 OKAY0.406
nec20_false-unreach-call.c below 1 OKAY0.453
nec40_true-unreach-call.c below 1 FAIL0.406
string_false-unreach-call.c below 1 OKAY0.76
string_true-unreach-call.c below 1 FAIL0.744
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.74
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.395
sum01_false-unreach-call_true-termination.c below 1 OKAY0.599
sum01_true-unreach-call_true-termination.c below 1 PASS0.418
sum03_false-unreach-call_true-termination.c below 1 OKAY0.646
sum03_true-unreach-call_false-termination.c below 1 PASS0.526
sum04_false-unreach-call_true-termination.c below 1 OKAY0.598
sum04_true-unreach-call_true-termination.c below 1 PASS0.394
sum_array_false-unreach-call.c below 1 OKAY0.663
sum_array_true-unreach-call.c below 1 FAIL0.706
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.345
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.622
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.448
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.36
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.378
trex01_false-unreach-call_true-termination.c below 3 OKAY0.629
trex01_true-unreach-call.c below 3 PASS0.933
trex02_false-unreach-call_true-termination.c below 3 OKAY0.556
trex02_true-unreach-call_true-termination.c below 3 PASS0.549
trex03_false-unreach-call_true-termination.c below 3 OKAY0.878
trex03_true-unreach-call.c below 3 PASS0.869
trex04_true-unreach-call_false-termination.c below 1 PASS0.424
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.409
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.253
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.421
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.415
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.31
vogal_false-unreach-call.c below 1 OKAY0.952
vogal_true-unreach-call.c below 1 FAIL0.932
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.345
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.347
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.339
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.354
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 198.553
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.571
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.564
Ackermann03_true-unreach-call.c below 7 FAIL1.599
Ackermann04_true-unreach-call.c below 7 FAIL1.61
Addition01_true-unreach-call_true-termination.c below 2 PASS0.825
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.838
Addition03_false-no-overflow.c below 2 PASS0.833
Addition03_true-unreach-call.c below 2 PASS0.823
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.622
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.563
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.542
Fibonacci01_true-unreach-call.c below TIMEOUT 300.006
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.005
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.006
gcd01_true-unreach-call_true-termination.c below 2 PASS0.727
gcd02_true-unreach-call.c below 2 FAIL1.449
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.305
McCarthy91_true-unreach-call.c below 7 FAIL1.233
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.775
Primes_true-unreach-call.c below 3 FAIL2.278
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.54
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.508
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.506
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.738
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.568
afterrec_2calls_true-unreach-call.c below 2 PASS0.566
afterrec_false-unreach-call.c below 2 OKAY0.459
afterrec_true-unreach-call.c below 2 PASS0.455
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.007
fibo_20_false-unreach-call.c below TIMEOUT 300.004
fibo_20_true-unreach-call.c below TIMEOUT 300.004
fibo_25_false-unreach-call.c below TIMEOUT 300.006
fibo_25_true-unreach-call.c below TIMEOUT 300.004
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.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.005
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.005
fibo_5_false-unreach-call.c below TIMEOUT 300.004
fibo_5_true-unreach-call.c below TIMEOUT 300.006
fibo_7_false-unreach-call.c below TIMEOUT 300.005
fibo_7_true-unreach-call.c below TIMEOUT 300.006
id2_b2_o3_true-unreach-call.c below 2 PASS0.949
id2_b3_o2_false-unreach-call.c below 2 OKAY0.972
id2_b3_o5_true-unreach-call.c below 2 PASS0.963
id2_b5_o10_true-unreach-call.c below 2 PASS0.978
id2_i5_o5_false-unreach-call.c below 2 OKAY0.552
id2_i5_o5_true-unreach-call.c below 2 PASS0.545
id_b2_o3_true-unreach-call.c below 2 PASS0.847
id_b3_o2_false-unreach-call.c below 2 OKAY0.825
id_b3_o5_true-unreach-call.c below 2 PASS0.866
id_b5_o10_true-unreach-call.c below 2 PASS0.858
id_i10_o10_false-unreach-call.c below 2 OKAY0.493
id_i10_o10_true-unreach-call.c below 2 PASS0.513
id_i15_o15_false-unreach-call.c below 2 OKAY0.496
id_i15_o15_true-unreach-call.c below 2 PASS0.503
id_i20_o20_false-unreach-call.c below 2 OKAY0.484
id_i20_o20_true-unreach-call.c below 2 PASS0.502
id_i25_o25_false-unreach-call.c below 2 OKAY0.503
id_i25_o25_true-unreach-call.c below 2 PASS0.5
id_i5_o5_false-unreach-call.c below 2 OKAY0.514
id_i5_o5_true-unreach-call.c below 2 PASS0.505
id_o1000_false-unreach-call.c below 2 OKAY0.5
id_o100_false-unreach-call.c below 2 OKAY0.509
id_o10_false-unreach-call.c below 2 OKAY0.515
id_o200_false-unreach-call.c below 2 OKAY0.498
id_o20_false-unreach-call.c below 2 OKAY0.503
id_o3_false-unreach-call.c below 2 OKAY0.505
sum_10x0_false-unreach-call.c below 2 OKAY0.592
sum_10x0_true-unreach-call.c below 2 PASS0.569
sum_15x0_false-unreach-call.c below 2 OKAY0.563
sum_15x0_true-unreach-call.c below 2 PASS0.56
sum_20x0_false-unreach-call.c below 2 OKAY0.579
sum_20x0_true-unreach-call.c below 2 PASS0.545
sum_25x0_false-unreach-call.c below 2 OKAY0.556
sum_25x0_true-unreach-call.c below 2 PASS0.562
sum_2x3_false-unreach-call.c below 2 OKAY0.552
sum_2x3_true-unreach-call.c below 2 PASS0.547
sum_non_eq_false-unreach-call.c below 2 OKAY0.571
sum_non_eq_true-unreach-call.c below 2 PASS0.559
sum_non_false-unreach-call.c below 2 OKAY0.568
sum_non_true-unreach-call.c below 2 PASS0.559
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.497
/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.55
rec-bhmr2007_true-unreach-call.c below 2 PASS0.573
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.09
rec-cggmp2005_true-unreach-call.c below 2 PASS0.51
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.555
rec-css2003_true-unreach-call.c below 2 PASS1.483
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.125
rec-gj2007b_true-unreach-call.c below 2 FAIL0.513
rec-gj2007_true-unreach-call.c below 2 FAIL0.655
rec-gr2006_true-unreach-call.c below 2 FAIL0.663
rec-gsv2008_true-unreach-call.c below 2 PASS0.527
rec-hhk2008_true-unreach-call.c below 2 PASS0.53
rec-jm2006_true-unreach-call.c below 2 PASS0.636
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.718
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.623
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.755
/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.453
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.558
rec-count_by_2_true-unreach-call.c below 2 PASS0.464
rec-count_by_k_true-unreach-call.c below 2 PASS0.496
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.513
rec-gauss_sum_true-unreach-call.c below 2 PASS0.556
rec-half_true-unreach-call.c below 2 FAIL0.509
rec-nested_true-unreach-call.c below 3 FAIL0.873
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.422
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.615
cubic_polynomial_unsafe.c below 2 OKAY0.618
edit_distance_bottom_up.c below 3 FAIL191.444
edit_distance_top_down.c below 3 FAIL5.141
log_log_n_solution.c below 3 FAIL0.579
log_log_n_solution_unsafe.c below 3 OKAY0.599
log_n_solution.c below 2 FAIL0.596
log_n_solution_unsafe.c below 2 OKAY0.578
multivariate_1.c below TIMEOUT 300.098
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL3.506
multivariate_higher_order_unsafe.c below 7 OKAY3.593
n_cubed_solution.c below EXCEPTION 99.877
n_cubed_solution_unsafe.c below EXCEPTION 0.027
n_log_n_solution.c below 8 FAIL1.648
n_log_n_solution_unsafe.c below 8 OKAY1.647
n_squared_two_base_case_even.c below 2 PASS0.683
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.69
n_squared_two_base_case_odd.c below 2 PASS0.707
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.706
pascals_dynamic.c below 3 FAIL2.779
pascals_dynamic_unsafe.c below 3 OKAY2.628
pascals_iterative.c below 1 FAIL4.977
pascals_iterative_unsafe.c below 1 OKAY4.886
pascals_recursive.c below 8 FAIL3.715
pascals_recursive_unsafe.c below 8 OKAY3.727
squared_solution.c below 8 FAIL3.092
squared_solution_unsafe.c below 8 OKAY3.132
two_n_even.c below 2 PASS0.524
two_n_even_unsafe.c below 2 OKAY0.538
two_n_odd.c below 2 PASS0.544
two_n_odd_unsafe.c below 2 OKAY0.538
two_to_n_over_two_even.c below 7 FAIL127.642
two_to_n_over_two_even_unsafe.c below 7 OKAY284.528
two_to_n_over_two_odd.c below 7 FAIL243.817
two_to_n_over_two_odd_unsafe.c below 7 OKAY148.025
two_to_n_squared.c below 5 FAIL20.69
two_to_n_squared_unsafe.c below 5 OKAY20.297
two_to_two_to_n.c below 7 FAIL1.486
two_to_two_to_n_unsafe.c below 7 OKAY1.449
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1792.371
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.422
adding_and_mult_unsafe.c below 1 OKAY0.415
binary_search_array_tree.c below 1 FAIL0.816
exp_add_linear.c below 1 PASS0.528
exp_add_linear_unsafe.c below 1 OKAY0.537
exp_add_loop_rec.c below 1 FAIL0.405
exp_add_loop_rec_unsafe.c below 1 OKAY0.411
exp_add_loop_variable.c below 1 PASS0.532
exp_add_loop_variable_unsafe.c below 1 OKAY0.494
exp_with_linear_inner_loop.c below 1 FAIL0.626
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.636
halving_log1.c below 1 FAIL0.641
linear_two_to_n.c below 7 FAIL1.768
linear_two_to_n_unsafe.c below 7 OKAY1.76
loop_five_to_n.c below 1 PASS0.484
loop_five_to_n_unsafe.c below 1 OKAY0.468
non_loop_five_to_n.c below 7 FAIL54.908
non_loop_five_to_n_unsafe.c below 7 OKAY54.648
power_log_modified.c below 1 PASS0.669
simple_exponential.c below 1 PASS0.468
simple_exponential_for.c below 1 PASS0.477
simple_exponential_for_unsafe.c below 1 OKAY0.499
simple_exponential_unsafe.c below 1 OKAY0.469
two_to_n_minus_n.c below 7 FAIL2.423
two_to_n_minus_n_loop.c below TIMEOUT 300.005
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.006
two_to_n_minus_n_unsafe.c below 7 OKAY2.379
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 727.894
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.715
02.c below 3 FAIL0.88
03.c below 1 PASS0.529
04.c below 1 PASS0.396
05.c below 3 PASS1.291
06.c below 3 FAIL10.159
07.c below 3 PASS0.716
08.c below 3 PASS1.57
09.c below 3 PASS1.069
10.c below 3 FAIL1.252
11.c below 1 PASS0.399
12.c below 3 PASS1.642
13.c below 3 PASS0.677
14.c below 3 PASS0.59
15.c below 1 PASS0.375
16.c below 1 PASS0.552
17.c below 1 PASS3.45
18.c below 1 PASS0.483
19.c below 1 PASS0.569
20.c below 3 FAIL0.794
21.c below 3 PASS0.692
22.c below 3 FAIL0.886
23.c below 1 PASS0.422
24.c below 1 PASS0.493
25.c below 3 FAIL1.667
26.c below TIMEOUT 300.004
27.c below 1 PASS0.541
28.c below 3 PASS0.692
29.c below 3 PASS1.173
30.c below 1 PASS0.409
31.c below 3 PASS1.365
32.c below 1 FAIL0.438
33.c below 3 PASS1.41
34.c below 1 FAIL0.442
35.c below 1 PASS0.362
36.c below 3 PASS2.938
37.c below 3 FAIL0.633
38.c below 1 FAIL0.45
39.c below 3 PASS0.545
40.c below 3 PASS0.958
41.c below 1 PASS0.429
42.c below 3 PASS0.988
43.c below 3 PASS0.645
44.c below 1 PASS0.4
45.c below 3 FAIL2.92
46.c below 3 FAIL1.968
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 351.978
/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.482
AGHKTW2017_loginSafe.c below 1 PASS0.996
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.592
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.569
BCK2011_gauss.c below 1 PASS0.524
BCK2011_strength_reduction.c below 1 PASS0.844
BCK2011_strength_reduction_linear.c below 1 PASS0.523
fibonacci_information_flow.c below 1 PASS0.675
loop_splitting_test_safe.c below 1 PASS0.713
TA2005_fib2.c below 1 PASS0.688
TA2005_fib.c below 1 PASS0.545
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.629
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.868
c3_cleanup_better.c below 3 PASS1.725
c3_cleanup.c below 3 PASS1.672
c3_intermediate.c below 3 PASS1.689
c3_noinv.c below 3 FAIL1.479
doublers.c below 1 FAIL0.66
doublers_easier.c below 3 FAIL1.269
doublers_easy.c below 1 FAIL0.726
exp_mult.c below 1 FAIL0.42
fig1_rotation_unsafe.c below 1 OKAY0.477
guessing_game.c below 3 FAIL0.602
not_P_solvable.c below 1 PASS0.372
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 11.959
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.432
maxequals_linear_1.c below 1 PASS0.628
maxequals_linear_2.c below 1 PASS0.647
maxequals_linear_3.c below 1 FAIL0.417
maxequals_linear_4.c below 1 PASS0.413
maxequals_linear_5.c below 1 PASS0.41
maxequals_linear_6.c below 1 FAIL0.421
maxequals_matrix1.c below 3 FAIL1.596
maxequals_matrix2.c below 3 FAIL1.592
maxequals_quadratic1.c below 1 FAIL0.433
maxequals_quadratic2.c below 1 PASS0.409
maxequals_stratified1.c below 3 PASS4.888
maxequals_stratified2.c below 3 PASS5.144
maxequals_stratified3.c below 3 FAIL5.279
nine.c below 1 FAIL0.424
nine_nondecreasing.c below 1 PASS0.682
sum_interval_1.c below 1 FAIL0.506
sum_interval_2.c below 1 FAIL0.487
sum_interval_3.c below 1 FAIL0.527
TrackingObjectFields.c below 3 PASS10.941
TrackingObjectFields_inlined.c below 1 PASS3.137
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 39.413
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.496
bobble2_varloop.c below 1 PASS0.486
bobble3.c below TIMEOUT 300.004
bobble4.c below 1 FAIL0.46
bobble5.c below 1 FAIL0.478
bobble.c below 1 PASS0.458
inchworm2.c below 1 TIMEOUT300.004
inchworm3.c below 1 PASS0.512
inchworm4.c below 1 PASS0.484
inchworm5.c below 1 PASS0.469
inchworm6_unsafe.c below 1 OKAY0.467
inchworm.c below 1 FAIL0.461
leapdiff2.c below 1 TIMEOUT300.006
leapfrog_annotated.c below 1 FAIL0.47
leapfrog_annotated_disjunction.c below 1 PASS0.48
leapfrog_asymmetric2.c below 1 FAIL0.532
leapfrog_asymmetric3.c below 1 FAIL0.537
leapfrog_asymmetric.c below 1 FAIL0.49
leapfrog.c below 1 FAIL0.446
leapfrog_materialized.c below 1 FAIL0.466
leapfrog_verbose.c below 1 FAIL0.482
leapspin.c below 1 FAIL0.415
leapsum2.c below 1 TIMEOUT300.004
leapthree.c below 1 FAIL0.489
microbobble2.c below 1 PASS0.438
microbobble3.c below 1 PASS0.435
microbobble_asymmetric.c below 1 PASS0.434
microbobble.c below 1 FAIL0.432
simple_bl2.c below 1 FAIL0.473
simple_bl3.c below 1 FAIL0.411
simple_bl.c below 1 FAIL0.476
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1212.695
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.37
binval_example_2_unsafe.c below 1 OKAY0.35
binval_example_3_unsafe.c below 1 OKAY0.336
binval_example_4.c below 1 PASS0.429
binval_example_4_unsafe.c below 1 OKAY0.401
binval_example_5.c below 1 FAIL1.623
binval_example_5_unsafe.c below 1 OKAY3.779
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.288