[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.359
kmp.c below 1 PASS1.625
qsort.c below 5 PASS0.921
speed_pldi09_fig1.c below 1 PASS0.519
speed_pldi09_fig4_2.c below 1 FAIL0.382
speed_pldi09_fig4_4.c below 1 PASS20.699
speed_pldi09_fig4_5.c below 1 PASS0.398
speed_pldi10_ex1.c below 1 PASS1.213
speed_pldi10_ex3.c below 1 PASS0.511
speed_pldi10_ex4.c below 1 PASS0.532
speed_popl10_fig2_1.c below 1 PASS0.454
speed_popl10_fig2_2.c below 1 FAIL0.349
speed_popl10_nested_multiple.c below 1 PASS0.446
speed_popl10_nested_single.c below 1 PASS0.426
speed_popl10_sequential_single.c below 1 PASS0.387
speed_popl10_simple_multiple.c below 1 PASS0.514
speed_popl10_simple_single_2.c below 1 PASS0.617
speed_popl10_simple_single.c below 1 PASS0.34
t07.c below 1 PASS0.412
t08.c below 1 PASS0.383
t09.c below 1 PASS0.38
t10.c below 1 PASS0.368
t11.c below 1 PASS0.46
t13.c below 1 FAIL0.416
t15.c below 1 PASS0.43
t16.c below 1 PASS0.395
t19.c below 1 PASS0.394
t20.c below 1 PASS0.385
t27.c below 1 PASS0.535
t28.c below 1 PASS0.476
t30.c below 1 FAIL0.404
t37.c below 2 PASS0.587
t39.c below 2 PASS0.549
t46.c below 1 PASS0.389
t47.c below 1 FAIL0.553
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 38.208
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.36
qsort_full.c below 4 PASS5.546
rec1-param_safe.c below 2 PASS0.382
rec1-param_unsafe.c below 2 OKAY0.374
rec1_safe.c below 2 PASS0.37
rec1_unsafe.c below 2 OKAY0.376
rec2-param_safe.c below 2 PASS0.367
rec2-param_unsafe.c below 2 OKAY0.379
rec2_safe.c below 2 PASS0.369
rec2_unsafe.c below 2 OKAY0.357
rec-test.c below 2 PASS0.363
sas03_bothbranches.c below 7 PASS0.711
sas03.c below 2 PASS0.782
simulated_lese_recursive.c below 2 PASS0.438
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.174
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.331
count_up_down_unsafe.c below 1 OKAY0.331
divide.c below 1 PASS0.322
factor_unsafe.c below 1 OKAY0.325
for_infinite_loop_1_safe.c below 1 PASS0.315
for_infinite_loop_2_safe.c below 1 PASS0.311
interproc.c below 1 PASS0.296
mult.c below 1 PASS0.327
pointer_arith.c below 1 PASS0.309
quotient.c below 3 PASS0.485
subtract.c below 1 PASS0.334
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.334
sum01_bug02_unsafe.c below 1 OKAY0.594
sum01_real_safe.c below 1 PASS0.322
sum01_safe.c below 1 PASS0.349
sum01_unsafe.c below 1 OKAY0.457
sum02_safe.c below 1 PASS0.352
sum03_safe.c below 1 PASS0.405
sum03_unsafe.c below 1 OKAY0.476
sum04_safe.c below 1 PASS0.345
sum04_unsafe.c below 1 OKAY0.475
terminator_02_safe.c below 1 PASS0.318
terminator_02_unsafe.c below 1 OKAY0.357
terminator_03_safe.c below 1 PASS0.331
terminator_03_unsafe.c below 1 OKAY0.333
token_ring01_safe.c below 4 FAIL67.881
token_ring01_unsafe.c below 4 OKAY190.705
toy_safe.c below EXCEPTION 163.401
trex01_safe.c below 1 PASS0.562
trex01_unsafe.c below 1 OKAY0.37
trex02_safe2.c below 3 PASS0.38
trex02_safe.c below 3 PASS0.378
trex02_unsafe.c below 3 OKAY0.398
trex03_safe.c below 1 PASS0.425
trex03_unsafe.c below 1 OKAY0.422
trex04_safe.c below 1 PASS0.357
while_infinite_loop_1_safe.c below 1 PASS0.318
while_infinite_loop_2_safe.c below 1 PASS0.302
while_infinite_loop_3_safe.c below 1 PASS0.322
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 435.355
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.374
blogger_simplified1.c below 3 PASS1.076
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.365
mult-proc-params.c below 3 PASS0.393
popall.c below 1 PASS0.696
simulated_scc.c below 1 PASS0.601
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.51
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.348
degree2_binomial.c below 1 PASS0.704
degree2_monomial.c below 1 PASS0.388
degree3_binomial.c below 1 PASS1.317
degree3_monomial.c below 1 PASS0.427
degree4_binomial.c below 1 PASS2.559
degree4_monomial.c below 1 PASS0.489
degree5_binomial.c below 1 PASS7.144
degree5_monomial.c below 1 PASS0.553
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 13.929
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.451
cubic_with_square_interproc.c below 2 PASS0.567
cubic_with_square_nonlinear.c below 1 PASS0.36
cubic_with_square_nonlinear_interproc.c below 2 PASS0.412
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.369
cubic_with_square_unsafe.c below 1 OKAY0.455
multi-input.c below 1 PASS210.597
multi-input_unsafe.c below 1 OKAY0.464
nondet_loop_bound.c below 1 PASS0.351
nondet_loop_bound_quartic.c below 1 PASS0.375
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.374
nondet_loop_bound_unsafe.c below 1 OKAY0.383
nonlinear_stratified.c below 1 PASS78.33
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube.c below 1 PASS0.598
quartic_with_cube_nonlinear.c below 1 PASS0.376
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.381
quartic_with_cube_unsafe.c below 1 OKAY0.489
quintic_with_quartic.c below 1 PASS1.018
quintic_with_quartic_nonlinear.c below 1 PASS0.419
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.453
quintic_with_quartic_unsafe.c below 1 OKAY1.015
ICRA Assertions (True) = 12/12
ICRA Assertions (False) = 9/10
ICRA Time = 598.241
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.677
degree2_FD_AllAux_AllAssm.c below 1 PASS160.359
degree2_FD_AllAux_FewAssm.c below 1 PASS5.004
degree2_FD_FewAux_FewAssm.c below 1 PASS0.877
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.948
degree3.c below 1 PASS0.657
degree3_FD.c below 1 PASS0.906
degree4.c below 1 PASS0.432
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 169.86
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.423
loop_unsafe.c below 1 OKAY0.438
simulated_lese_parser.c below 1 PASS0.347
simulated_lese_sentinel.c below 1 PASS0.355
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.563
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.356
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.356
/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.355
array_true-unreach-call1.c below 1 FAIL0.344
array_true-unreach-call2.c below 1 FAIL0.361
array_true-unreach-call3.c below 1 PASS0.354
array_true-unreach-call4.c below 1 FAIL0.333
const_false-unreach-call1.c below 1 OKAY0.343
const_true-unreach-call1.c below 1 PASS0.34
diamond_false-unreach-call1.c below 1 OKAY0.374
diamond_true-unreach-call1.c below 1 PASS0.354
diamond_true-unreach-call2.c below 1 PASS0.371
functions_false-unreach-call1.c below 3 OKAY0.389
functions_true-unreach-call1.c below 3 PASS0.373
multivar_false-unreach-call1.c below 1 OKAY0.344
multivar_true-unreach-call1.c below 1 PASS0.349
nested_false-unreach-call1.c below 1 OKAY0.379
nested_true-unreach-call1.c below 1 PASS0.347
overflow_true-unreach-call1.c below 1 PASS0.314
phases_false-unreach-call1.c below 1 OKAY0.399
phases_false-unreach-call2.c below 1 OKAY0.33
phases_true-unreach-call1.c below 1 PASS0.39
phases_true-unreach-call2.c below 1 PASS0.338
simple_false-unreach-call1.c below 1 OKAY0.326
simple_false-unreach-call2.c below 1 OKAY0.326
simple_false-unreach-call3.c below 1 OKAY0.317
simple_false-unreach-call4.c below 1 OKAY0.322
simple_true-unreach-call1.c below 1 PASS0.329
simple_true-unreach-call2.c below 1 PASS0.314
simple_true-unreach-call3.c below 1 PASS0.327
simple_true-unreach-call4.c below 1 PASS0.343
underapprox_false-unreach-call1.c below 1 OKAY0.334
underapprox_false-unreach-call2.c below 1 OKAY0.348
underapprox_true-unreach-call1.c below 1 FAIL0.354
underapprox_true-unreach-call2.c below 1 PASS0.342
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.17
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.827
apache-get-tag_true-unreach-call.c below 1 FAIL0.422
down_true-unreach-call.c below 1 PASS0.355
fragtest_simple_true-unreach-call.c below 1 PASS0.446
half_2_true-unreach-call.c below 1 PASS0.385
heapsort_true-unreach-call.c below 1 TIMEOUT300.192
id_build_true-unreach-call.c below 1 PASS0.457
id_trans_false-unreach-call.c below 1 OKAY0.338
large_const_true-unreach-call.c below 1 PASS0.424
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.376
nested6_true-unreach-call.c below 1 FAIL0.502
nested9_true-unreach-call.c below 1 PASS0.526
nest-if3_true-unreach-call.c below 1 PASS0.467
NetBSD_loop_true-unreach-call.c below 1 PASS0.334
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.381
seq_true-unreach-call.c below 1 PASS0.427
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.469
string_concat-noarr_true-unreach-call.c below 1 PASS0.381
up_true-unreach-call.c below 1 PASS0.364
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 309.073
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.39
bhmr2007_true-unreach-call.c below 1 PASS0.386
cggmp2005b_true-unreach-call.c below 1 PASS0.49
cggmp2005_true-unreach-call.c below 1 PASS0.346
cggmp2005_variant_true-unreach-call.c below 1 PASS0.354
css2003_true-unreach-call.c below 1 PASS0.754
ddlm2013_true-unreach-call.c below 1 PASS0.514
gcnr2008_false-unreach-call.c below 1 OKAY0.898
gj2007b_true-unreach-call.c below 1 FAIL0.364
gj2007_true-unreach-call.c below 1 PASS0.451
gr2006_true-unreach-call.c below 1 PASS0.415
gsv2008_true-unreach-call.c below 1 PASS0.331
hhk2008_true-unreach-call.c below 1 PASS0.333
jm2006_true-unreach-call.c below 1 PASS0.39
jm2006_variant_true-unreach-call.c below 1 PASS0.453
mcmillan2006_true-unreach-call.c below 1 FAIL0.365
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.234
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.315
count_by_1_variant_true-unreach-call.c below 1 PASS0.382
count_by_2_true-unreach-call.c below 1 PASS0.316
count_by_k_true-unreach-call.c below 1 PASS0.336
count_by_nondet_true-unreach-call.c below 1 FAIL0.345
gauss_sum_true-unreach-call.c below 1 PASS0.354
half_true-unreach-call.c below 1 FAIL0.35
nested_true-unreach-call.c below 1 PASS0.424
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.822
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.393
array_true-unreach-call.c below 1 FAIL0.39
bubble_sort_false-unreach-call.c below 4 OKAY47.932
bubble_sort_true-unreach-call.c below 1 PASS3.567
compact_false-unreach-call.c below 1 OKAY0.389
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.353
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.332
eureka_01_false-unreach-call.c below 1 OKAY2.009
eureka_01_true-unreach-call.c below 1 FAIL1.411
eureka_05_true-unreach-call.c below TIMEOUT 300.004
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.341
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.318
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.311
heavy_false-unreach-call.c below 1 OKAY0.459
heavy_true-unreach-call.c below 1 PASS0.436
insertion_sort_false-unreach-call.c below 1 OKAY1.522
insertion_sort_true-unreach-call.c below 1 FAIL0.523
invert_string_false-unreach-call.c below 1 OKAY0.479
invert_string_true-unreach-call.c below 1 FAIL0.514
linear_sea.ch_true-unreach-call.c below 1 FAIL0.378
linear_search_false-unreach-call.c below 1 OKAY0.396
lu.cmp_true-unreach-call.c below 3 PASS15.934
ludcmp_false-unreach-call.c below 3 OKAY16.144
matrix_false-unreach-call_true-termination.c below 1 OKAY1.029
matrix_true-unreach-call_true-termination.c below 1 FAIL0.411
n.c11_true-unreach-call.c below 3 FAIL0.409
n.c24_false-unreach-call.c below 3 OKAY2.571
n.c40_true-unreach-call.c below 1 FAIL0.349
nec11_false-unreach-call.c below 1 OKAY0.358
nec20_false-unreach-call.c below 1 OKAY0.376
nec40_true-unreach-call.c below 1 FAIL0.358
string_false-unreach-call.c below 1 OKAY0.584
string_true-unreach-call.c below 1 FAIL0.613
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.585
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.327
sum01_false-unreach-call_true-termination.c below 1 OKAY0.469
sum01_true-unreach-call_true-termination.c below 1 PASS0.36
sum03_false-unreach-call_true-termination.c below 1 OKAY0.489
sum03_true-unreach-call_false-termination.c below 1 PASS0.408
sum04_false-unreach-call_true-termination.c below 1 OKAY0.483
sum04_true-unreach-call_true-termination.c below 1 PASS0.35
sum_array_false-unreach-call.c below 1 OKAY0.563
sum_array_true-unreach-call.c below 1 FAIL0.619
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.333
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.435
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.349
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.339
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.331
trex01_false-unreach-call_true-termination.c below 3 OKAY0.441
trex01_true-unreach-call.c below 3 PASS0.666
trex02_false-unreach-call_true-termination.c below 3 OKAY0.4
trex02_true-unreach-call_true-termination.c below 3 PASS0.39
trex03_false-unreach-call_true-termination.c below 3 OKAY0.667
trex03_true-unreach-call.c below 3 PASS0.651
trex04_true-unreach-call_false-termination.c below 1 PASS0.367
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.346
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.38
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.376
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.36
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY3.781
vogal_false-unreach-call.c below 1 OKAY0.728
vogal_true-unreach-call.c below 1 FAIL0.773
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.314
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.311
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.31
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 424.601
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.916
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.883
Ackermann03_true-unreach-call.c below 7 FAIL0.959
Ackermann04_true-unreach-call.c below 7 FAIL0.93
Addition01_true-unreach-call_true-termination.c below 2 PASS0.52
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.517
Addition03_false-no-overflow.c below 2 PASS0.538
Addition03_true-unreach-call.c below 2 PASS0.548
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.478
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.41
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.423
Fibonacci01_true-unreach-call.c below 7 FAIL0.687
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.674
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.692
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.705
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.673
gcd01_true-unreach-call_true-termination.c below 2 PASS0.534
gcd02_true-unreach-call.c below 2 FAIL0.927
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY6.848
McCarthy91_true-unreach-call.c below 7 PASS6.869
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.561
Primes_true-unreach-call.c below 3 FAIL1.37
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.663
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.38
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.389
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 7/7
ICRA Time = 30.094
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.444
afterrec_2calls_true-unreach-call.c below 2 PASS0.393
afterrec_false-unreach-call.c below 2 OKAY0.364
afterrec_true-unreach-call.c below 2 PASS0.364
fibo_10_false-unreach-call.c below 7 OKAY0.672
fibo_10_true-unreach-call.c below 7 FAIL0.658
fibo_15_false-unreach-call.c below 7 OKAY0.655
fibo_15_true-unreach-call.c below 7 FAIL0.641
fibo_20_false-unreach-call.c below 7 OKAY0.668
fibo_20_true-unreach-call.c below 7 FAIL0.658
fibo_25_false-unreach-call.c below 7 OKAY0.645
fibo_25_true-unreach-call.c below 7 FAIL0.682
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.032
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.012
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.009
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.011
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.014
fibo_5_false-unreach-call.c below 7 OKAY0.666
fibo_5_true-unreach-call.c below 7 FAIL0.687
fibo_7_false-unreach-call.c below 7 OKAY0.67
fibo_7_true-unreach-call.c below 7 FAIL0.678
id2_b2_o3_true-unreach-call.c below 2 PASS0.631
id2_b3_o2_false-unreach-call.c below 2 OKAY0.636
id2_b3_o5_true-unreach-call.c below 2 PASS0.627
id2_b5_o10_true-unreach-call.c below 2 PASS0.601
id2_i5_o5_false-unreach-call.c below 2 OKAY0.391
id2_i5_o5_true-unreach-call.c below 2 PASS0.387
id_b2_o3_true-unreach-call.c below 2 PASS0.554
id_b3_o2_false-unreach-call.c below 2 OKAY0.526
id_b3_o5_true-unreach-call.c below 2 PASS0.54
id_b5_o10_true-unreach-call.c below 2 PASS0.526
id_i10_o10_false-unreach-call.c below 2 OKAY0.362
id_i10_o10_true-unreach-call.c below 2 PASS0.356
id_i15_o15_false-unreach-call.c below 2 OKAY0.359
id_i15_o15_true-unreach-call.c below 2 PASS0.371
id_i20_o20_false-unreach-call.c below 2 OKAY0.371
id_i20_o20_true-unreach-call.c below 2 PASS0.375
id_i25_o25_false-unreach-call.c below 2 OKAY0.383
id_i25_o25_true-unreach-call.c below 2 PASS0.366
id_i5_o5_false-unreach-call.c below 2 OKAY0.388
id_i5_o5_true-unreach-call.c below 2 PASS0.369
id_o1000_false-unreach-call.c below 2 OKAY0.371
id_o100_false-unreach-call.c below 2 OKAY0.378
id_o10_false-unreach-call.c below 2 OKAY0.369
id_o200_false-unreach-call.c below 2 OKAY0.369
id_o20_false-unreach-call.c below 2 OKAY0.367
id_o3_false-unreach-call.c below 2 OKAY0.367
sum_10x0_false-unreach-call.c below 2 OKAY0.408
sum_10x0_true-unreach-call.c below 2 PASS0.395
sum_15x0_false-unreach-call.c below 2 OKAY0.422
sum_15x0_true-unreach-call.c below 2 PASS0.401
sum_20x0_false-unreach-call.c below 2 OKAY0.41
sum_20x0_true-unreach-call.c below 2 PASS0.413
sum_25x0_false-unreach-call.c below 2 OKAY0.412
sum_25x0_true-unreach-call.c below 2 PASS0.415
sum_2x3_false-unreach-call.c below 2 OKAY0.414
sum_2x3_true-unreach-call.c below 2 PASS0.421
sum_non_eq_false-unreach-call.c below 2 OKAY0.4
sum_non_eq_true-unreach-call.c below 2 PASS0.41
sum_non_false-unreach-call.c below 2 OKAY0.407
sum_non_true-unreach-call.c below 2 PASS0.415
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5426.873
/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.41
rec-bhmr2007_true-unreach-call.c below 2 PASS0.399
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.61
rec-cggmp2005_true-unreach-call.c below 2 PASS0.376
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.414
rec-css2003_true-unreach-call.c below 2 PASS0.965
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.058
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.726
rec-gj2007b_true-unreach-call.c below 2 FAIL0.375
rec-gj2007_true-unreach-call.c below 2 FAIL0.44
rec-gr2006_true-unreach-call.c below 2 FAIL0.459
rec-gsv2008_true-unreach-call.c below 2 PASS0.445
rec-hhk2008_true-unreach-call.c below 2 PASS0.367
rec-jm2006_true-unreach-call.c below 2 PASS0.444
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.488
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.398
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.374
/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.363
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.383
rec-count_by_2_true-unreach-call.c below 2 PASS0.348
rec-count_by_k_true-unreach-call.c below 2 PASS0.379
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.403
rec-gauss_sum_true-unreach-call.c below 2 PASS0.401
rec-half_true-unreach-call.c below 2 FAIL0.387
rec-nested_true-unreach-call.c below 3 FAIL0.511
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.175
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.509
cubic_polynomial_unsafe.c below 2 OKAY0.488
edit_distance_bottom_up.c below 3 FAIL117.612
edit_distance_top_down.c below 3 FAIL2.642
log_log_n_solution.c below 3 FAIL0.426
log_log_n_solution_unsafe.c below 3 OKAY0.424
log_n_solution.c below 2 FAIL0.447
log_n_solution_unsafe.c below 2 OKAY0.422
multivariate_1.c below TIMEOUT 300.004
multivariate_1_unsafe.c below TIMEOUT 300.004
multivariate_higher_order.c below 7 FAIL19.007
multivariate_higher_order_unsafe.c below 7 OKAY18.82
n_cubed_solution.c below EXCEPTION 45.587
n_cubed_solution_unsafe.c below EXCEPTION 0.024
n_log_n_solution.c below TIMEOUT 300.05
n_log_n_solution_unsafe.c below TIMEOUT 300.045
n_squared_two_base_case_even.c below 2 PASS0.471
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.479
n_squared_two_base_case_odd.c below 2 PASS0.47
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.471
pascals_dynamic.c below 3 FAIL2.372
pascals_dynamic_unsafe.c below 3 OKAY2.454
pascals_iterative.c below 1 FAIL3.475
pascals_iterative_unsafe.c below 1 OKAY3.476
pascals_recursive.c below 8 FAIL9.615
pascals_recursive_unsafe.c below 8 OKAY9.514
squared_solution.c below TIMEOUT 300.004
squared_solution_unsafe.c below TIMEOUT 300.004
two_n_even.c below 2 PASS0.395
two_n_even_unsafe.c below 2 OKAY0.42
two_n_odd.c below 2 PASS0.399
two_n_odd_unsafe.c below 2 OKAY0.406
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.004
two_to_n_over_two_odd_unsafe.c below TIMEOUT 300.004
two_to_n_squared.c below 8 FAIL20.565
two_to_n_squared_unsafe.c below 8 OKAY20.879
two_to_two_to_n.c below 7 FAIL0.826
two_to_two_to_n_unsafe.c below 7 OKAY0.811
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 13/19
ICRA Time = 3284.033
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.349
adding_and_mult_unsafe.c below 1 OKAY0.368
binary_search_array_tree.c below 1 FAIL0.608
exp_add_linear.c below 1 PASS0.417
exp_add_linear_unsafe.c below 1 OKAY0.434
exp_add_loop_rec.c below 1 FAIL0.368
exp_add_loop_rec_unsafe.c below 1 OKAY0.363
exp_add_loop_variable.c below 1 PASS0.412
exp_add_loop_variable_unsafe.c below 1 OKAY0.403
exp_with_linear_inner_loop.c below 1 FAIL0.466
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.466
halving_log1.c below 1 FAIL0.503
linear_two_to_n.c below 8 FAIL1.076
linear_two_to_n_unsafe.c below 8 OKAY1.069
loop_five_to_n.c below 1 PASS0.394
loop_five_to_n_unsafe.c below 1 OKAY0.393
non_loop_five_to_n.c below TIMEOUT 300.031
non_loop_five_to_n_unsafe.c below TIMEOUT 300.027
power_log.c below 1 PASS0.46
power_log_modified.c below 1 PASS0.489
simple_exponential.c below 1 PASS0.382
simple_exponential_for.c below 1 PASS0.395
simple_exponential_for_unsafe.c below 1 OKAY0.396
simple_exponential_unsafe.c below 1 OKAY0.368
two_to_n_minus_n.c below 7 FAIL1.115
two_to_n_minus_n_loop.c below 7 FAIL1.606
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.613
two_to_n_minus_n_unsafe.c below 7 OKAY1.142
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 616.113