[Version Information]
WALi-OpenNWA version: 97ff72fc319b11f39abbceff5a35ed182ebe8e82 (2017-06-26 12:47:30 -0400) "CoFloCo benchmarks"
duet version: 034a8aab77caebb54aa247239a77fa54e14e64da (2017-06-30 07:15:46 -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.363
kmp.c below 1 PASS0.99
qsort.c below 2 PASS0.57
speed_pldi09_fig1.c below 1 PASS0.496
speed_pldi09_fig4_2.c below 1 PASS0.393
speed_pldi09_fig4_4.c below 1 PASS20.852
speed_pldi09_fig4_5.c below 1 PASS0.404
speed_pldi10_ex1.c below 1 PASS1.221
speed_pldi10_ex3.c below 1 PASS0.521
speed_pldi10_ex4.c below 1 PASS0.45
speed_popl10_fig2_1.c below 1 PASS0.467
speed_popl10_fig2_2.c below 1 PASS0.365
speed_popl10_nested_multiple.c below 1 PASS0.456
speed_popl10_nested_single.c below 1 PASS0.411
speed_popl10_sequential_single.c below 1 PASS0.391
speed_popl10_simple_multiple.c below 1 PASS0.508
speed_popl10_simple_single_2.c below 1 PASS0.6
speed_popl10_simple_single.c below 1 PASS0.365
t07.c below 1 PASS0.424
t08.c below 1 PASS0.398
t09.c below 1 PASS0.376
t10.c below 1 PASS0.363
t11.c below 1 PASS0.47
t13.c below 1 PASS0.415
t15.c below 1 PASS0.427
t16.c below 1 PASS0.417
t19.c below 1 PASS0.395
t20.c below 1 PASS0.384
t27.c below 1 PASS0.539
t28.c below 1 PASS0.467
t30.c below 1 FAIL0.446
t37.c below 2 PASS0.601
t39.c below 2 PASS0.546
t46.c below 1 PASS0.418
t47.c below 1 PASS0.531
ICRA Assertions (True) = 33/35
ICRA Assertions (False) = 0/0
ICRA Time = 37.44
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.36
qsort_full.c below 2 PASS3.037
rec1-param_safe.c below 2 PASS0.375
rec1-param_unsafe.c below 2 OKAY0.388
rec1_safe.c below 2 PASS0.364
rec1_unsafe.c below 2 OKAY0.378
rec2-param_safe.c below 2 PASS0.361
rec2-param_unsafe.c below 2 OKAY0.389
rec2_safe.c below 2 PASS0.378
rec2_unsafe.c below 2 OKAY0.369
rec-test.c below 2 PASS0.372
sas03_bothbranches.c below 2 PASS0.404
sas03.c below 2 PASS0.737
simulated_lese_recursive.c below 2 PASS0.445
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 8.357
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.326
count_up_down_unsafe.c below 1 OKAY0.349
divide.c below 1 PASS0.338
factor_unsafe.c below 1 OKAY0.328
for_infinite_loop_1_safe.c below 1 PASS0.319
for_infinite_loop_2_safe.c below 1 PASS0.331
interproc.c below 1 PASS0.313
mult.c below 1 PASS0.328
pointer_arith.c below 1 PASS0.298
quotient.c below 3 PASS0.502
subtract.c below 1 PASS0.327
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.336
sum01_bug02_unsafe.c below 1 UNSOUND0.532
sum01_real_safe.c below 1 PASS0.341
sum01_safe.c below 1 PASS0.347
sum01_unsafe.c below 1 UNSOUND0.441
sum02_safe.c below 1 PASS0.35
sum03_safe.c below 1 PASS0.385
sum03_unsafe.c below 1 UNSOUND0.441
sum04_safe.c below 1 PASS0.338
sum04_unsafe.c below 1 UNSOUND0.439
terminator_02_safe.c below 1 PASS0.341
terminator_02_unsafe.c below 1 OKAY0.371
terminator_03_safe.c below 1 PASS0.333
terminator_03_unsafe.c below 1 OKAY0.319
token_ring01_safe.c below 4 PASS81.394
token_ring01_unsafe.c below 4 UNSOUND116.626
toy_safe.c below EXCEPTION 164.461
trex01_safe.c below 1 PASS0.677
trex01_unsafe.c below 1 OKAY0.363
trex02_safe2.c below 2 PASS0.356
trex02_safe.c below 2 PASS0.351
trex02_unsafe.c below 2 OKAY0.366
trex03_safe.c below 1 PASS0.409
trex03_unsafe.c below 1 OKAY0.427
trex04_safe.c below 1 PASS0.354
while_infinite_loop_1_safe.c below 1 PASS0.302
while_infinite_loop_2_safe.c below 1 PASS0.367
while_infinite_loop_3_safe.c below 1 PASS0.3
ICRA Assertions (True) = 25/26
ICRA Assertions (False) = 8/13
ICRA Time = 375.826
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.388
blogger_simplified1.c below 3 PASS1.067
divided_difference2.c below TIMEOUT 300.009
mult-proc.c below 3 PASS0.367
mult-proc-params.c below 3 PASS0.394
popall.c below 1 PASS0.658
simulated_scc.c below 1 PASS0.643
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.526
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.357
degree2_binomial.c below 1 PASS0.677
degree2_monomial.c below 1 PASS0.389
degree3_binomial.c below 1 PASS1.285
degree3_monomial.c below 1 PASS0.453
degree4_binomial.c below 1 PASS1.508
degree4_monomial.c below 1 PASS0.561
degree5_binomial.c below 1 PASS1.927
degree5_monomial.c below 1 PASS0.677
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 7.834
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.437
cubic_with_square_interproc.c below 2 PASS0.543
cubic_with_square_nonlinear.c below 1 PASS0.362
cubic_with_square_nonlinear_interproc.c below 2 PASS0.4
cubic_with_square_nonlinear_unsafe.c below 1 UNSOUND0.388
cubic_with_square_unsafe.c below 1 UNSOUND0.433
multi-input.c below 1 PASS0.437
multi-input_unsafe.c below 1 UNSOUND0.418
nondet_loop_bound.c below 1 PASS0.356
nondet_loop_bound_quartic.c below 1 PASS0.372
nondet_loop_bound_quartic_unsafe.c below 1 UNSOUND0.351
nondet_loop_bound_unsafe.c below 1 OKAY0.359
nonlinear_stratified.c below 1 TIMEOUT300.004
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube.c below 1 PASS0.588
quartic_with_cube_nonlinear.c below 1 PASS0.387
quartic_with_cube_nonlinear_unsafe.c below 1 UNSOUND0.384
quartic_with_cube_unsafe.c below 1 UNSOUND0.483
quintic_with_quartic.c below 1 PASS0.987
quintic_with_quartic_nonlinear.c below 1 PASS0.482
quintic_with_quartic_nonlinear_unsafe.c below 1 UNSOUND0.427
quintic_with_quartic_unsafe.c below 1 UNSOUND0.985
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 1/10
ICRA Time = 609.587
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.679
degree2_FD_AllAux_AllAssm.c below 1 PASS6.572
degree2_FD_AllAux_FewAssm.c below 1 PASS5.284
degree2_FD_FewAux_FewAssm.c below 1 PASS0.87
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.922
degree3.c below 1 PASS0.631
degree3_FD.c below 1 PASS0.8
degree4.c below 1 PASS0.432
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 16.19
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.425
loop_unsafe.c below 1 UNSOUND0.428
simulated_lese_parser.c below 1 PASS0.351
simulated_lese_sentinel.c below 1 PASS0.353
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 0/1
ICRA Time = 1.557
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.347
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.347
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.027
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.027
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 UNSOUND0.345
array_false-unreach-call2.c below 1 UNSOUND0.35
array_false-unreach-call3.c below 1 UNSOUND0.348
array_true-unreach-call1.c below 1 PASS0.343
array_true-unreach-call2.c below 1 PASS0.359
array_true-unreach-call3.c below 1 PASS0.354
array_true-unreach-call4.c below 1 FAIL0.342
const_false-unreach-call1.c below 1 UNSOUND0.332
const_true-unreach-call1.c below 1 PASS0.352
diamond_false-unreach-call1.c below 1 UNSOUND0.387
diamond_true-unreach-call1.c below 1 PASS0.371
diamond_true-unreach-call2.c below 1 PASS0.377
functions_false-unreach-call1.c below 3 OKAY0.377
functions_true-unreach-call1.c below 3 PASS0.368
multivar_false-unreach-call1.c below 1 OKAY0.373
multivar_true-unreach-call1.c below 1 PASS0.335
nested_false-unreach-call1.c below 1 UNSOUND0.33
nested_true-unreach-call1.c below 1 PASS0.335
overflow_true-unreach-call1.c below 1 PASS0.318
phases_false-unreach-call1.c below 1 UNSOUND0.397
phases_false-unreach-call2.c below 1 OKAY0.33
phases_true-unreach-call1.c below 1 PASS0.396
phases_true-unreach-call2.c below 1 PASS0.346
simple_false-unreach-call1.c below 1 UNSOUND0.323
simple_false-unreach-call2.c below 1 OKAY0.32
simple_false-unreach-call3.c below 1 OKAY0.325
simple_false-unreach-call4.c below 1 UNSOUND0.323
simple_true-unreach-call1.c below 1 PASS0.333
simple_true-unreach-call2.c below 1 PASS0.32
simple_true-unreach-call3.c below 1 PASS0.327
simple_true-unreach-call4.c below 1 PASS0.33
underapprox_false-unreach-call1.c below 1 UNSOUND0.343
underapprox_false-unreach-call2.c below 1 UNSOUND0.337
underapprox_true-unreach-call1.c below 1 PASS0.338
underapprox_true-unreach-call2.c below 1 PASS0.335
ICRA Assertions (True) = 18/19
ICRA Assertions (False) = 5/16
ICRA Time = 12.119
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.818
apache-get-tag_true-unreach-call.c below 1 FAIL0.431
down_true-unreach-call.c below 1 PASS0.387
fragtest_simple_true-unreach-call.c below 1 PASS0.437
half_2_true-unreach-call.c below 1 PASS0.386
heapsort_true-unreach-call.c below 1 FAIL2.867
id_build_true-unreach-call.c below 1 PASS0.327
id_trans_false-unreach-call.c below 1 OKAY0.349
large_const_true-unreach-call.c below 1 PASS0.41
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.377
nested6_true-unreach-call.c below 1 PASS0.487
nested9_true-unreach-call.c below 1 PASS0.527
nest-if3_true-unreach-call.c below 1 PASS0.472
NetBSD_loop_true-unreach-call.c below 1 PASS0.346
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.388
seq_true-unreach-call.c below 1 PASS0.434
SpamAssassin-loop_true-unreach-call.c below 1 PASS0.958
string_concat-noarr_true-unreach-call.c below 1 PASS0.398
up_true-unreach-call.c below 1 PASS0.355
ICRA Assertions (True) = 15/18
ICRA Assertions (False) = 1/1
ICRA Time = 11.154
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.381
bhmr2007_true-unreach-call.c below 1 PASS0.374
cggmp2005b_true-unreach-call.c below 1 PASS0.441
cggmp2005_true-unreach-call.c below 1 PASS0.347
cggmp2005_variant_true-unreach-call.c below 1 PASS0.347
css2003_true-unreach-call.c below 1 PASS0.755
ddlm2013_true-unreach-call.c below 1 PASS0.48
gcnr2008_false-unreach-call.c below 1 OKAY0.87
gj2007b_true-unreach-call.c below 1 PASS0.364
gj2007_true-unreach-call.c below 1 PASS0.431
gr2006_true-unreach-call.c below 1 PASS0.425
gsv2008_true-unreach-call.c below 1 PASS0.343
hhk2008_true-unreach-call.c below 1 PASS0.349
jm2006_true-unreach-call.c below 1 PASS0.394
jm2006_variant_true-unreach-call.c below 1 PASS0.447
mcmillan2006_true-unreach-call.c below 1 FAIL0.376
ICRA Assertions (True) = 14/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.124
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.323
count_by_1_variant_true-unreach-call.c below 1 PASS0.373
count_by_2_true-unreach-call.c below 1 PASS0.321
count_by_k_true-unreach-call.c below 1 PASS0.33
count_by_nondet_true-unreach-call.c below 1 PASS0.355
gauss_sum_true-unreach-call.c below 1 PASS0.357
half_true-unreach-call.c below 1 PASS0.371
nested_true-unreach-call.c below 1 PASS0.419
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.849
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.379
array_true-unreach-call.c below 1 FAIL0.371
bubble_sort_false-unreach-call.c below 3 OKAY48.008
bubble_sort_true-unreach-call.c below 1 PASS3.638
compact_false-unreach-call.c below 1 UNSOUND0.384
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.343
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.342
eureka_01_false-unreach-call.c below 1 OKAY2.212
eureka_01_true-unreach-call.c below 1 PASS1.145
eureka_05_true-unreach-call.c below 1 PASS0.567
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.32
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.311
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.321
heavy_false-unreach-call.c below 1 UNSOUND0.388
heavy_true-unreach-call.c below 1 PASS0.39
insertion_sort_false-unreach-call.c below 1 UNSOUND1.191
insertion_sort_true-unreach-call.c below 1 FAIL0.548
invert_string_false-unreach-call.c below 1 OKAY0.533
invert_string_true-unreach-call.c below 1 PASS0.489
linear_sea.ch_true-unreach-call.c below 1 FAIL0.373
linear_search_false-unreach-call.c below 1 UNSOUND0.395
lu.cmp_true-unreach-call.c below 3 PASS10.405
ludcmp_false-unreach-call.c below 3 UNSOUND10.674
matrix_false-unreach-call_true-termination.c below 1 OKAY1.015
matrix_true-unreach-call_true-termination.c below 1 FAIL0.416
n.c11_true-unreach-call.c below 3 PASS0.418
n.c24_false-unreach-call.c below 3 UNSOUND2.516
n.c40_true-unreach-call.c below 1 FAIL0.354
nec11_false-unreach-call.c below 1 OKAY0.353
nec20_false-unreach-call.c below 1 UNSOUND0.378
nec40_true-unreach-call.c below 1 FAIL0.368
string_false-unreach-call.c below 1 UNSOUND0.53
string_true-unreach-call.c below 1 PASS0.506
sum01_bug02_false-unreach-call_true-termination.c below 1 UNSOUND0.545
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.339
sum01_false-unreach-call_true-termination.c below 1 UNSOUND0.438
sum01_true-unreach-call_true-termination.c below 1 PASS0.342
sum03_false-unreach-call_true-termination.c below 1 UNSOUND0.488
sum03_true-unreach-call_false-termination.c below 1 PASS0.426
sum04_false-unreach-call_true-termination.c below 1 UNSOUND0.456
sum04_true-unreach-call_true-termination.c below 1 PASS0.356
sum_array_false-unreach-call.c below 1 OKAY0.57
sum_array_true-unreach-call.c below 1 FAIL0.637
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.332
terminator_02_false-unreach-call_true-termination.c below 2 OKAY0.415
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.35
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.333
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.334
trex01_false-unreach-call_true-termination.c below 3 OKAY0.443
trex01_true-unreach-call.c below 3 PASS0.659
trex02_false-unreach-call_true-termination.c below 2 OKAY0.359
trex02_true-unreach-call_true-termination.c below 2 PASS0.38
trex03_false-unreach-call_true-termination.c below 2 OKAY0.584
trex03_true-unreach-call.c below 2 PASS0.537
trex04_true-unreach-call_false-termination.c below 1 PASS0.376
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.353
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.135
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.362
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.349
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 UNSOUND3.517
vogal_false-unreach-call.c below 1 UNSOUND0.603
vogal_true-unreach-call.c below 1 PASS0.597
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.306
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.302
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.308
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.309
ICRA Assertions (True) = 27/34
ICRA Assertions (False) = 18/32
ICRA Time = 112.421
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below EXCEPTION 0.959
Ackermann02_false-unreach-call_false-termination.c below EXCEPTION 0.935
Ackermann03_true-unreach-call.c below EXCEPTION 0.96
Ackermann04_true-unreach-call.c below EXCEPTION 0.958
Addition01_true-unreach-call_true-termination.c below 2 PASS0.533
Addition02_false-unreach-call_false-termination.c below 2 UNSOUND0.503
Addition03_false-no-overflow.c below 2 PASS0.509
Addition03_true-unreach-call.c below 2 PASS0.526
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.449
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.427
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.412
Fibonacci01_true-unreach-call.c below 9 FAIL0.735
Fibonacci02_true-unreach-call_true-termination.c below 9 FAIL0.743
Fibonacci03_true-unreach-call_true-termination.c below 9 FAIL0.762
Fibonacci04_false-unreach-call_true-termination.c below 9 OKAY0.722
Fibonacci05_false-unreach-call_true-termination.c below 9 OKAY0.725
gcd01_true-unreach-call_true-termination.c below 2 PASS0.516
gcd02_true-unreach-call.c below 2 FAIL0.897
McCarthy91_false-unreach-call_false-termination.c below 3 OKAY0.433
McCarthy91_true-unreach-call.c below 3 PASS0.445
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.549
Primes_true-unreach-call.c below 2 PASS1.145
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.288
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.356
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.369
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 5/7
ICRA Time = 16.856
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.412
afterrec_2calls_true-unreach-call.c below 2 PASS0.401
afterrec_false-unreach-call.c below 2 OKAY0.371
afterrec_true-unreach-call.c below 2 PASS0.364
fibo_10_false-unreach-call.c below 9 OKAY0.699
fibo_10_true-unreach-call.c below 9 FAIL0.712
fibo_15_false-unreach-call.c below 9 OKAY0.705
fibo_15_true-unreach-call.c below 9 FAIL0.73
fibo_20_false-unreach-call.c below 9 OKAY0.72
fibo_20_true-unreach-call.c below 9 FAIL0.719
fibo_25_false-unreach-call.c below 9 OKAY0.703
fibo_25_true-unreach-call.c below 9 FAIL0.773
fibo_2calls_10_false-unreach-call.c below 3 UNSOUND0.713
fibo_2calls_10_true-unreach-call.c below 3 PASS0.733
fibo_2calls_15_false-unreach-call.c below 3 UNSOUND0.724
fibo_2calls_15_true-unreach-call.c below 3 PASS0.765
fibo_2calls_20_false-unreach-call.c below 3 UNSOUND0.724
fibo_2calls_20_true-unreach-call.c below 3 PASS0.699
fibo_2calls_25_false-unreach-call.c below 3 UNSOUND0.712
fibo_2calls_25_true-unreach-call.c below 3 PASS0.725
fibo_2calls_2_false-unreach-call.c below 3 OKAY0.799
fibo_2calls_2_true-unreach-call.c below 3 PASS0.7
fibo_2calls_4_false-unreach-call.c below 3 UNSOUND0.733
fibo_2calls_4_true-unreach-call.c below 3 PASS0.742
fibo_2calls_5_false-unreach-call.c below 3 UNSOUND0.699
fibo_2calls_5_true-unreach-call.c below 3 PASS0.717
fibo_2calls_6_false-unreach-call.c below 3 UNSOUND0.736
fibo_2calls_6_true-unreach-call.c below 3 PASS0.721
fibo_2calls_8_false-unreach-call.c below 3 UNSOUND0.723
fibo_2calls_8_true-unreach-call.c below 3 PASS0.727
fibo_5_false-unreach-call.c below 9 OKAY0.689
fibo_5_true-unreach-call.c below 9 FAIL0.73
fibo_7_false-unreach-call.c below 9 OKAY0.739
fibo_7_true-unreach-call.c below 9 FAIL0.717
id2_b2_o3_true-unreach-call.c below 2 PASS0.608
id2_b3_o2_false-unreach-call.c below 2 OKAY0.612
id2_b3_o5_true-unreach-call.c below 2 PASS0.598
id2_b5_o10_true-unreach-call.c below 2 PASS0.632
id2_i5_o5_false-unreach-call.c below 2 OKAY0.401
id2_i5_o5_true-unreach-call.c below 2 PASS0.391
id_b2_o3_true-unreach-call.c below 2 PASS0.543
id_b3_o2_false-unreach-call.c below 2 OKAY0.549
id_b3_o5_true-unreach-call.c below 2 PASS0.518
id_b5_o10_true-unreach-call.c below 2 PASS0.509
id_i10_o10_false-unreach-call.c below 2 OKAY0.369
id_i10_o10_true-unreach-call.c below 2 PASS0.38
id_i15_o15_false-unreach-call.c below 2 OKAY0.362
id_i15_o15_true-unreach-call.c below 2 PASS0.384
id_i20_o20_false-unreach-call.c below 2 OKAY0.375
id_i20_o20_true-unreach-call.c below 2 PASS0.383
id_i25_o25_false-unreach-call.c below 2 OKAY0.371
id_i25_o25_true-unreach-call.c below 2 PASS0.368
id_i5_o5_false-unreach-call.c below 2 OKAY0.372
id_i5_o5_true-unreach-call.c below 2 PASS0.385
id_o1000_false-unreach-call.c below 2 OKAY0.365
id_o100_false-unreach-call.c below 2 OKAY0.376
id_o10_false-unreach-call.c below 2 OKAY0.36
id_o200_false-unreach-call.c below 2 OKAY0.374
id_o20_false-unreach-call.c below 2 OKAY0.37
id_o3_false-unreach-call.c below 2 OKAY0.388
sum_10x0_false-unreach-call.c below 2 OKAY0.424
sum_10x0_true-unreach-call.c below 2 PASS0.413
sum_15x0_false-unreach-call.c below 2 OKAY0.413
sum_15x0_true-unreach-call.c below 2 PASS0.399
sum_20x0_false-unreach-call.c below 2 OKAY0.407
sum_20x0_true-unreach-call.c below 2 PASS0.405
sum_25x0_false-unreach-call.c below 2 OKAY0.421
sum_25x0_true-unreach-call.c below 2 PASS0.411
sum_2x3_false-unreach-call.c below 2 OKAY0.402
sum_2x3_true-unreach-call.c below 2 PASS0.402
sum_non_eq_false-unreach-call.c below 2 OKAY0.406
sum_non_eq_true-unreach-call.c below 2 PASS0.394
sum_non_false-unreach-call.c below 2 OKAY0.406
sum_non_true-unreach-call.c below 2 PASS0.41
ICRA Assertions (True) = 30/36
ICRA Assertions (False) = 30/38
ICRA Time = 40.332
/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.406
rec-bhmr2007_true-unreach-call.c below 2 PASS0.417
rec-cggmp2005b_true-unreach-call.c below 2 PASS0.537
rec-cggmp2005_true-unreach-call.c below 2 PASS0.37
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.399
rec-css2003_true-unreach-call.c below 2 PASS0.948
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.089
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.74
rec-gj2007b_true-unreach-call.c below 2 FAIL0.37
rec-gj2007_true-unreach-call.c below 2 PASS0.461
rec-gr2006_true-unreach-call.c below 2 PASS0.488
rec-gsv2008_true-unreach-call.c below 2 PASS0.436
rec-hhk2008_true-unreach-call.c below 2 PASS0.377
rec-jm2006_true-unreach-call.c below 2 PASS0.45
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.487
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.416
ICRA Assertions (True) = 12/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.391
/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.367
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.394
rec-count_by_2_true-unreach-call.c below 2 PASS0.354
rec-count_by_k_true-unreach-call.c below 2 PASS0.381
rec-count_by_nondet_true-unreach-call.c below 2 PASS0.405
rec-gauss_sum_true-unreach-call.c below 2 PASS0.411
rec-half_true-unreach-call.c below 2 PASS0.387
rec-nested_true-unreach-call.c below 3 FAIL0.509
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.208
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.509
edit_distance_bottom_up.c below 3 PASS117.659
edit_distance_top_down.c below 3 PASS2.189
log_log_n_solution.c below 2 FAIL0.398
log_n_solution.c below 2 PASS0.444
multivariate_1.c below TIMEOUT 300.135
multivariate_higher_order.c below 2 PASS0.749
n_cubed_solution.c below 3 PASS0.883
n_log_n_solution.c below 2 PASS0.5
n_squared_two_base_case_even.c below 2 PASS0.468
n_squared_two_base_case_odd.c below 2 PASS0.483
pascals_dynamic.c below 3 FAIL3.403
pascals_iterative.c below 1 FAIL3.611
pascals_recursive.c below 9 PASS1.131
squared_solution.c below 2 PASS0.507
two_n_even.c below 2 PASS0.407
two_n_odd.c below 2 PASS0.408
two_to_n_over_two_even.c below 2 PASS0.437
two_to_n_over_two_odd.c below 2 PASS0.436
two_to_n_squared.c below 3 FAIL4.009
two_to_two_to_n.c below 2 PASS0.469
ICRA Assertions (True) = 16/21
ICRA Assertions (False) = 0/0
ICRA Time = 439.235
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.361
binary_search_array_tree.c below 1 FAIL0.576
exp_add_loop_rec.c below 1 FAIL0.358
exp_add_loop_variable.c below 1 PASS0.389
exp_with_linear_inner_loop.c below 1 FAIL0.475
halving_log1.c below 1 PASS0.48
linear_two_to_n.c below 2 FAIL0.451
loop_five_to_n.c below 1 PASS0.372
non_loop_five_to_n.c below 2 FAIL0.724
power_log.c below 1 PASS0.477
power_log_modified.c below 1 PASS0.466
simple_exponential.c below 1 PASS0.368
simple_exponential_for.c below 1 PASS0.388
two_to_n_minus_n.c below 2 PASS0.485
two_to_n_minus_n_loop.c below 3 PASS0.714
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 0/0
ICRA Time = 7.084