[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.422
kmp.c below 1 PASS1.399
qsort.c below 4 PASS1.326
speed_pldi09_fig1.c below 1 PASS0.682
speed_pldi09_fig4_2.c below 1 FAIL0.441
speed_pldi09_fig4_4.c below 1 PASS0.601
speed_pldi09_fig4_5.c below 1 PASS0.498
speed_pldi10_ex1.c below 1 PASS1.69
speed_pldi10_ex3.c below 1 PASS0.692
speed_pldi10_ex4.c below 1 PASS0.752
speed_popl10_fig2_1.c below 1 PASS0.652
speed_popl10_fig2_2.c below 1 FAIL0.429
speed_popl10_nested_multiple.c below 1 PASS0.604
speed_popl10_nested_single.c below 1 PASS0.526
speed_popl10_sequential_single.c below 1 PASS0.499
speed_popl10_simple_multiple.c below 1 PASS0.743
speed_popl10_simple_single_2.c below 1 PASS0.917
speed_popl10_simple_single.c below 1 PASS0.41
t07.c below 1 PASS0.561
t08.c below 1 PASS0.493
t09.c below 1 PASS0.457
t10.c below 1 PASS0.447
t11.c below 1 PASS0.633
t13.c below 1 FAIL0.53
t15.c below 1 PASS0.541
t16.c below 1 PASS0.476
t19.c below 1 PASS0.505
t20.c below 1 PASS0.476
t27.c below 1 PASS0.771
t28.c below 1 PASS0.728
t30.c below 1 FAIL0.487
t37.c below 2 PASS0.942
t39.c below 2 PASS0.789
t46.c below 1 PASS0.528
t47.c below 1 PASS0.684
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.331
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.505
qsort_full.c below 4 PASS12.231
rec1-param_safe.c below 2 PASS0.553
rec1-param_unsafe.c below 2 OKAY0.533
rec1_safe.c below 2 PASS0.489
rec1_unsafe.c below 2 OKAY0.476
rec2-param_safe.c below 2 PASS0.488
rec2-param_unsafe.c below 2 OKAY0.476
rec2_safe.c below 2 PASS0.467
rec2_unsafe.c below 2 OKAY0.482
rec-test.c below 2 PASS0.474
sas03_bothbranches.c below 7 PASS1.219
sas03.c below 2 PASS0.908
simulated_lese_recursive.c below 2 PASS0.656
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.957
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.401
count_up_down_unsafe.c below 1 OKAY0.414
divide.c below 1 PASS0.409
factor_unsafe.c below 1 OKAY0.372
for_infinite_loop_1_safe.c below 1 PASS0.353
for_infinite_loop_2_safe.c below 1 PASS0.354
interproc.c below 1 PASS0.331
mult.c below 1 PASS0.384
pointer_arith.c below 1 PASS0.335
quotient.c below 3 PASS0.742
subtract.c below 1 PASS0.386
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.408
sum01_bug02_unsafe.c below 1 OKAY0.732
sum01_real_safe.c below 1 PASS0.395
sum01_safe.c below 1 PASS0.411
sum01_unsafe.c below 1 OKAY0.586
sum02_safe.c below 1 PASS0.441
sum03_safe.c below 1 PASS0.481
sum03_unsafe.c below 1 OKAY0.591
sum04_safe.c below 1 PASS0.413
sum04_unsafe.c below 1 OKAY0.598
terminator_02_safe.c below 1 PASS0.366
terminator_02_unsafe.c below 1 OKAY0.424
terminator_03_safe.c below 1 PASS0.368
terminator_03_unsafe.c below 1 OKAY0.373
token_ring01_safe.c below 4 FAIL126.929
token_ring01_unsafe.c below 4 OKAY211.272
toy_safe.c below EXCEPTION 132.867
trex01_safe.c below 1 PASS0.805
trex01_unsafe.c below 1 OKAY0.452
trex02_safe2.c below 3 PASS0.534
trex02_safe.c below 3 PASS0.533
trex02_unsafe.c below 3 OKAY0.551
trex03_safe.c below 1 PASS0.523
trex03_unsafe.c below 1 OKAY0.508
trex04_safe.c below 1 PASS0.396
while_infinite_loop_1_safe.c below 1 PASS0.33
while_infinite_loop_2_safe.c below 1 PASS0.353
while_infinite_loop_3_safe.c below 1 PASS0.338
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 487.459
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.55
blogger_simplified1.c below 3 PASS1.682
divided_difference2.c below TIMEOUT 300.01
mult-proc.c below 3 PASS0.531
mult-proc-params.c below 3 PASS0.534
popall.c below 1 PASS0.97
simulated_scc.c below 1 PASS0.845
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.122
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.411
degree2_binomial.c below 1 PASS0.922
degree2_monomial.c below 1 PASS0.486
degree3_binomial.c below 1 FAIL5.001
degree3_monomial.c below 1 PASS1.016
degree4_binomial.c below 1 FAIL5.174
degree4_monomial.c below 1 PASS1.718
degree5_binomial.c below 1 FAIL16.546
degree5_monomial.c below 1 PASS3.273
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 34.547
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.538
cubic_with_square_interproc.c below 2 FAIL0.737
cubic_with_square_nonlinear.c below 1 FAIL0.662
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.723
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.662
cubic_with_square_unsafe.c below 1 OKAY0.507
multi-input.c below 1 FAIL11.161
multi-input_unsafe.c below 1 OKAY10.703
nondet_loop_bound.c below 1 FAIL0.586
nondet_loop_bound_quartic.c below 1 FAIL0.763
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.815
nondet_loop_bound_unsafe.c below 1 OKAY0.578
nonlinear_stratified.c below 1 PASS128.173
nonlinear_stratified_unsafe.c below 1 OKAY72.593
quartic_with_cube.c below 1 FAIL0.716
quartic_with_cube_nonlinear.c below 1 FAIL1.057
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY1.047
quartic_with_cube_unsafe.c below 1 OKAY0.57
quintic_with_quartic.c below 1 PASS1.126
quintic_with_quartic_nonlinear.c below 1 PASS1.196
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.184
quintic_with_quartic_unsafe.c below 1 OKAY1.147
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 237.244
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.018
degree2_FD_AllAux_AllAssm.c below 1 PASS112.294
degree2_FD_AllAux_FewAssm.c below 1 PASS7.424
degree2_FD_FewAux_FewAssm.c below 1 PASS1.398
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.412
degree3.c below 1 PASS1.229
degree3_FD.c below 1 PASS1.394
degree4.c below 1 PASS2.009
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 128.178
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.53
loop_unsafe.c below 1 OKAY0.532
simulated_lese_parser.c below 1 PASS0.412
simulated_lese_sentinel.c below 1 PASS0.418
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.892
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.425
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.425
/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.384
array_false-unreach-call2.c below 1 OKAY0.42
array_false-unreach-call3.c below 1 OKAY0.406
array_true-unreach-call1.c below 1 FAIL0.407
array_true-unreach-call2.c below 1 FAIL0.41
array_true-unreach-call3.c below 1 PASS0.391
array_true-unreach-call4.c below 1 FAIL0.386
const_false-unreach-call1.c below 1 OKAY0.41
const_true-unreach-call1.c below 1 PASS0.39
diamond_false-unreach-call1.c below 1 OKAY0.387
diamond_true-unreach-call1.c below 1 PASS0.406
diamond_true-unreach-call2.c below 1 PASS0.414
functions_false-unreach-call1.c below 3 OKAY0.513
functions_true-unreach-call1.c below 3 PASS0.516
multivar_false-unreach-call1.c below 1 OKAY0.407
multivar_true-unreach-call1.c below 1 PASS0.397
nested_false-unreach-call1.c below 1 OKAY0.471
nested_true-unreach-call1.c below 1 PASS0.444
overflow_true-unreach-call1.c below 1 PASS0.361
phases_false-unreach-call1.c below 1 OKAY0.48
phases_false-unreach-call2.c below 1 OKAY0.402
phases_true-unreach-call1.c below 1 PASS0.507
phases_true-unreach-call2.c below 1 PASS0.391
simple_false-unreach-call1.c below 1 OKAY0.369
simple_false-unreach-call2.c below 1 OKAY0.366
simple_false-unreach-call3.c below 1 OKAY0.36
simple_false-unreach-call4.c below 1 OKAY0.402
simple_true-unreach-call1.c below 1 PASS0.376
simple_true-unreach-call2.c below 1 PASS0.365
simple_true-unreach-call3.c below 1 PASS0.36
simple_true-unreach-call4.c below 1 PASS0.374
underapprox_false-unreach-call1.c below 1 OKAY0.419
underapprox_false-unreach-call2.c below 1 OKAY0.412
underapprox_true-unreach-call1.c below 1 FAIL0.409
underapprox_true-unreach-call2.c below 1 PASS0.396
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.308
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.61
apache-get-tag_true-unreach-call.c below 1 FAIL0.616
down_true-unreach-call.c below 1 PASS0.467
fragtest_simple_true-unreach-call.c below 1 PASS0.606
half_2_true-unreach-call.c below 1 PASS0.489
heapsort_true-unreach-call.c below 1 PASS2.375
id_build_true-unreach-call.c below 1 PASS0.428
id_trans_false-unreach-call.c below 1 OKAY0.38
id_trans_true-unreach-call.c below 1 PASS0.382
large_const_true-unreach-call.c below 1 PASS0.532
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.465
nested6_true-unreach-call.c below 1 FAIL0.639
nested9_true-unreach-call.c below 1 PASS0.745
nest-if3_true-unreach-call.c below 1 PASS0.585
NetBSD_loop_true-unreach-call.c below 1 PASS0.402
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.481
seq_true-unreach-call.c below 1 PASS0.564
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.62
string_concat-noarr_true-unreach-call.c below 1 PASS0.504
up_true-unreach-call.c below 1 PASS0.473
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.363
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.439
bhmr2007_true-unreach-call.c below 1 PASS0.457
cggmp2005b_true-unreach-call.c below 1 PASS0.649
cggmp2005_true-unreach-call.c below 1 PASS0.419
cggmp2005_variant_true-unreach-call.c below 1 PASS0.429
css2003_true-unreach-call.c below 1 PASS1.113
ddlm2013_true-unreach-call.c below 1 PASS0.636
gcnr2008_false-unreach-call.c below 1 OKAY1.153
gj2007b_true-unreach-call.c below 1 FAIL0.445
gj2007_true-unreach-call.c below 1 PASS0.58
gr2006_true-unreach-call.c below 1 PASS0.565
gsv2008_true-unreach-call.c below 1 PASS0.397
hhk2008_true-unreach-call.c below 1 PASS0.415
jm2006_true-unreach-call.c below 1 PASS0.56
jm2006_variant_true-unreach-call.c below 1 PASS0.653
mcmillan2006_true-unreach-call.c below 1 FAIL0.473
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.383
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.382
count_by_1_variant_true-unreach-call.c below 1 PASS0.495
count_by_2_true-unreach-call.c below 1 PASS0.394
count_by_k_true-unreach-call.c below 1 PASS0.375
count_by_nondet_true-unreach-call.c below 1 PASS0.406
gauss_sum_true-unreach-call.c below 1 PASS0.428
half_true-unreach-call.c below 1 FAIL0.439
nested_true-unreach-call.c below 1 PASS0.538
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.457
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.431
array_true-unreach-call.c below 1 FAIL0.486
bubble_sort_false-unreach-call.c below 4 OKAY81.253
bubble_sort_true-unreach-call.c below 1 PASS5.363
compact_false-unreach-call.c below 1 OKAY0.469
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.398
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.428
eureka_01_false-unreach-call.c below 1 OKAY2.907
eureka_01_true-unreach-call.c below 1 FAIL1.632
eureka_05_true-unreach-call.c below 1 FAIL0.892
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.396
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.383
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.356
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.367
heavy_false-unreach-call.c below 1 OKAY0.609
heavy_true-unreach-call.c below 1 PASS0.584
insertion_sort_false-unreach-call.c below 1 OKAY1.57
insertion_sort_true-unreach-call.c below 1 FAIL0.654
invert_string_false-unreach-call.c below 1 OKAY0.598
invert_string_true-unreach-call.c below 1 FAIL0.625
linear_sea.ch_true-unreach-call.c below 1 FAIL0.446
linear_search_false-unreach-call.c below 1 OKAY0.475
lu.cmp_true-unreach-call.c below 3 PASS28.287
ludcmp_false-unreach-call.c below 3 OKAY28.258
matrix_false-unreach-call_true-termination.c below 1 OKAY1.403
matrix_true-unreach-call_true-termination.c below 1 FAIL0.537
n.c11_true-unreach-call.c below 3 FAIL0.577
n.c24_false-unreach-call.c below 3 OKAY5.426
n.c40_true-unreach-call.c below 1 FAIL0.394
nec11_false-unreach-call.c below 1 OKAY0.404
nec20_false-unreach-call.c below 1 OKAY0.454
nec40_true-unreach-call.c below 1 FAIL0.414
string_false-unreach-call.c below 1 OKAY0.78
string_true-unreach-call.c below 1 FAIL0.774
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.726
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.398
sum01_false-unreach-call_true-termination.c below 1 OKAY0.606
sum01_true-unreach-call_true-termination.c below 1 PASS0.407
sum03_false-unreach-call_true-termination.c below 1 OKAY0.643
sum03_true-unreach-call_false-termination.c below 1 PASS0.52
sum04_false-unreach-call_true-termination.c below 1 OKAY0.588
sum04_true-unreach-call_true-termination.c below 1 PASS0.413
sum_array_false-unreach-call.c below 1 OKAY0.668
sum_array_true-unreach-call.c below 1 FAIL0.725
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.353
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.614
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.434
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.373
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.386
trex01_false-unreach-call_true-termination.c below 3 OKAY0.631
trex01_true-unreach-call.c below 3 PASS0.982
trex02_false-unreach-call_true-termination.c below 3 OKAY0.574
trex02_true-unreach-call_true-termination.c below 3 PASS0.544
trex03_false-unreach-call_true-termination.c below 3 OKAY0.899
trex03_true-unreach-call.c below 3 PASS0.889
trex04_true-unreach-call_false-termination.c below 1 PASS0.428
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.405
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.412
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.431
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.415
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.371
vogal_false-unreach-call.c below 1 OKAY0.994
vogal_true-unreach-call.c below 1 FAIL0.94
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.34
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.333
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.364
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.333
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 202.169
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.629
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.615
Ackermann03_true-unreach-call.c below 7 FAIL1.66
Ackermann04_true-unreach-call.c below 7 FAIL1.613
Addition01_true-unreach-call_true-termination.c below 2 PASS0.858
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.833
Addition03_false-no-overflow.c below 2 PASS0.836
Addition03_true-unreach-call.c below 2 PASS0.832
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.611
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.578
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.574
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.004
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.007
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.004
gcd01_true-unreach-call_true-termination.c below 2 PASS0.775
gcd02_true-unreach-call.c below 2 FAIL1.426
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.258
McCarthy91_true-unreach-call.c below 7 FAIL1.296
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.786
Primes_true-unreach-call.c below 3 FAIL2.247
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.628
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.513
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.525
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1524.12
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.564
afterrec_2calls_true-unreach-call.c below 2 PASS0.55
afterrec_false-unreach-call.c below 2 OKAY0.486
afterrec_true-unreach-call.c below 2 PASS0.467
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.006
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.018
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.017
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.006
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.006
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.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.006
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.006
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.006
fibo_7_true-unreach-call.c below TIMEOUT 300.006
id2_b2_o3_true-unreach-call.c below 2 PASS1.017
id2_b3_o2_false-unreach-call.c below 2 OKAY1.018
id2_b3_o5_true-unreach-call.c below 2 PASS0.986
id2_b5_o10_true-unreach-call.c below 2 PASS0.966
id2_i5_o5_false-unreach-call.c below 2 OKAY0.578
id2_i5_o5_true-unreach-call.c below 2 PASS0.563
id_b2_o3_true-unreach-call.c below 2 PASS0.858
id_b3_o2_false-unreach-call.c below 2 OKAY0.83
id_b3_o5_true-unreach-call.c below 2 PASS0.829
id_b5_o10_true-unreach-call.c below 2 PASS0.84
id_i10_o10_false-unreach-call.c below 2 OKAY0.517
id_i10_o10_true-unreach-call.c below 2 PASS0.521
id_i15_o15_false-unreach-call.c below 2 OKAY0.522
id_i15_o15_true-unreach-call.c below 2 PASS0.526
id_i20_o20_false-unreach-call.c below 2 OKAY0.504
id_i20_o20_true-unreach-call.c below 2 PASS0.519
id_i25_o25_false-unreach-call.c below 2 OKAY0.52
id_i25_o25_true-unreach-call.c below 2 PASS0.512
id_i5_o5_false-unreach-call.c below 2 OKAY0.522
id_i5_o5_true-unreach-call.c below 2 PASS0.517
id_o1000_false-unreach-call.c below 2 OKAY0.544
id_o100_false-unreach-call.c below 2 OKAY0.554
id_o10_false-unreach-call.c below 2 OKAY0.571
id_o200_false-unreach-call.c below 2 OKAY0.52
id_o20_false-unreach-call.c below 2 OKAY0.54
id_o3_false-unreach-call.c below 2 OKAY0.566
sum_10x0_false-unreach-call.c below 2 OKAY0.644
sum_10x0_true-unreach-call.c below 2 PASS0.597
sum_15x0_false-unreach-call.c below 2 OKAY0.569
sum_15x0_true-unreach-call.c below 2 PASS0.584
sum_20x0_false-unreach-call.c below 2 OKAY0.578
sum_20x0_true-unreach-call.c below 2 PASS0.582
sum_25x0_false-unreach-call.c below 2 OKAY0.587
sum_25x0_true-unreach-call.c below 2 PASS0.58
sum_2x3_false-unreach-call.c below 2 OKAY0.575
sum_2x3_true-unreach-call.c below 2 PASS0.578
sum_non_eq_false-unreach-call.c below 2 OKAY0.568
sum_non_eq_true-unreach-call.c below 2 PASS0.587
sum_non_false-unreach-call.c below 2 OKAY0.592
sum_non_true-unreach-call.c below 2 PASS0.575
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9027.405
/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.599
rec-bhmr2007_true-unreach-call.c below 2 PASS0.627
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.149
rec-cggmp2005_true-unreach-call.c below 2 PASS0.54
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.581
rec-css2003_true-unreach-call.c below 2 PASS1.526
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.181
rec-gj2007b_true-unreach-call.c below 2 FAIL0.52
rec-gj2007_true-unreach-call.c below 2 FAIL0.694
rec-gr2006_true-unreach-call.c below 2 FAIL0.706
rec-gsv2008_true-unreach-call.c below 2 PASS0.557
rec-hhk2008_true-unreach-call.c below 2 PASS0.524
rec-jm2006_true-unreach-call.c below 2 PASS0.663
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.778
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.65
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 311.299
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c below 2 PASS0.483
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.585
rec-count_by_2_true-unreach-call.c below 2 PASS0.474
rec-count_by_k_true-unreach-call.c below 2 PASS0.495
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.548
rec-gauss_sum_true-unreach-call.c below 2 PASS0.594
rec-half_true-unreach-call.c below 2 FAIL0.629
rec-nested_true-unreach-call.c below 3 FAIL1.295
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 5.103
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.922
cubic_polynomial_unsafe.c below 2 OKAY0.646
edit_distance_bottom_up.c below 3 FAIL195.124
edit_distance_top_down.c below 3 FAIL5.442
log_log_n_solution.c below 3 FAIL0.617
log_log_n_solution_unsafe.c below 3 OKAY0.611
log_n_solution.c below 2 FAIL0.592
log_n_solution_unsafe.c below 2 OKAY0.627
multivariate_1.c below TIMEOUT 300.1
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL3.573
multivariate_higher_order_unsafe.c below 7 OKAY3.787
n_cubed_solution.c below EXCEPTION 106.647
n_cubed_solution_unsafe.c below EXCEPTION 0.03
n_log_n_solution.c below 8 FAIL1.753
n_log_n_solution_unsafe.c below 8 OKAY1.679
n_squared_two_base_case_even.c below 2 PASS0.699
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.731
n_squared_two_base_case_odd.c below 2 PASS0.753
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.735
pascals_dynamic.c below 3 FAIL2.821
pascals_dynamic_unsafe.c below 3 OKAY2.882
pascals_iterative.c below 1 FAIL5.089
pascals_iterative_unsafe.c below 1 OKAY5.129
pascals_recursive.c below 8 FAIL3.873
pascals_recursive_unsafe.c below 8 OKAY3.821
squared_solution.c below 8 FAIL3.277
squared_solution_unsafe.c below 8 OKAY3.333
two_n_even.c below 2 PASS0.558
two_n_even_unsafe.c below 2 OKAY0.523
two_n_odd.c below 2 PASS0.551
two_n_odd_unsafe.c below 2 OKAY0.534
two_to_n_over_two_even.c below 7 FAIL137.732
two_to_n_over_two_even_unsafe.c below 7 OKAY142.668
two_to_n_over_two_odd.c below 7 FAIL258.926
two_to_n_over_two_odd_unsafe.c below 7 OKAY144.453
two_to_n_squared.c below 5 FAIL21.754
two_to_n_squared_unsafe.c below 5 OKAY21.177
two_to_two_to_n.c below 7 FAIL1.571
two_to_two_to_n_unsafe.c below 7 OKAY1.54
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1687.286
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.44
adding_and_mult_unsafe.c below 1 OKAY0.431
binary_search_array_tree.c below 1 FAIL0.831
exp_add_linear.c below 1 PASS0.543
exp_add_linear_unsafe.c below 1 OKAY0.539
exp_add_loop_rec.c below 1 FAIL0.424
exp_add_loop_rec_unsafe.c below 1 OKAY0.435
exp_add_loop_variable.c below 1 PASS0.51
exp_add_loop_variable_unsafe.c below 1 OKAY0.508
exp_with_linear_inner_loop.c below 1 FAIL0.636
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.627
halving_log1.c below 1 FAIL0.654
linear_two_to_n.c below 7 FAIL1.818
linear_two_to_n_unsafe.c below 7 OKAY1.786
loop_five_to_n.c below 1 PASS0.468
loop_five_to_n_unsafe.c below 1 OKAY0.455
non_loop_five_to_n.c below 7 FAIL56.872
non_loop_five_to_n_unsafe.c below 7 OKAY56.61
power_log_modified.c below 1 PASS0.696
simple_exponential.c below 1 PASS0.473
simple_exponential_for.c below 1 PASS0.478
simple_exponential_for_unsafe.c below 1 OKAY0.518
simple_exponential_unsafe.c below 1 OKAY0.487
two_to_n_minus_n.c below 7 FAIL2.498
two_to_n_minus_n_loop.c below TIMEOUT 300.007
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.007
two_to_n_minus_n_unsafe.c below 7 OKAY2.49
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 732.241
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.746
02.c below 3 FAIL0.976
03.c below 1 PASS0.524
04.c below 1 PASS0.4
05.c below 3 PASS1.362
06.c below 3 FAIL10.697
07.c below 3 PASS0.719
08.c below 3 PASS1.595
09.c below 3 PASS1.111
10.c below 3 FAIL1.286
11.c below 1 PASS0.425
12.c below 3 PASS1.727
13.c below 3 PASS0.725
14.c below 3 PASS0.622
15.c below 1 PASS0.39
16.c below 1 PASS0.561
17.c below 1 PASS3.728
18.c below 1 PASS0.514
19.c below 1 PASS0.64
20.c below 3 FAIL0.915
21.c below 3 PASS0.769
22.c below 3 FAIL0.988
23.c below 1 PASS0.451
24.c below 1 PASS0.494
25.c below 3 FAIL1.719
26.c below TIMEOUT 300.004
27.c below 1 PASS0.516
28.c below 3 PASS0.685
29.c below 3 PASS1.231
30.c below 1 PASS0.423
31.c below 3 PASS1.347
32.c below 1 FAIL0.44
33.c below 3 PASS1.462
34.c below 1 FAIL0.474
35.c below 1 PASS0.362
36.c below 3 PASS3.047
37.c below 3 FAIL0.666
38.c below 1 FAIL0.449
39.c below 3 PASS0.578
40.c below 3 PASS1.001
41.c below 1 PASS0.446
42.c below 3 PASS1.022
43.c below 3 PASS0.683
44.c below 1 PASS0.434
45.c below 3 FAIL3.068
46.c below 3 FAIL2.161
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 354.583
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.504
AGHKTW2017_foo.c below 1 PASS0.498
AGHKTW2017_loginSafe.c below 1 PASS1.055
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.574
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.578
BCK2011_gauss.c below 1 PASS0.528
BCK2011_strength_reduction.c below 1 PASS0.876
BCK2011_strength_reduction_linear.c below 1 PASS0.539
fibonacci_information_flow.c below 1 PASS0.682
loop_splitting_test_safe.c below 1 PASS0.723
TA2005_fib2.c below 1 PASS0.721
TA2005_fib.c below 1 PASS0.564
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.842
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.848
c3_cleanup_better.c below 3 PASS1.754
c3_cleanup.c below 3 PASS1.729
c3_intermediate.c below 3 PASS1.825
c3_noinv.c below 3 FAIL1.541
doublers.c below 1 FAIL0.714
doublers_easier.c below 3 FAIL1.379
doublers_easy.c below 1 FAIL0.751
exp_mult.c below 1 FAIL0.43
fig1_rotation_unsafe.c below 1 OKAY0.47
guessing_game.c below 3 FAIL0.62
not_P_solvable.c below 1 PASS0.392
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 12.453
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.448
maxequals_linear_1.c below 1 PASS0.655
maxequals_linear_2.c below 1 PASS0.724
maxequals_linear_3.c below 1 FAIL0.435
maxequals_linear_4.c below 1 PASS0.433
maxequals_linear_5.c below 1 PASS0.44
maxequals_linear_6.c below 1 FAIL0.457
maxequals_matrix1.c below 3 FAIL1.784
maxequals_matrix2.c below 3 FAIL1.693
maxequals_quadratic1.c below 1 FAIL0.432
maxequals_quadratic2.c below 1 PASS0.433
maxequals_stratified1.c below 3 PASS5.128
maxequals_stratified2.c below 3 PASS5.477
maxequals_stratified3.c below 3 FAIL5.566
nine.c below 1 FAIL0.443
nine_nondecreasing.c below 1 PASS0.686
sum_interval_1.c below 1 FAIL0.54
sum_interval_2.c below 1 FAIL0.491
sum_interval_3.c below 1 FAIL0.538
TrackingObjectFields.c below 3 PASS11.648
TrackingObjectFields_inlined.c below 1 PASS3.35
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 41.801
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.516
bobble2_varloop.c below 1 PASS0.498
bobble3.c below TIMEOUT 300.005
bobble4.c below 1 FAIL0.476
bobble5.c below 1 FAIL0.487
bobble.c below 1 PASS0.457
inchworm2.c below 1 TIMEOUT300.005
inchworm3.c below 1 PASS0.527
inchworm4.c below 1 PASS0.506
inchworm5.c below 1 PASS0.52
inchworm6_unsafe.c below 1 OKAY0.501
inchworm.c below 1 FAIL0.483
leapdiff2.c below 1 TIMEOUT300.006
leapfrog_annotated.c below 1 FAIL0.489
leapfrog_annotated_disjunction.c below 1 PASS0.485
leapfrog_asymmetric2.c below 1 FAIL0.563
leapfrog_asymmetric3.c below 1 FAIL0.563
leapfrog_asymmetric.c below 1 FAIL0.488
leapfrog.c below 1 FAIL0.438
leapfrog_materialized.c below 1 FAIL0.487
leapfrog_verbose.c below 1 FAIL0.486
leapspin.c below 1 FAIL0.414
leapsum2.c below 1 TIMEOUT300.005
leapthree.c below 1 FAIL0.486
microbobble2.c below 1 PASS0.457
microbobble3.c below 1 PASS0.438
microbobble_asymmetric.c below 1 PASS0.453
microbobble.c below 1 FAIL0.43
simple_bl2.c below 1 FAIL0.479
simple_bl3.c below 1 FAIL0.415
simple_bl.c below 1 FAIL0.502
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1213.065
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.346
binval_example_2_unsafe.c below 1 OKAY0.362
binval_example_3_unsafe.c below 1 OKAY0.349
binval_example_4.c below 1 PASS0.439
binval_example_4_unsafe.c below 1 OKAY0.415
binval_example_5.c below 1 FAIL1.611
binval_example_5_unsafe.c below 1 OKAY3.843
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.365