[Version Information]
WALi-OpenNWA version: be2c095cbf8ea078087a03cba4c7b85ea673fca0 (2017-07-05 19:28:46 -0400) "Updated frankensuite to avoid integer overflow"
duet version: 37312f93042d9322883c425e7b53f0a32ea6ba3b (2017-07-05 19:03:26 -0400) "Big O bounds in print_hull"
# 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-bytes             base  Bytes library distributed with the OCaml compiler
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.5.3  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
cppo                  1.4.1  Equivalent of the C preprocessor for OCaml programs
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170101  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.8  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.1  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             20170627v3  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            4.1  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
result                  1.2  Compatibility Result module
Z3                 20161217  Z3 SMT solver

Test Name Output No. of Rounds Result Run Time
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below 1 FAIL0.355
kmp.c below 1 PASS1.609
qsort.c below 5 PASS0.895
speed_pldi09_fig1.c below 1 PASS0.488
speed_pldi09_fig4_2.c below 1 FAIL0.387
speed_pldi09_fig4_4.c below 1 PASS20.935
speed_pldi09_fig4_5.c below 1 PASS0.391
speed_pldi10_ex1.c below 1 PASS1.219
speed_pldi10_ex3.c below 1 PASS0.514
speed_pldi10_ex4.c below 1 PASS0.529
speed_popl10_fig2_1.c below 1 PASS0.477
speed_popl10_fig2_2.c below 1 FAIL0.373
speed_popl10_nested_multiple.c below 1 PASS0.468
speed_popl10_nested_single.c below 1 PASS0.435
speed_popl10_sequential_single.c below 1 PASS0.373
speed_popl10_simple_multiple.c below 1 PASS0.509
speed_popl10_simple_single_2.c below 1 PASS0.598
speed_popl10_simple_single.c below 1 PASS0.347
t07.c below 1 PASS0.404
t08.c below 1 PASS0.377
t09.c below 1 PASS0.384
t10.c below 1 PASS0.362
t11.c below 1 PASS0.457
t13.c below 1 FAIL0.416
t15.c below 1 PASS0.418
t16.c below 1 PASS0.401
t19.c below 1 PASS0.392
t20.c below 1 PASS0.376
t27.c below 1 PASS0.558
t28.c below 1 PASS0.471
t30.c below 1 FAIL0.413
t37.c below 2 PASS0.58
t39.c below 2 PASS0.554
t46.c below 1 PASS0.401
t47.c below 1 FAIL0.569
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 38.435
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.375
qsort_full.c below 4 PASS5.522
rec1-param_safe.c below 2 PASS0.379
rec1-param_unsafe.c below 2 OKAY0.376
rec1_safe.c below 2 PASS0.367
rec1_unsafe.c below 2 OKAY0.37
rec2-param_safe.c below 2 PASS0.381
rec2-param_unsafe.c below 2 OKAY0.371
rec2_safe.c below 2 PASS0.381
rec2_unsafe.c below 2 OKAY0.365
rec-test.c below 2 PASS0.376
sas03_bothbranches.c below 7 PASS0.71
sas03.c below 2 PASS0.788
simulated_lese_recursive.c below 2 PASS0.444
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.205
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.346
count_up_down_unsafe.c below 1 OKAY0.339
divide.c below 1 PASS0.329
factor_unsafe.c below 1 OKAY0.312
for_infinite_loop_1_safe.c below 1 PASS0.31
for_infinite_loop_2_safe.c below 1 PASS0.32
interproc.c below 1 PASS0.311
mult.c below 1 PASS0.32
pointer_arith.c below 1 PASS0.304
quotient.c below 3 PASS0.458
subtract.c below 1 PASS0.325
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.343
sum01_bug02_unsafe.c below 1 OKAY0.608
sum01_real_safe.c below 1 PASS0.344
sum01_safe.c below 1 PASS0.339
sum01_unsafe.c below 1 OKAY0.465
sum02_safe.c below 1 PASS0.354
sum03_safe.c below 1 PASS0.396
sum03_unsafe.c below 1 OKAY0.479
sum04_safe.c below 1 PASS0.348
sum04_unsafe.c below 1 OKAY0.468
terminator_02_safe.c below 1 PASS0.311
terminator_02_unsafe.c below 1 OKAY0.353
terminator_03_safe.c below 1 PASS0.323
terminator_03_unsafe.c below 1 OKAY0.316
token_ring01_safe.c below 4 FAIL67.696
token_ring01_unsafe.c below 4 OKAY230.897
toy_safe.c below EXCEPTION 164.918
trex01_safe.c below 1 PASS0.725
trex01_unsafe.c below 1 OKAY0.369
trex02_safe2.c below 3 PASS0.375
trex02_safe.c below 3 PASS0.39
trex02_unsafe.c below 3 OKAY0.385
trex03_safe.c below 1 PASS0.411
trex03_unsafe.c below 1 OKAY0.43
trex04_safe.c below 1 PASS0.352
while_infinite_loop_1_safe.c below 1 PASS0.306
while_infinite_loop_2_safe.c below 1 PASS0.299
while_infinite_loop_3_safe.c below 1 PASS0.309
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 476.983
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.383
blogger_simplified1.c below 3 PASS1.045
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.375
mult-proc-params.c below 3 PASS0.382
popall.c below 1 PASS0.687
simulated_scc.c below 1 PASS0.621
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.498
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.363
degree2_binomial.c below 1 PASS0.719
degree2_monomial.c below 1 PASS0.391
degree3_binomial.c below 1 PASS1.353
degree3_monomial.c below 1 PASS0.433
degree4_binomial.c below 1 PASS2.607
degree4_monomial.c below 1 PASS0.504
degree5_binomial.c below 1 PASS7.152
degree5_monomial.c below 1 PASS0.571
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 14.093
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.448
cubic_with_square_interproc.c below 2 PASS0.565
cubic_with_square_nonlinear.c below 1 PASS0.369
cubic_with_square_nonlinear_interproc.c below 2 PASS0.411
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.382
cubic_with_square_unsafe.c below 1 OKAY0.444
multi-input.c below 1 PASS212.078
multi-input_unsafe.c below 1 OKAY0.472
nondet_loop_bound.c below 1 PASS0.363
nondet_loop_bound_quartic.c below 1 PASS0.372
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.362
nondet_loop_bound_unsafe.c below 1 OKAY0.384
nonlinear_stratified.c below 1 PASS78.826
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube.c below 1 PASS0.609
quartic_with_cube_nonlinear.c below 1 PASS0.378
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.387
quartic_with_cube_unsafe.c below 1 OKAY0.499
quintic_with_quartic.c below 1 PASS1.006
quintic_with_quartic_nonlinear.c below 1 PASS0.444
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.428
quintic_with_quartic_unsafe.c below 1 OKAY0.997
ICRA Assertions (True) = 12/12
ICRA Assertions (False) = 9/10
ICRA Time = 600.228
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.69
degree2_FD_AllAux_AllAssm.c below 1 PASS151.06
degree2_FD_AllAux_FewAssm.c below 1 PASS4.973
degree2_FD_FewAux_FewAssm.c below 1 PASS0.899
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.897
degree3.c below 1 PASS0.618
degree3_FD.c below 1 PASS0.802
degree4.c below 1 PASS0.412
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 160.351
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.43
loop_unsafe.c below 1 OKAY0.417
simulated_lese_parser.c below 1 PASS0.341
simulated_lese_sentinel.c below 1 PASS0.351
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.539
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.342
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.342
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.004
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.004
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.347
array_false-unreach-call2.c below 1 OKAY0.36
array_false-unreach-call3.c below 1 OKAY0.353
array_true-unreach-call1.c below 1 FAIL0.363
array_true-unreach-call2.c below 1 FAIL0.36
array_true-unreach-call3.c below 1 PASS0.352
array_true-unreach-call4.c below 1 FAIL0.35
const_false-unreach-call1.c below 1 OKAY0.354
const_true-unreach-call1.c below 1 PASS0.333
diamond_false-unreach-call1.c below 1 OKAY0.366
diamond_true-unreach-call1.c below 1 PASS0.363
diamond_true-unreach-call2.c below 1 PASS0.364
functions_false-unreach-call1.c below 3 OKAY0.368
functions_true-unreach-call1.c below 3 PASS0.374
multivar_false-unreach-call1.c below 1 OKAY0.366
multivar_true-unreach-call1.c below 1 PASS0.35
nested_false-unreach-call1.c below 1 OKAY0.381
nested_true-unreach-call1.c below 1 PASS0.368
overflow_true-unreach-call1.c below 1 PASS0.323
phases_false-unreach-call1.c below 1 OKAY0.406
phases_false-unreach-call2.c below 1 OKAY0.339
phases_true-unreach-call1.c below 1 PASS0.387
phases_true-unreach-call2.c below 1 PASS0.327
simple_false-unreach-call1.c below 1 OKAY0.332
simple_false-unreach-call2.c below 1 OKAY0.333
simple_false-unreach-call3.c below 1 OKAY0.323
simple_false-unreach-call4.c below 1 OKAY0.326
simple_true-unreach-call1.c below 1 PASS0.324
simple_true-unreach-call2.c below 1 PASS0.328
simple_true-unreach-call3.c below 1 PASS0.321
simple_true-unreach-call4.c below 1 PASS0.321
underapprox_false-unreach-call1.c below 1 OKAY0.335
underapprox_false-unreach-call2.c below 1 OKAY0.359
underapprox_true-unreach-call1.c below 1 FAIL0.338
underapprox_true-unreach-call2.c below 1 PASS0.335
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.229
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.828
apache-get-tag_true-unreach-call.c below 1 FAIL0.416
down_true-unreach-call.c below 1 PASS0.363
fragtest_simple_true-unreach-call.c below 1 PASS0.441
half_2_true-unreach-call.c below 1 PASS0.397
heapsort_true-unreach-call.c below 1 TIMEOUT300.198
id_build_true-unreach-call.c below 1 PASS0.457
id_trans_false-unreach-call.c below 1 OKAY0.352
large_const_true-unreach-call.c below 1 PASS0.431
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.383
nested6_true-unreach-call.c below 1 FAIL0.492
nested9_true-unreach-call.c below 1 PASS0.505
nest-if3_true-unreach-call.c below 1 PASS0.459
NetBSD_loop_true-unreach-call.c below 1 PASS0.337
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.392
seq_true-unreach-call.c below 1 PASS0.437
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.458
string_concat-noarr_true-unreach-call.c below 1 PASS0.399
up_true-unreach-call.c below 1 PASS0.368
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 309.113
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.378
bhmr2007_true-unreach-call.c below 1 PASS0.381
cggmp2005b_true-unreach-call.c below 1 PASS0.473
cggmp2005_true-unreach-call.c below 1 PASS0.336
cggmp2005_variant_true-unreach-call.c below 1 PASS0.343
css2003_true-unreach-call.c below 1 PASS0.766
ddlm2013_true-unreach-call.c below 1 PASS0.511
gcnr2008_false-unreach-call.c below 1 OKAY0.899
gj2007b_true-unreach-call.c below 1 FAIL0.382
gj2007_true-unreach-call.c below 1 PASS0.447
gr2006_true-unreach-call.c below 1 PASS0.451
gsv2008_true-unreach-call.c below 1 PASS0.35
hhk2008_true-unreach-call.c below 1 PASS0.331
jm2006_true-unreach-call.c below 1 PASS0.402
jm2006_variant_true-unreach-call.c below 1 PASS0.464
mcmillan2006_true-unreach-call.c below 1 FAIL0.381
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.295
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.314
count_by_1_variant_true-unreach-call.c below 1 PASS0.384
count_by_2_true-unreach-call.c below 1 PASS0.323
count_by_k_true-unreach-call.c below 1 PASS0.345
count_by_nondet_true-unreach-call.c below 1 FAIL0.341
gauss_sum_true-unreach-call.c below 1 PASS0.376
half_true-unreach-call.c below 1 FAIL0.362
nested_true-unreach-call.c below 1 PASS0.408
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.853
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.372
array_true-unreach-call.c below 1 FAIL0.375
bubble_sort_false-unreach-call.c below 4 OKAY48.131
bubble_sort_true-unreach-call.c below 1 PASS3.552
compact_false-unreach-call.c below 1 OKAY0.381
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.349
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.336
eureka_01_false-unreach-call.c below 1 OKAY1.985
eureka_01_true-unreach-call.c below 1 FAIL1.451
eureka_05_true-unreach-call.c below TIMEOUT 300.005
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.332
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.324
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.314
heavy_false-unreach-call.c below 1 OKAY0.451
heavy_true-unreach-call.c below 1 PASS0.436
insertion_sort_false-unreach-call.c below 1 OKAY1.489
insertion_sort_true-unreach-call.c below 1 FAIL0.542
invert_string_false-unreach-call.c below 1 OKAY0.494
invert_string_true-unreach-call.c below 1 FAIL0.522
linear_sea.ch_true-unreach-call.c below 1 FAIL0.374
linear_search_false-unreach-call.c below 1 OKAY0.399
lu.cmp_true-unreach-call.c below 3 PASS15.697
ludcmp_false-unreach-call.c below 3 OKAY15.99
matrix_false-unreach-call_true-termination.c below 1 OKAY1.0
matrix_true-unreach-call_true-termination.c below 1 FAIL0.42
n.c11_true-unreach-call.c below 3 FAIL0.422
n.c24_false-unreach-call.c below 3 OKAY2.567
n.c40_true-unreach-call.c below 1 FAIL0.339
nec11_false-unreach-call.c below 1 OKAY0.353
nec20_false-unreach-call.c below 1 OKAY0.389
nec40_true-unreach-call.c below 1 FAIL0.357
string_false-unreach-call.c below 1 OKAY0.594
string_true-unreach-call.c below 1 FAIL0.631
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.617
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.331
sum01_false-unreach-call_true-termination.c below 1 OKAY0.457
sum01_true-unreach-call_true-termination.c below 1 PASS0.358
sum03_false-unreach-call_true-termination.c below 1 OKAY0.483
sum03_true-unreach-call_false-termination.c below 1 PASS0.419
sum04_false-unreach-call_true-termination.c below 1 OKAY0.481
sum04_true-unreach-call_true-termination.c below 1 PASS0.347
sum_array_false-unreach-call.c below 1 OKAY0.553
sum_array_true-unreach-call.c below 1 FAIL0.613
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.322
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.449
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.341
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.331
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.33
trex01_false-unreach-call_true-termination.c below 3 OKAY0.42
trex01_true-unreach-call.c below 3 PASS0.68
trex02_false-unreach-call_true-termination.c below 3 OKAY0.398
trex02_true-unreach-call_true-termination.c below 3 PASS0.401
trex03_false-unreach-call_true-termination.c below 3 OKAY0.649
trex03_true-unreach-call.c below 3 PASS0.644
trex04_true-unreach-call_false-termination.c below 1 PASS0.385
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.361
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.383
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.353
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.357
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY3.832
vogal_false-unreach-call.c below 1 OKAY0.735
vogal_true-unreach-call.c below 1 FAIL0.712
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.311
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.31
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.307
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.3
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 424.343
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.919
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.883
Ackermann03_true-unreach-call.c below 7 FAIL0.93
Ackermann04_true-unreach-call.c below 7 FAIL0.934
Addition01_true-unreach-call_true-termination.c below 2 PASS0.543
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.525
Addition03_false-no-overflow.c below 2 PASS0.541
Addition03_true-unreach-call.c below 2 PASS0.544
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.462
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.411
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.396
Fibonacci01_true-unreach-call.c below 7 FAIL0.682
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.668
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.694
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.657
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.669
gcd01_true-unreach-call_true-termination.c below 2 PASS0.539
gcd02_true-unreach-call.c below 2 FAIL0.921
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY6.843
McCarthy91_true-unreach-call.c below 7 PASS6.939
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.556
Primes_true-unreach-call.c below 3 FAIL1.362
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.648
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.372
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.387
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 7/7
ICRA Time = 30.025
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.418
afterrec_2calls_true-unreach-call.c below 2 PASS0.397
afterrec_false-unreach-call.c below 2 OKAY0.37
afterrec_true-unreach-call.c below 2 PASS0.371
fibo_10_false-unreach-call.c below 7 OKAY0.645
fibo_10_true-unreach-call.c below 7 FAIL0.686
fibo_15_false-unreach-call.c below 7 OKAY0.672
fibo_15_true-unreach-call.c below 7 FAIL0.651
fibo_20_false-unreach-call.c below 7 OKAY0.662
fibo_20_true-unreach-call.c below 7 FAIL0.672
fibo_25_false-unreach-call.c below 7 OKAY0.685
fibo_25_true-unreach-call.c below 7 FAIL0.647
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.03
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.011
fibo_5_false-unreach-call.c below 7 OKAY0.657
fibo_5_true-unreach-call.c below 7 FAIL0.665
fibo_7_false-unreach-call.c below 7 OKAY0.659
fibo_7_true-unreach-call.c below 7 FAIL0.671
id2_b2_o3_true-unreach-call.c below 2 PASS0.618
id2_b3_o2_false-unreach-call.c below 2 OKAY0.666
id2_b3_o5_true-unreach-call.c below 2 PASS0.631
id2_b5_o10_true-unreach-call.c below 2 PASS0.621
id2_i5_o5_false-unreach-call.c below 2 OKAY0.403
id2_i5_o5_true-unreach-call.c below 2 PASS0.398
id_b2_o3_true-unreach-call.c below 2 PASS0.553
id_b3_o2_false-unreach-call.c below 2 OKAY0.543
id_b3_o5_true-unreach-call.c below 2 PASS0.559
id_b5_o10_true-unreach-call.c below 2 PASS0.528
id_i10_o10_false-unreach-call.c below 2 OKAY0.372
id_i10_o10_true-unreach-call.c below 2 PASS0.377
id_i15_o15_false-unreach-call.c below 2 OKAY0.367
id_i15_o15_true-unreach-call.c below 2 PASS0.367
id_i20_o20_false-unreach-call.c below 2 OKAY0.379
id_i20_o20_true-unreach-call.c below 2 PASS0.374
id_i25_o25_false-unreach-call.c below 2 OKAY0.373
id_i25_o25_true-unreach-call.c below 2 PASS0.365
id_i5_o5_false-unreach-call.c below 2 OKAY0.364
id_i5_o5_true-unreach-call.c below 2 PASS0.364
id_o1000_false-unreach-call.c below 2 OKAY0.37
id_o100_false-unreach-call.c below 2 OKAY0.38
id_o10_false-unreach-call.c below 2 OKAY0.391
id_o200_false-unreach-call.c below 2 OKAY0.391
id_o20_false-unreach-call.c below 2 OKAY0.382
id_o3_false-unreach-call.c below 2 OKAY0.371
sum_10x0_false-unreach-call.c below 2 OKAY0.419
sum_10x0_true-unreach-call.c below 2 PASS0.401
sum_15x0_false-unreach-call.c below 2 OKAY0.409
sum_15x0_true-unreach-call.c below 2 PASS0.41
sum_20x0_false-unreach-call.c below 2 OKAY0.405
sum_20x0_true-unreach-call.c below 2 PASS0.419
sum_25x0_false-unreach-call.c below 2 OKAY0.419
sum_25x0_true-unreach-call.c below 2 PASS0.418
sum_2x3_false-unreach-call.c below 2 OKAY0.408
sum_2x3_true-unreach-call.c below 2 PASS0.409
sum_non_eq_false-unreach-call.c below 2 OKAY0.397
sum_non_eq_true-unreach-call.c below 2 PASS0.4
sum_non_false-unreach-call.c below 2 OKAY0.409
sum_non_true-unreach-call.c below 2 PASS0.399
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5426.988
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-lit
rec-afnp2014_true-unreach-call.c below 2 PASS0.422
rec-bhmr2007_true-unreach-call.c below 2 PASS0.406
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.613
rec-cggmp2005_true-unreach-call.c below 2 PASS0.391
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.424
rec-css2003_true-unreach-call.c below 2 PASS0.952
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.062
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.757
rec-gj2007b_true-unreach-call.c below 2 FAIL0.358
rec-gj2007_true-unreach-call.c below 2 FAIL0.469
rec-gr2006_true-unreach-call.c below 2 FAIL0.46
rec-gsv2008_true-unreach-call.c below 2 PASS0.426
rec-hhk2008_true-unreach-call.c below 2 PASS0.386
rec-jm2006_true-unreach-call.c below 2 PASS0.454
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.49
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.425
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.495
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c below 2 PASS0.353
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.389
rec-count_by_2_true-unreach-call.c below 2 PASS0.359
rec-count_by_k_true-unreach-call.c below 2 PASS0.379
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.386
rec-gauss_sum_true-unreach-call.c below 2 PASS0.417
rec-half_true-unreach-call.c below 2 FAIL0.408
rec-nested_true-unreach-call.c below 3 FAIL0.509
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.2
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.505
cubic_polynomial_unsafe.c below 2 OKAY0.521
edit_distance_bottom_up.c below 3 FAIL125.011
edit_distance_top_down.c below 3 FAIL2.608
log_log_n_solution.c below 3 FAIL0.4
log_log_n_solution_unsafe.c below 3 OKAY0.429
log_n_solution.c below 2 FAIL0.435
log_n_solution_unsafe.c below 2 OKAY0.438
multivariate_1.c below TIMEOUT 300.004
multivariate_1_unsafe.c below TIMEOUT 300.004
multivariate_higher_order.c below 7 FAIL19.073
multivariate_higher_order_unsafe.c below 7 OKAY18.641
n_cubed_solution.c below EXCEPTION 46.175
n_cubed_solution_unsafe.c below EXCEPTION 0.025
n_log_n_solution.c below TIMEOUT 300.046
n_log_n_solution_unsafe.c below TIMEOUT 300.047
n_squared_two_base_case_even.c below 2 PASS0.474
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.474
n_squared_two_base_case_odd.c below 2 PASS0.495
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.489
pascals_dynamic.c below 3 FAIL2.455
pascals_dynamic_unsafe.c below 3 OKAY2.484
pascals_iterative.c below 1 FAIL3.489
pascals_iterative_unsafe.c below 1 OKAY3.581
pascals_recursive.c below 8 FAIL9.5
pascals_recursive_unsafe.c below 8 OKAY9.506
squared_solution.c below TIMEOUT 300.004
squared_solution_unsafe.c below TIMEOUT 300.004
two_n_even.c below 2 PASS0.406
two_n_even_unsafe.c below 2 OKAY0.416
two_n_odd.c below 2 PASS0.405
two_n_odd_unsafe.c below 2 OKAY0.403
two_to_n_over_two_even.c below TIMEOUT 300.004
two_to_n_over_two_even_unsafe.c below TIMEOUT 300.004
two_to_n_over_two_odd.c below TIMEOUT 300.005
two_to_n_over_two_odd_unsafe.c below TIMEOUT 300.004
two_to_n_squared.c below 8 FAIL20.909
two_to_n_squared_unsafe.c below 8 OKAY20.191
two_to_two_to_n.c below 7 FAIL0.825
two_to_two_to_n_unsafe.c below 7 OKAY0.812
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 13/19
ICRA Time = 3291.701
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.356
adding_and_mult_unsafe.c below 1 OKAY0.366
binary_search_array_tree.c below 1 FAIL0.615
exp_add_linear.c below 1 PASS0.417
exp_add_linear_unsafe.c below 1 OKAY0.413
exp_add_loop_rec.c below 1 FAIL0.356
exp_add_loop_rec_unsafe.c below 1 OKAY0.367
exp_add_loop_variable.c below 1 PASS0.41
exp_add_loop_variable_unsafe.c below 1 OKAY0.411
exp_with_linear_inner_loop.c below 1 FAIL0.455
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.465
halving_log1.c below 1 FAIL0.496
linear_two_to_n.c below 8 FAIL1.072
linear_two_to_n_unsafe.c below 8 OKAY1.078
loop_five_to_n.c below 1 PASS0.384
loop_five_to_n_unsafe.c below 1 OKAY0.39
non_loop_five_to_n.c below TIMEOUT 300.03
non_loop_five_to_n_unsafe.c below TIMEOUT 300.028
power_log.c below 1 PASS0.486
power_log_modified.c below 1 PASS0.484
simple_exponential.c below 1 PASS0.384
simple_exponential_for.c below 1 PASS0.368
simple_exponential_for_unsafe.c below 1 OKAY0.394
simple_exponential_unsafe.c below 1 OKAY0.384
two_to_n_minus_n.c below 7 FAIL1.172
two_to_n_minus_n_loop.c below 7 FAIL1.712
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.67
two_to_n_minus_n_unsafe.c below 7 OKAY1.227
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 616.39