[Version Information]
WALi-OpenNWA version: f73a8d6dbe21a2004e864fa68f50e0f3de181d25 (2017-12-06 13:06:14 -0600) "Adding guessing_game.c benchmark"
duet version: f185e6421ae9790ed06b5cde5f446a44a8a544d9 (2017-12-06 21:48:54 -0500) "Merge branch 'Newton-ark2' of https://github.com/zkincaid/duet into Newton-ark2"
# 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.405
kmp.c below 1 PASS1.374
qsort.c below 4 PASS1.354
speed_pldi09_fig1.c below 1 PASS0.7
speed_pldi09_fig4_2.c below 1 FAIL0.462
speed_pldi09_fig4_4.c below 1 PASS0.603
speed_pldi09_fig4_5.c below 1 PASS0.494
speed_pldi10_ex1.c below 1 PASS1.693
speed_pldi10_ex3.c below 1 PASS0.72
speed_pldi10_ex4.c below 1 PASS0.777
speed_popl10_fig2_1.c below 1 PASS0.637
speed_popl10_fig2_2.c below 1 FAIL0.436
speed_popl10_nested_multiple.c below 1 PASS0.57
speed_popl10_nested_single.c below 1 PASS0.547
speed_popl10_sequential_single.c below 1 PASS0.494
speed_popl10_simple_multiple.c below 1 PASS0.726
speed_popl10_simple_single_2.c below 1 PASS0.924
speed_popl10_simple_single.c below 1 PASS0.399
t07.c below 1 PASS0.572
t08.c below 1 PASS0.5
t09.c below 1 PASS0.464
t10.c below 1 PASS0.434
t11.c below 1 PASS0.622
t13.c below 1 FAIL0.541
t15.c below 1 PASS0.518
t16.c below 1 PASS0.494
t19.c below 1 PASS0.517
t20.c below 1 PASS0.465
t27.c below 1 PASS0.779
t28.c below 1 PASS0.718
t30.c below 1 FAIL0.473
t37.c below 2 PASS0.903
t39.c below 2 PASS0.789
t46.c below 1 PASS0.52
t47.c below 1 PASS0.706
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.33
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.51
qsort_full.c below 4 PASS11.849
rec1-param_safe.c below 2 PASS0.513
rec1-param_unsafe.c below 2 OKAY0.519
rec1_safe.c below 2 PASS0.499
rec1_unsafe.c below 2 OKAY0.46
rec2-param_safe.c below 2 PASS0.492
rec2-param_unsafe.c below 2 OKAY0.467
rec2_safe.c below 2 PASS0.48
rec2_unsafe.c below 2 OKAY0.465
rec-test.c below 2 PASS0.489
sas03_bothbranches.c below 7 PASS1.233
sas03.c below 2 PASS0.891
simulated_lese_recursive.c below 2 PASS0.657
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.524
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.396
count_up_down_unsafe.c below 1 OKAY0.402
divide.c below 1 PASS0.404
factor_unsafe.c below 1 OKAY0.355
for_infinite_loop_1_safe.c below 1 PASS0.35
for_infinite_loop_2_safe.c below 1 PASS0.359
interproc.c below 1 PASS0.316
mult.c below 1 PASS0.381
pointer_arith.c below 1 PASS0.327
quotient.c below 3 PASS0.725
subtract.c below 1 PASS0.385
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.387
sum01_bug02_unsafe.c below 1 OKAY0.737
sum01_real_safe.c below 1 PASS0.39
sum01_safe.c below 1 PASS0.415
sum01_unsafe.c below 1 OKAY0.573
sum02_safe.c below 1 PASS0.438
sum03_safe.c below 1 PASS0.469
sum03_unsafe.c below 1 OKAY0.593
sum04_safe.c below 1 PASS0.412
sum04_unsafe.c below 1 OKAY0.596
terminator_02_safe.c below 1 PASS0.365
terminator_02_unsafe.c below 1 OKAY0.416
terminator_03_safe.c below 1 PASS0.368
terminator_03_unsafe.c below 1 OKAY0.366
token_ring01_safe.c below 4 FAIL129.774
token_ring01_unsafe.c below 4 OKAY202.287
toy_safe.c below EXCEPTION 134.445
trex01_safe.c below 1 PASS1.108
trex01_unsafe.c below 1 OKAY0.463
trex02_safe2.c below 3 PASS0.551
trex02_safe.c below 3 PASS0.539
trex02_unsafe.c below 3 OKAY0.547
trex03_safe.c below 1 PASS0.524
trex03_unsafe.c below 1 OKAY0.504
trex04_safe.c below 1 PASS0.401
while_infinite_loop_1_safe.c below 1 PASS0.342
while_infinite_loop_2_safe.c below 1 PASS0.336
while_infinite_loop_3_safe.c below 1 PASS0.342
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 483.088
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.554
blogger_simplified1.c below 3 PASS1.683
divided_difference2.c below TIMEOUT 300.01
mult-proc.c below 3 PASS0.545
mult-proc-params.c below 3 PASS0.542
popall.c below 1 PASS0.968
simulated_scc.c below 1 PASS0.854
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.156
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.414
degree2_binomial.c below 1 PASS0.952
degree2_monomial.c below 1 PASS0.489
degree3_binomial.c below 1 FAIL4.985
degree3_monomial.c below 1 PASS1.031
degree4_binomial.c below 1 FAIL5.094
degree4_monomial.c below 1 PASS1.664
degree5_binomial.c below 1 FAIL16.551
degree5_monomial.c below 1 PASS3.118
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 34.298
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.515
cubic_with_square_interproc.c below 2 FAIL0.735
cubic_with_square_nonlinear.c below 1 FAIL0.692
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.72
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.648
cubic_with_square_unsafe.c below 1 OKAY0.531
multi-input.c below 1 FAIL10.851
multi-input_unsafe.c below 1 OKAY10.882
nondet_loop_bound.c below 1 FAIL0.566
nondet_loop_bound_quartic.c below 1 FAIL0.764
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.792
nondet_loop_bound_unsafe.c below 1 OKAY0.578
nonlinear_stratified.c below 1 PASS128.105
nonlinear_stratified_unsafe.c below 1 OKAY69.586
quartic_with_cube.c below 1 FAIL0.716
quartic_with_cube_nonlinear.c below 1 FAIL0.985
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY1.019
quartic_with_cube_unsafe.c below 1 OKAY0.562
quintic_with_quartic.c below 1 PASS1.12
quintic_with_quartic_nonlinear.c below 1 PASS1.231
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.196
quintic_with_quartic_unsafe.c below 1 OKAY1.164
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 233.958
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.011
degree2_FD_AllAux_AllAssm.c below 1 PASS108.829
degree2_FD_AllAux_FewAssm.c below 1 PASS7.175
degree2_FD_FewAux_FewAssm.c below 1 PASS1.37
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.369
degree3.c below 1 PASS1.165
degree3_FD.c below 1 PASS1.244
degree4.c below 1 PASS1.972
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 124.135
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.548
loop_unsafe.c below 1 OKAY0.548
simulated_lese_parser.c below 1 PASS0.408
simulated_lese_sentinel.c below 1 PASS0.404
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.908
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.42
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.42
/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.402
array_false-unreach-call2.c below 1 OKAY0.42
array_false-unreach-call3.c below 1 OKAY0.39
array_true-unreach-call1.c below 1 FAIL0.384
array_true-unreach-call2.c below 1 FAIL0.417
array_true-unreach-call3.c below 1 PASS0.381
array_true-unreach-call4.c below 1 FAIL0.386
const_false-unreach-call1.c below 1 OKAY0.417
const_true-unreach-call1.c below 1 PASS0.406
diamond_false-unreach-call1.c below 1 OKAY0.432
diamond_true-unreach-call1.c below 1 PASS0.396
diamond_true-unreach-call2.c below 1 PASS0.415
functions_false-unreach-call1.c below 3 OKAY0.504
functions_true-unreach-call1.c below 3 PASS0.522
multivar_false-unreach-call1.c below 1 OKAY0.415
multivar_true-unreach-call1.c below 1 PASS0.42
nested_false-unreach-call1.c below 1 OKAY0.461
nested_true-unreach-call1.c below 1 PASS0.463
overflow_true-unreach-call1.c below 1 PASS0.361
phases_false-unreach-call1.c below 1 OKAY0.503
phases_false-unreach-call2.c below 1 OKAY0.394
phases_true-unreach-call1.c below 1 PASS0.507
phases_true-unreach-call2.c below 1 PASS0.386
simple_false-unreach-call1.c below 1 OKAY0.371
simple_false-unreach-call2.c below 1 OKAY0.362
simple_false-unreach-call3.c below 1 OKAY0.356
simple_false-unreach-call4.c below 1 OKAY0.372
simple_true-unreach-call1.c below 1 PASS0.376
simple_true-unreach-call2.c below 1 PASS0.341
simple_true-unreach-call3.c below 1 PASS0.362
simple_true-unreach-call4.c below 1 PASS0.369
underapprox_false-unreach-call1.c below 1 OKAY0.409
underapprox_false-unreach-call2.c below 1 OKAY0.41
underapprox_true-unreach-call1.c below 1 FAIL0.398
underapprox_true-unreach-call2.c below 1 PASS0.39
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.298
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.598
apache-get-tag_true-unreach-call.c below 1 FAIL0.623
down_true-unreach-call.c below 1 PASS0.454
fragtest_simple_true-unreach-call.c below 1 PASS0.595
half_2_true-unreach-call.c below 1 PASS0.499
heapsort_true-unreach-call.c below 1 PASS2.351
id_build_true-unreach-call.c below 1 PASS0.427
id_trans_false-unreach-call.c below 1 OKAY0.38
id_trans_true-unreach-call.c below 1 PASS0.395
large_const_true-unreach-call.c below 1 PASS0.522
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.449
nested6_true-unreach-call.c below 1 FAIL0.649
nested9_true-unreach-call.c below 1 PASS0.727
nest-if3_true-unreach-call.c below 1 PASS0.566
NetBSD_loop_true-unreach-call.c below 1 PASS0.383
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.514
seq_true-unreach-call.c below 1 PASS0.57
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.627
string_concat-noarr_true-unreach-call.c below 1 PASS0.502
up_true-unreach-call.c below 1 PASS0.457
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.288
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.435
bhmr2007_true-unreach-call.c below 1 PASS0.452
cggmp2005b_true-unreach-call.c below 1 PASS0.655
cggmp2005_true-unreach-call.c below 1 PASS0.431
cggmp2005_variant_true-unreach-call.c below 1 PASS0.42
css2003_true-unreach-call.c below 1 PASS1.127
ddlm2013_true-unreach-call.c below 1 PASS0.603
gcnr2008_false-unreach-call.c below 1 OKAY1.163
gj2007b_true-unreach-call.c below 1 FAIL0.445
gj2007_true-unreach-call.c below 1 PASS0.578
gr2006_true-unreach-call.c below 1 PASS0.576
gsv2008_true-unreach-call.c below 1 PASS0.4
hhk2008_true-unreach-call.c below 1 PASS0.388
jm2006_true-unreach-call.c below 1 PASS0.543
jm2006_variant_true-unreach-call.c below 1 PASS0.618
mcmillan2006_true-unreach-call.c below 1 FAIL0.464
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.298
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.381
count_by_1_variant_true-unreach-call.c below 1 PASS0.476
count_by_2_true-unreach-call.c below 1 PASS0.363
count_by_k_true-unreach-call.c below 1 PASS0.382
count_by_nondet_true-unreach-call.c below 1 PASS0.404
gauss_sum_true-unreach-call.c below 1 PASS0.432
half_true-unreach-call.c below 1 FAIL0.422
nested_true-unreach-call.c below 1 PASS0.532
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.392
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.44
array_true-unreach-call.c below 1 FAIL0.451
bubble_sort_false-unreach-call.c below 4 OKAY79.984
bubble_sort_true-unreach-call.c below 1 PASS5.342
compact_false-unreach-call.c below 1 OKAY0.479
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.402
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.396
eureka_01_false-unreach-call.c below 1 OKAY2.713
eureka_01_true-unreach-call.c below 1 FAIL1.626
eureka_05_true-unreach-call.c below 1 FAIL0.866
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.383
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.399
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.365
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.355
heavy_false-unreach-call.c below 1 OKAY0.61
heavy_true-unreach-call.c below 1 PASS0.594
insertion_sort_false-unreach-call.c below 1 OKAY1.547
insertion_sort_true-unreach-call.c below 1 FAIL0.614
invert_string_false-unreach-call.c below 1 OKAY0.607
invert_string_true-unreach-call.c below 1 FAIL0.664
linear_sea.ch_true-unreach-call.c below 1 FAIL0.411
linear_search_false-unreach-call.c below 1 OKAY0.437
lu.cmp_true-unreach-call.c below 3 PASS28.237
ludcmp_false-unreach-call.c below 3 OKAY28.126
matrix_false-unreach-call_true-termination.c below 1 OKAY1.388
matrix_true-unreach-call_true-termination.c below 1 FAIL0.526
n.c11_true-unreach-call.c below 3 FAIL0.579
n.c24_false-unreach-call.c below 3 OKAY5.313
n.c40_true-unreach-call.c below 1 FAIL0.402
nec11_false-unreach-call.c below 1 OKAY0.412
nec20_false-unreach-call.c below 1 OKAY0.446
nec40_true-unreach-call.c below 1 FAIL0.404
string_false-unreach-call.c below 1 OKAY0.744
string_true-unreach-call.c below 1 FAIL0.776
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.734
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.389
sum01_false-unreach-call_true-termination.c below 1 OKAY0.6
sum01_true-unreach-call_true-termination.c below 1 PASS0.397
sum03_false-unreach-call_true-termination.c below 1 OKAY0.632
sum03_true-unreach-call_false-termination.c below 1 PASS0.531
sum04_false-unreach-call_true-termination.c below 1 OKAY0.602
sum04_true-unreach-call_true-termination.c below 1 PASS0.421
sum_array_false-unreach-call.c below 1 OKAY0.667
sum_array_true-unreach-call.c below 1 FAIL0.718
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.351
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.623
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.44
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.354
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.37
trex01_false-unreach-call_true-termination.c below 3 OKAY0.618
trex01_true-unreach-call.c below 3 PASS0.956
trex02_false-unreach-call_true-termination.c below 3 OKAY0.554
trex02_true-unreach-call_true-termination.c below 3 PASS0.554
trex03_false-unreach-call_true-termination.c below 3 OKAY0.904
trex03_true-unreach-call.c below 3 PASS0.912
trex04_true-unreach-call_false-termination.c below 1 PASS0.429
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.398
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.462
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.417
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.404
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.155
vogal_false-unreach-call.c below 1 OKAY0.958
vogal_true-unreach-call.c below 1 FAIL0.977
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.339
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.353
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.34
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.341
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 199.938
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.595
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.623
Ackermann03_true-unreach-call.c below 7 FAIL1.569
Ackermann04_true-unreach-call.c below 7 FAIL1.6
Addition01_true-unreach-call_true-termination.c below 2 PASS0.845
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.832
Addition03_false-no-overflow.c below 2 PASS0.832
Addition03_true-unreach-call.c below 2 PASS0.814
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.623
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.556
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.579
Fibonacci01_true-unreach-call.c below TIMEOUT 300.004
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.005
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.007
gcd01_true-unreach-call_true-termination.c below 2 PASS0.748
gcd02_true-unreach-call.c below 2 FAIL1.394
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.311
McCarthy91_true-unreach-call.c below 7 FAIL1.262
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.76
Primes_true-unreach-call.c below 3 FAIL2.309
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.567
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.516
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.501
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.864
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.58
afterrec_2calls_true-unreach-call.c below 2 PASS0.554
afterrec_false-unreach-call.c below 2 OKAY0.483
afterrec_true-unreach-call.c below 2 PASS0.478
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.008
fibo_20_false-unreach-call.c below TIMEOUT 300.006
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.005
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.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.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 PASS1.031
id2_b3_o2_false-unreach-call.c below 2 OKAY1.049
id2_b3_o5_true-unreach-call.c below 2 PASS0.993
id2_b5_o10_true-unreach-call.c below 2 PASS1.016
id2_i5_o5_false-unreach-call.c below 2 OKAY0.587
id2_i5_o5_true-unreach-call.c below 2 PASS0.608
id_b2_o3_true-unreach-call.c below 2 PASS0.895
id_b3_o2_false-unreach-call.c below 2 OKAY0.895
id_b3_o5_true-unreach-call.c below 2 PASS0.893
id_b5_o10_true-unreach-call.c below 2 PASS0.894
id_i10_o10_false-unreach-call.c below 2 OKAY0.523
id_i10_o10_true-unreach-call.c below 2 PASS0.541
id_i15_o15_false-unreach-call.c below 2 OKAY0.524
id_i15_o15_true-unreach-call.c below 2 PASS0.532
id_i20_o20_false-unreach-call.c below 2 OKAY0.534
id_i20_o20_true-unreach-call.c below 2 PASS0.541
id_i25_o25_false-unreach-call.c below 2 OKAY0.519
id_i25_o25_true-unreach-call.c below 2 PASS0.545
id_i5_o5_false-unreach-call.c below 2 OKAY0.531
id_i5_o5_true-unreach-call.c below 2 PASS0.544
id_o1000_false-unreach-call.c below 2 OKAY0.539
id_o100_false-unreach-call.c below 2 OKAY0.54
id_o10_false-unreach-call.c below 2 OKAY0.525
id_o200_false-unreach-call.c below 2 OKAY0.538
id_o20_false-unreach-call.c below 2 OKAY0.52
id_o3_false-unreach-call.c below 2 OKAY0.545
sum_10x0_false-unreach-call.c below 2 OKAY0.618
sum_10x0_true-unreach-call.c below 2 PASS0.603
sum_15x0_false-unreach-call.c below 2 OKAY0.581
sum_15x0_true-unreach-call.c below 2 PASS0.591
sum_20x0_false-unreach-call.c below 2 OKAY0.599
sum_20x0_true-unreach-call.c below 2 PASS0.577
sum_25x0_false-unreach-call.c below 2 OKAY0.596
sum_25x0_true-unreach-call.c below 2 PASS0.586
sum_2x3_false-unreach-call.c below 2 OKAY0.611
sum_2x3_true-unreach-call.c below 2 PASS0.588
sum_non_eq_false-unreach-call.c below 2 OKAY0.588
sum_non_eq_true-unreach-call.c below 2 PASS0.613
sum_non_false-unreach-call.c below 2 OKAY0.594
sum_non_true-unreach-call.c below 2 PASS0.602
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9028.026
/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.601
rec-bhmr2007_true-unreach-call.c below 2 PASS0.581
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.157
rec-cggmp2005_true-unreach-call.c below 2 PASS0.533
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.579
rec-css2003_true-unreach-call.c below 2 PASS1.602
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.005
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.166
rec-gj2007b_true-unreach-call.c below 2 FAIL0.521
rec-gj2007_true-unreach-call.c below 2 FAIL0.704
rec-gr2006_true-unreach-call.c below 2 FAIL0.715
rec-gsv2008_true-unreach-call.c below 2 PASS0.562
rec-hhk2008_true-unreach-call.c below 2 PASS0.533
rec-jm2006_true-unreach-call.c below 2 PASS0.675
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.763
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.619
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 311.316
/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.471
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.544
rec-count_by_2_true-unreach-call.c below 2 PASS0.484
rec-count_by_k_true-unreach-call.c below 2 PASS0.505
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.545
rec-gauss_sum_true-unreach-call.c below 2 PASS0.55
rec-half_true-unreach-call.c below 2 FAIL0.534
rec-nested_true-unreach-call.c below 3 FAIL0.904
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.537
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.625
cubic_polynomial_unsafe.c below 2 OKAY0.63
edit_distance_bottom_up.c below 3 FAIL193.067
edit_distance_top_down.c below 3 FAIL5.368
log_log_n_solution.c below 3 FAIL0.599
log_log_n_solution_unsafe.c below 3 OKAY0.632
log_n_solution.c below 2 FAIL0.66
log_n_solution_unsafe.c below 2 OKAY0.613
multivariate_1.c below TIMEOUT 300.096
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL4.012
multivariate_higher_order_unsafe.c below 7 OKAY3.865
n_cubed_solution.c below EXCEPTION 103.927
n_cubed_solution_unsafe.c below EXCEPTION 0.026
n_log_n_solution.c below 8 FAIL1.678
n_log_n_solution_unsafe.c below 8 OKAY1.723
n_squared_two_base_case_even.c below 2 PASS0.701
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.716
n_squared_two_base_case_odd.c below 2 PASS0.717
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.738
pascals_dynamic.c below 3 FAIL2.731
pascals_dynamic_unsafe.c below 3 OKAY2.812
pascals_iterative.c below 1 FAIL5.322
pascals_iterative_unsafe.c below 1 OKAY5.48
pascals_recursive.c below 8 FAIL3.99
pascals_recursive_unsafe.c below 8 OKAY3.774
squared_solution.c below 8 FAIL3.214
squared_solution_unsafe.c below 8 OKAY3.19
two_n_even.c below 2 PASS0.55
two_n_even_unsafe.c below 2 OKAY0.57
two_n_odd.c below 2 PASS0.565
two_n_odd_unsafe.c below 2 OKAY0.56
two_to_n_over_two_even.c below 7 FAIL133.879
two_to_n_over_two_even_unsafe.c below 7 OKAY296.615
two_to_n_over_two_odd.c below 7 FAIL253.571
two_to_n_over_two_odd_unsafe.c below 7 OKAY146.426
two_to_n_squared.c below 5 FAIL21.274
two_to_n_squared_unsafe.c below 5 OKAY21.998
two_to_two_to_n.c below 7 FAIL1.493
two_to_two_to_n_unsafe.c below 7 OKAY1.486
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1829.899
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.436
adding_and_mult_unsafe.c below 1 OKAY0.453
binary_search_array_tree.c below 1 FAIL0.813
exp_add_linear.c below 1 PASS0.61
exp_add_linear_unsafe.c below 1 OKAY0.553
exp_add_loop_rec.c below 1 FAIL0.499
exp_add_loop_rec_unsafe.c below 1 OKAY0.431
exp_add_loop_variable.c below 1 PASS0.536
exp_add_loop_variable_unsafe.c below 1 OKAY0.55
exp_with_linear_inner_loop.c below 1 FAIL0.781
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.737
halving_log1.c below 1 FAIL0.695
linear_two_to_n.c below 7 FAIL1.932
linear_two_to_n_unsafe.c below 7 OKAY2.024
loop_five_to_n.c below 1 PASS0.514
loop_five_to_n_unsafe.c below 1 OKAY0.573
non_loop_five_to_n.c below 7 FAIL56.864
non_loop_five_to_n_unsafe.c below 7 OKAY56.353
power_log_modified.c below 1 PASS0.687
simple_exponential.c below 1 PASS0.462
simple_exponential_for.c below 1 PASS0.473
simple_exponential_for_unsafe.c below 1 OKAY0.484
simple_exponential_unsafe.c below 1 OKAY0.488
two_to_n_minus_n.c below 7 FAIL2.469
two_to_n_minus_n_loop.c below TIMEOUT 300.008
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.005
two_to_n_minus_n_unsafe.c below 7 OKAY2.449
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 732.879
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.732
02.c below 3 FAIL0.939
03.c below 1 PASS0.557
04.c below 1 PASS0.409
05.c below 3 PASS1.318
06.c below 3 FAIL10.687
07.c below 3 PASS0.733
08.c below 3 PASS1.679
09.c below 3 PASS1.119
10.c below 3 FAIL1.312
11.c below 1 PASS0.404
12.c below 3 PASS1.703
13.c below 3 PASS0.711
14.c below 3 PASS0.598
15.c below 1 PASS0.397
16.c below 1 PASS0.537
17.c below 1 PASS3.488
18.c below 1 PASS0.489
19.c below 1 PASS0.599
20.c below 3 FAIL0.837
21.c below 3 PASS0.693
22.c below 3 FAIL0.906
23.c below 1 PASS0.433
24.c below 1 PASS0.5
25.c below 3 FAIL1.755
26.c below TIMEOUT 300.007
27.c below 1 PASS0.577
28.c below 3 PASS0.768
29.c below 3 PASS1.246
30.c below 1 PASS0.448
31.c below 3 PASS1.417
32.c below 1 FAIL0.491
33.c below 3 PASS1.581
34.c below 1 FAIL0.455
35.c below 1 PASS0.399
36.c below 3 PASS3.032
37.c below 3 FAIL0.677
38.c below 1 FAIL0.466
39.c below 3 PASS0.583
40.c below 3 PASS1.047
41.c below 1 PASS0.462
42.c below 3 PASS1.093
43.c below 3 PASS0.706
44.c below 1 PASS0.418
45.c below 3 FAIL3.176
46.c below 3 FAIL2.133
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 354.717
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.498
AGHKTW2017_foo.c below 1 PASS0.5
AGHKTW2017_loginSafe.c below 1 PASS1.104
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.608
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.597
BCK2011_gauss.c below 1 PASS0.582
BCK2011_strength_reduction.c below 1 PASS0.887
BCK2011_strength_reduction_linear.c below 1 PASS0.552
fibonacci_information_flow.c below 1 PASS0.746
loop_splitting_test_safe.c below 1 PASS0.708
TA2005_fib2.c below 1 PASS0.728
TA2005_fib.c below 1 PASS0.58
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 8.09
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.894
c3_cleanup_better.c below 3 PASS1.841
c3_cleanup.c below 3 PASS1.83
c3_intermediate.c below 3 PASS1.797
c3_noinv.c below 3 FAIL1.581
doublers.c below 1 FAIL0.665
doublers_easier.c below 3 FAIL1.362
doublers_easy.c below 1 FAIL0.772
exp_mult.c below 1 FAIL0.459
fig1_rotation_unsafe.c below 1 OKAY0.491
guessing_game.c below 3 FAIL0.655
not_P_solvable.c below 1 PASS0.429
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 12.776
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.463
maxequals_linear_1.c below 1 PASS0.647
maxequals_linear_2.c below 1 PASS0.656
maxequals_linear_3.c below 1 FAIL0.427
maxequals_linear_4.c below 1 PASS0.419
maxequals_linear_5.c below 1 PASS0.442
maxequals_linear_6.c below 1 FAIL0.458
maxequals_matrix1.c below 3 FAIL1.793
maxequals_matrix2.c below 3 FAIL1.705
maxequals_quadratic1.c below 1 FAIL0.481
maxequals_quadratic2.c below 1 PASS0.445
maxequals_stratified1.c below 3 PASS5.307
maxequals_stratified2.c below 3 PASS5.3
maxequals_stratified3.c below 3 FAIL5.562
nine.c below 1 FAIL0.454
nine_nondecreasing.c below 1 PASS0.697
sum_interval_1.c below 1 FAIL0.522
sum_interval_2.c below 1 FAIL0.499
sum_interval_3.c below 1 FAIL0.539
TrackingObjectFields.c below 3 PASS11.692
TrackingObjectFields_inlined.c below 1 PASS3.351
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 41.859
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.495
bobble2_varloop.c below 1 PASS0.5
bobble3.c below TIMEOUT 300.004
bobble4.c below 1 FAIL0.482
bobble5.c below 1 FAIL0.486
bobble.c below 1 PASS0.475
inchworm2.c below 1 TIMEOUT300.005
inchworm3.c below 1 PASS0.505
inchworm4.c below 1 PASS0.501
inchworm5.c below 1 PASS0.463
inchworm6_unsafe.c below 1 OKAY0.469
inchworm.c below 1 FAIL0.467
leapdiff2.c below 1 TIMEOUT300.006
leapfrog_annotated.c below 1 FAIL0.479
leapfrog_annotated_disjunction.c below 1 PASS0.472
leapfrog_asymmetric2.c below 1 FAIL0.556
leapfrog_asymmetric3.c below 1 FAIL0.559
leapfrog_asymmetric.c below 1 FAIL0.51
leapfrog.c below 1 FAIL0.44
leapfrog_materialized.c below 1 FAIL0.493
leapfrog_verbose.c below 1 FAIL0.49
leapspin.c below 1 FAIL0.418
leapsum2.c below 1 TIMEOUT300.005
leapthree.c below 1 FAIL0.499
microbobble2.c below 1 PASS0.452
microbobble3.c below 1 PASS0.47
microbobble_asymmetric.c below 1 PASS0.476
microbobble.c below 1 FAIL0.445
simple_bl2.c below 1 FAIL0.504
simple_bl3.c below 1 FAIL0.414
simple_bl.c below 1 FAIL0.486
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1213.026
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.36
binval_example_2_unsafe.c below 1 OKAY0.363
binval_example_3_unsafe.c below 1 OKAY0.346
binval_example_4.c below 1 PASS0.431
binval_example_4_unsafe.c below 1 OKAY0.419
binval_example_5.c below 1 FAIL1.672
binval_example_5_unsafe.c below 1 OKAY3.9
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.491