[Version Information]
WALi-OpenNWA version: 97ff72fc319b11f39abbceff5a35ed182ebe8e82 (2017-06-26 12:47:30 -0400) "CoFloCo benchmarks"
duet version: b5786c2400b4b2dc8f5ecf16bd9d2656de3c6f47 (2017-06-27 22:28:06 -0400) "Merge remote-tracking branch 'origin/ark2' 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-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.403
kmp.c below 1 PASS0.725
qsort.c below 7 PASS1.427
speed_pldi09_fig1.c below 1 PASS0.377
speed_pldi09_fig4_2.c below 1 FAIL0.377
speed_pldi09_fig4_4.c below 1 PASS0.434
speed_pldi09_fig4_5.c below 1 PASS0.355
speed_pldi10_ex1.c below 1 PASS2.023
speed_pldi10_ex3.c below 1 PASS0.436
speed_pldi10_ex4.c below 1 PASS0.42
speed_popl10_fig2_1.c below 1 PASS0.383
speed_popl10_fig2_2.c below 1 FAIL0.356
speed_popl10_nested_multiple.c below 1 PASS0.429
speed_popl10_nested_single.c below 1 PASS0.391
speed_popl10_sequential_single.c below 1 PASS0.359
speed_popl10_simple_multiple.c below 1 PASS0.369
speed_popl10_simple_single_2.c below 1 PASS0.424
speed_popl10_simple_single.c below 1 PASS0.339
t07.c below 1 PASS0.363
t08.c below 1 PASS0.363
t09.c below 1 PASS0.357
t10.c below 1 PASS0.356
t11.c below 1 PASS0.378
t13.c below 1 FAIL0.377
t15.c below 1 PASS0.4
t16.c below 1 PASS0.378
t19.c below 1 PASS0.342
t20.c below 1 PASS0.349
t27.c below 1 PASS0.407
t28.c below 1 PASS0.392
t30.c below 1 FAIL0.357
t37.c below 2 PASS0.425
t39.c below 2 PASS0.431
t46.c below 1 PASS0.349
t47.c below 1 PASS0.355
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 16.406
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.359
qsort_full.c below 4 PASS8.832
rec1-param_safe.c below 2 PASS0.361
rec1-param_unsafe.c below 2 OKAY0.367
rec1_safe.c below 2 PASS0.346
rec1_unsafe.c below 2 OKAY0.413
rec2-param_safe.c below 2 PASS0.571
rec2-param_unsafe.c below 2 OKAY0.35
rec2_safe.c below 2 PASS0.575
rec2_unsafe.c below 2 OKAY0.363
rec-test.c below 2 PASS0.421
sas03_bothbranches.c below 7 PASS0.518
sas03.c below 2 PASS0.879
simulated_lese_recursive.c below 2 PASS0.486
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 14.841
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.335
count_up_down_unsafe.c below 1 OKAY0.337
divide.c below 1 PASS0.348
factor_unsafe.c below 1 OKAY0.453
for_infinite_loop_1_safe.c below 1 PASS0.366
for_infinite_loop_2_safe.c below 1 PASS0.327
interproc.c below 1 PASS0.349
mult.c below 1 PASS0.342
pointer_arith.c below 1 PASS0.46
quotient.c below 3 PASS0.413
subtract.c below 1 PASS0.342
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.352
sum01_bug02_unsafe.c below 1 OKAY0.402
sum01_real_safe.c below 1 PASS0.468
sum01_safe.c below 1 PASS0.329
sum01_unsafe.c below 1 OKAY0.368
sum02_safe.c below 1 PASS0.341
sum03_safe.c below 1 PASS0.566
sum03_unsafe.c below 1 OKAY0.383
sum04_safe.c below 1 PASS0.337
sum04_unsafe.c below 1 OKAY0.367
terminator_02_safe.c below 1 PASS0.557
terminator_02_unsafe.c below 1 OKAY0.359
terminator_03_safe.c below 1 PASS0.506
terminator_03_unsafe.c below 1 OKAY0.411
token_ring01_safe.c below 4 FAIL158.053
token_ring01_unsafe.c below 4 OKAY120.861
toy_safe.c below EXCEPTION 196.943
trex01_safe.c below 1 PASS0.55
trex01_unsafe.c below 1 OKAY0.37
trex02_safe2.c below 3 PASS0.387
trex02_safe.c below 3 PASS0.382
trex02_unsafe.c below 3 OKAY0.38
trex03_safe.c below 1 PASS0.434
trex03_unsafe.c below 1 OKAY0.493
trex04_safe.c below 1 PASS0.352
while_infinite_loop_1_safe.c below 1 PASS0.307
while_infinite_loop_2_safe.c below 1 PASS0.322
while_infinite_loop_3_safe.c below 1 PASS0.334
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 489.986
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.38
blogger_simplified1.c below 3 PASS0.736
divided_difference2.c below TIMEOUT 300.006
mult-proc.c below 3 PASS0.352
mult-proc-params.c below 3 PASS0.364
popall.c below 1 PASS0.401
simulated_scc.c below 1 PASS0.457
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 302.696
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.341
degree2_binomial.c below 1 PASS0.461
degree2_monomial.c below 1 PASS0.373
degree3_binomial.c below EXCEPTION 0.597
degree3_monomial.c below 1 PASS0.394
degree4_binomial.c below EXCEPTION 0.603
degree4_monomial.c below 1 PASS0.444
degree5_binomial.c below EXCEPTION 0.668
degree5_monomial.c below 1 PASS0.498
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 4.379
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below EXCEPTION 0.344
cubic_with_square_interproc.c below EXCEPTION 0.349
cubic_with_square_nonlinear.c below EXCEPTION 0.336
cubic_with_square_nonlinear_interproc.c below EXCEPTION 0.341
cubic_with_square_nonlinear_unsafe.c below EXCEPTION 0.333
cubic_with_square_unsafe.c below EXCEPTION 0.34
multi-input.c below EXCEPTION 0.377
multi-input_unsafe.c below EXCEPTION 0.366
nondet_loop_bound.c below EXCEPTION 0.329
nondet_loop_bound_quartic.c below EXCEPTION 0.341
nondet_loop_bound_quartic_unsafe.c below EXCEPTION 0.335
nondet_loop_bound_unsafe.c below EXCEPTION 0.337
nonlinear_stratified.c below EXCEPTION 0.34
nonlinear_stratified_unsafe.c below EXCEPTION 0.362
quartic_with_cube.c below EXCEPTION 0.347
quartic_with_cube_nonlinear.c below EXCEPTION 0.358
quartic_with_cube_nonlinear_unsafe.c below EXCEPTION 0.347
quartic_with_cube_unsafe.c below 1 OKAY0.375
quintic_with_quartic.c below EXCEPTION 0.346
quintic_with_quartic_nonlinear.c below EXCEPTION 0.324
quintic_with_quartic_nonlinear_unsafe.c below EXCEPTION 0.327
quintic_with_quartic_unsafe.c below EXCEPTION 0.362
ICRA Assertions (True) = 0/12
ICRA Assertions (False) = 1/10
ICRA Time = 7.616
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.477
degree2_FD_AllAux_AllAssm.c below 1 PASS2.052
degree2_FD_AllAux_FewAssm.c below 1 PASS5.752
degree2_FD_FewAux_FewAssm.c below 1 PASS0.602
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.607
degree3.c below 1 PASS0.493
degree3_FD.c below 1 PASS0.614
degree4.c below 1 PASS0.401
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 10.998
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.411
loop_unsafe.c below 1 OKAY0.427
simulated_lese_parser.c below 1 PASS0.33
simulated_lese_sentinel.c below 1 PASS0.336
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.504
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.352
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.352
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.005
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.005
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.333
array_false-unreach-call2.c below 1 OKAY0.349
array_false-unreach-call3.c below 1 OKAY0.35
array_true-unreach-call1.c below 1 FAIL0.34
array_true-unreach-call2.c below 1 FAIL0.374
array_true-unreach-call3.c below 1 PASS0.34
array_true-unreach-call4.c below 1 FAIL0.363
const_false-unreach-call1.c below 1 OKAY0.343
const_true-unreach-call1.c below 1 PASS0.321
diamond_false-unreach-call1.c below 1 OKAY0.357
diamond_true-unreach-call1.c below 1 PASS0.34
diamond_true-unreach-call2.c below 1 PASS0.363
functions_false-unreach-call1.c below 3 OKAY0.358
functions_true-unreach-call1.c below 3 PASS0.363
multivar_false-unreach-call1.c below 1 OKAY0.329
multivar_true-unreach-call1.c below 1 PASS0.338
nested_false-unreach-call1.c below 1 OKAY0.33
nested_true-unreach-call1.c below 1 PASS0.333
overflow_true-unreach-call1.c below 1 PASS0.316
phases_false-unreach-call1.c below 1 OKAY0.344
phases_false-unreach-call2.c below 1 OKAY0.339
phases_true-unreach-call1.c below 1 PASS0.354
phases_true-unreach-call2.c below 1 PASS0.364
simple_false-unreach-call1.c below 1 OKAY0.301
simple_false-unreach-call2.c below 1 OKAY0.323
simple_false-unreach-call3.c below 1 OKAY0.339
simple_false-unreach-call4.c below 1 OKAY0.331
simple_true-unreach-call1.c below 1 PASS0.333
simple_true-unreach-call2.c below 1 PASS0.324
simple_true-unreach-call3.c below 1 PASS0.316
simple_true-unreach-call4.c below 1 PASS0.313
underapprox_false-unreach-call1.c below 1 OKAY0.34
underapprox_false-unreach-call2.c below 1 OKAY0.346
underapprox_true-unreach-call1.c below 1 FAIL0.339
underapprox_true-unreach-call2.c below 1 PASS0.325
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 11.871
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.796
apache-get-tag_true-unreach-call.c below 1 FAIL0.431
down_true-unreach-call.c below 1 PASS0.331
fragtest_simple_true-unreach-call.c below 1 PASS0.369
half_2_true-unreach-call.c below 1 PASS0.348
heapsort_true-unreach-call.c below 1 PASS2.508
id_build_true-unreach-call.c below 1 PASS0.353
id_trans_false-unreach-call.c below 1 OKAY0.342
large_const_true-unreach-call.c below 1 PASS0.412
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.367
nested6_true-unreach-call.c below 1 FAIL0.405
nested9_true-unreach-call.c below 1 PASS0.44
nest-if3_true-unreach-call.c below 1 PASS0.394
NetBSD_loop_true-unreach-call.c below 1 PASS0.347
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.38
seq_true-unreach-call.c below 1 PASS0.381
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.004
string_concat-noarr_true-unreach-call.c below 1 PASS0.371
up_true-unreach-call.c below 1 PASS0.341
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 309.32
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.351
bhmr2007_true-unreach-call.c below 1 PASS0.367
cggmp2005b_true-unreach-call.c below 1 PASS0.39
cggmp2005_true-unreach-call.c below 1 PASS0.328
cggmp2005_variant_true-unreach-call.c below 1 PASS0.33
css2003_true-unreach-call.c below 1 PASS0.439
ddlm2013_true-unreach-call.c below 1 PASS0.385
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.031
gj2007b_true-unreach-call.c below 1 FAIL0.368
gj2007_true-unreach-call.c below 1 PASS0.353
gr2006_true-unreach-call.c below 1 PASS0.348
gsv2008_true-unreach-call.c below 1 PASS0.337
hhk2008_true-unreach-call.c below 1 PASS0.356
jm2006_true-unreach-call.c below 1 PASS0.354
jm2006_variant_true-unreach-call.c below 1 PASS0.367
mcmillan2006_true-unreach-call.c below 1 FAIL0.378
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.482
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.33
count_by_1_variant_true-unreach-call.c below 1 PASS0.336
count_by_2_true-unreach-call.c below 1 PASS0.333
count_by_k_true-unreach-call.c below 1 PASS0.331
count_by_nondet_true-unreach-call.c below 1 FAIL0.358
gauss_sum_true-unreach-call.c below 1 PASS0.346
half_true-unreach-call.c below EXCEPTION 0.341
nested_true-unreach-call.c below 1 PASS0.382
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.757
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.38
array_true-unreach-call.c below 1 FAIL0.381
bubble_sort_false-unreach-call.c below 4 OKAY77.553
bubble_sort_true-unreach-call.c below 1 PASS1.261
compact_false-unreach-call.c below 1 OKAY0.36
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.335
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.346
eureka_01_false-unreach-call.c below 1 OKAY1.438
eureka_01_true-unreach-call.c below 1 FAIL1.295
eureka_05_true-unreach-call.c below 1 PASS0.54
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.342
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.333
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.329
heavy_false-unreach-call.c below 1 OKAY0.428
heavy_true-unreach-call.c below 1 PASS0.445
insertion_sort_false-unreach-call.c below 1 OKAY0.959
insertion_sort_true-unreach-call.c below 1 FAIL0.577
invert_string_false-unreach-call.c below 1 OKAY0.455
invert_string_true-unreach-call.c below 1 FAIL0.462
linear_sea.ch_true-unreach-call.c below 1 FAIL0.375
linear_search_false-unreach-call.c below 1 UNSOUND0.424
lu.cmp_true-unreach-call.c below 3 PASS9.333
ludcmp_false-unreach-call.c below 3 OKAY9.643
matrix_false-unreach-call_true-termination.c below 1 OKAY0.547
matrix_true-unreach-call_true-termination.c below 1 FAIL0.403
n.c11_true-unreach-call.c below 3 FAIL0.414
n.c24_false-unreach-call.c below 3 OKAY2.542
n.c40_true-unreach-call.c below 1 FAIL0.345
nec11_false-unreach-call.c below 1 OKAY0.343
nec20_false-unreach-call.c below 1 OKAY0.389
nec40_true-unreach-call.c below 1 FAIL0.358
string_false-unreach-call.c below 1 OKAY0.651
string_true-unreach-call.c below 1 FAIL0.643
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.383
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.35
sum01_false-unreach-call_true-termination.c below 1 OKAY0.37
sum01_true-unreach-call_true-termination.c below 1 PASS0.346
sum03_false-unreach-call_true-termination.c below 1 OKAY0.425
sum03_true-unreach-call_false-termination.c below 1 PASS0.366
sum04_false-unreach-call_true-termination.c below 1 OKAY0.368
sum04_true-unreach-call_true-termination.c below 1 PASS0.322
sum_array_false-unreach-call.c below 1 OKAY0.517
sum_array_true-unreach-call.c below 1 FAIL0.568
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.325
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.406
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.351
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.332
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.331
trex01_false-unreach-call_true-termination.c below 3 OKAY0.447
trex01_true-unreach-call.c below 3 PASS0.773
trex02_false-unreach-call_true-termination.c below 3 OKAY0.373
trex02_true-unreach-call_true-termination.c below 3 PASS0.386
trex03_false-unreach-call_true-termination.c below 3 OKAY0.677
trex03_true-unreach-call.c below 3 PASS0.642
trex04_true-unreach-call_false-termination.c below 1 PASS0.404
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.342
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS4.032
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.356
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.362
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY3.106
vogal_false-unreach-call.c below 1 OKAY0.691
vogal_true-unreach-call.c below 1 FAIL0.673
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.331
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.335
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.326
ICRA Assertions (True) = 22/34
ICRA Assertions (False) = 31/32
ICRA Time = 134.978
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.948
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.905
Ackermann03_true-unreach-call.c below 7 FAIL0.932
Ackermann04_true-unreach-call.c below 7 FAIL0.939
Addition01_true-unreach-call_true-termination.c below 2 PASS0.443
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.445
Addition03_false-no-overflow.c below 2 PASS0.448
Addition03_true-unreach-call.c below 2 PASS0.463
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.382
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.4
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.39
Fibonacci01_true-unreach-call.c below EXCEPTION 0.691
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.601
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 0.618
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 0.634
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 0.722
gcd01_true-unreach-call_true-termination.c below 2 PASS0.439
gcd02_true-unreach-call.c below 2 FAIL0.691
McCarthy91_false-unreach-call_false-termination.c below 8 OKAY3.052
McCarthy91_true-unreach-call.c below 8 FAIL3.127
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.445
Primes_true-unreach-call.c below 3 FAIL0.97
recHanoi01_true-unreach-call_true-termination.c below EXCEPTION 0.5
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.358
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.36
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 19.903
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.382
afterrec_2calls_true-unreach-call.c below 2 PASS0.376
afterrec_false-unreach-call.c below 2 OKAY0.352
afterrec_true-unreach-call.c below 2 PASS0.353
fibo_10_false-unreach-call.c below EXCEPTION 0.662
fibo_10_true-unreach-call.c below EXCEPTION 0.68
fibo_15_false-unreach-call.c below EXCEPTION 0.661
fibo_15_true-unreach-call.c below EXCEPTION 0.664
fibo_20_false-unreach-call.c below EXCEPTION 0.62
fibo_20_true-unreach-call.c below EXCEPTION 0.644
fibo_25_false-unreach-call.c below EXCEPTION 0.654
fibo_25_true-unreach-call.c below EXCEPTION 0.674
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.021
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.016
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.017
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.009
fibo_5_false-unreach-call.c below EXCEPTION 0.669
fibo_5_true-unreach-call.c below EXCEPTION 0.651
fibo_7_false-unreach-call.c below EXCEPTION 0.671
fibo_7_true-unreach-call.c below EXCEPTION 0.685
id2_b2_o3_true-unreach-call.c below 2 PASS0.56
id2_b3_o2_false-unreach-call.c below 2 OKAY0.563
id2_b3_o5_true-unreach-call.c below 2 PASS0.564
id2_b5_o10_true-unreach-call.c below 2 PASS0.525
id2_i5_o5_false-unreach-call.c below 2 OKAY0.394
id2_i5_o5_true-unreach-call.c below 2 PASS0.385
id_b2_o3_true-unreach-call.c below 2 PASS0.446
id_b3_o2_false-unreach-call.c below 2 OKAY0.463
id_b3_o5_true-unreach-call.c below 2 PASS0.44
id_b5_o10_true-unreach-call.c below 2 PASS0.448
id_i10_o10_false-unreach-call.c below 2 OKAY0.381
id_i10_o10_true-unreach-call.c below 2 PASS0.369
id_i15_o15_false-unreach-call.c below 2 OKAY0.368
id_i15_o15_true-unreach-call.c below 2 PASS0.417
id_i20_o20_false-unreach-call.c below 2 OKAY0.381
id_i20_o20_true-unreach-call.c below 2 PASS0.376
id_i25_o25_false-unreach-call.c below 2 OKAY0.37
id_i25_o25_true-unreach-call.c below 2 PASS0.365
id_i5_o5_false-unreach-call.c below 2 OKAY0.369
id_i5_o5_true-unreach-call.c below 2 PASS0.362
id_o1000_false-unreach-call.c below 2 OKAY0.365
id_o100_false-unreach-call.c below 2 OKAY0.381
id_o10_false-unreach-call.c below 2 OKAY0.368
id_o200_false-unreach-call.c below 2 OKAY0.371
id_o20_false-unreach-call.c below 2 OKAY0.374
id_o3_false-unreach-call.c below 2 OKAY0.36
sum_10x0_false-unreach-call.c below 2 OKAY0.382
sum_10x0_true-unreach-call.c below 2 PASS0.383
sum_15x0_false-unreach-call.c below 2 OKAY0.352
sum_15x0_true-unreach-call.c below 2 PASS0.385
sum_20x0_false-unreach-call.c below 2 OKAY0.377
sum_20x0_true-unreach-call.c below 2 PASS0.364
sum_25x0_false-unreach-call.c below 2 OKAY0.375
sum_25x0_true-unreach-call.c below 2 PASS0.376
sum_2x3_false-unreach-call.c below 2 OKAY0.378
sum_2x3_true-unreach-call.c below 2 PASS0.355
sum_non_eq_false-unreach-call.c below 2 OKAY0.376
sum_non_eq_true-unreach-call.c below 2 PASS0.37
sum_non_false-unreach-call.c below 2 OKAY0.376
sum_non_true-unreach-call.c below 2 PASS0.365
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 5425.56
/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.369
rec-bhmr2007_true-unreach-call.c below 2 PASS0.387
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.508
rec-cggmp2005_true-unreach-call.c below 2 PASS0.345
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.345
rec-css2003_true-unreach-call.c below 2 PASS0.545
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.327
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.617
rec-gj2007b_true-unreach-call.c below 2 FAIL0.373
rec-gj2007_true-unreach-call.c below 2 FAIL0.382
rec-gr2006_true-unreach-call.c below 2 FAIL0.375
rec-gsv2008_true-unreach-call.c below 2 PASS0.35
rec-hhk2008_true-unreach-call.c below 2 PASS0.373
rec-jm2006_true-unreach-call.c below 2 PASS0.384
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.394
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.416
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 6.49
/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.344
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.369
rec-count_by_2_true-unreach-call.c below 2 PASS0.351
rec-count_by_k_true-unreach-call.c below 2 PASS0.376
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.384
rec-gauss_sum_true-unreach-call.c below 2 PASS0.372
rec-half_true-unreach-call.c below EXCEPTION 0.351
rec-nested_true-unreach-call.c below 3 PASS0.471
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.018
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below EXCEPTION 0.371
edit_distance_bottom_up.c below 3 FAIL32.384
edit_distance_top_down.c below 3 FAIL2.535
log_log_n_solution.c below 3 FAIL0.401
log_n_solution.c below 2 FAIL0.397
multivariate_1.c below TIMEOUT 300.008
multivariate_higher_order.c below 7 FAIL1.545
n_cubed_solution.c below EXCEPTION 0.368
n_log_n_solution.c below TIMEOUT 300.096
n_squared_two_base_case_even.c below 2 PASS0.377
n_squared_two_base_case_odd.c below 2 PASS0.372
pascals_dynamic.c below 3 FAIL2.276
pascals_iterative.c below 1 FAIL1.342
pascals_recursive.c below EXCEPTION 0.459
squared_solution.c below TIMEOUT 300.029
two_n_even.c below 2 PASS0.387
two_n_odd.c below 2 PASS0.368
two_to_n_over_two_even.c below EXCEPTION 0.641
two_to_n_over_two_odd.c below EXCEPTION 0.649
two_to_n_squared.c below 5 FAIL10.153
two_to_two_to_n.c below 7 FAIL0.814
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 0/0
ICRA Time = 955.972
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.333
binary_search_array_tree.c below 1 FAIL0.922
exp_add_loop_rec.c below 1 FAIL0.35
exp_add_loop_variable.c below 1 PASS0.36
exp_with_linear_inner_loop.c below 1 FAIL0.422
halving_log1.c below 1 FAIL0.434
linear_two_to_n.c below 8 FAIL5.246
loop_five_to_n.c below 1 FAIL0.346
non_loop_five_to_n.c below EXCEPTION 0.625
power_log.c below 1 PASS0.403
power_log_modified.c below 1 PASS0.458
simple_exponential.c below 1 PASS0.376
simple_exponential_for.c below 1 PASS0.349
two_to_n_minus_n.c below EXCEPTION 0.489
two_to_n_minus_n_loop.c below EXCEPTION 0.557
ICRA Assertions (True) = 6/15
ICRA Assertions (False) = 0/0
ICRA Time = 11.67