[Version Information]
WALi-OpenNWA version: 97ff72fc319b11f39abbceff5a35ed182ebe8e82 (2017-06-26 12:47:30 -0400) "CoFloCo benchmarks"
duet version: 8c2d24447ec25f66452279a6d8885e76607364d0 (2017-07-01 13:36:16 -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.56
kmp.c below 1 PASS1.751
qsort.c below 2 PASS0.612
speed_pldi09_fig1.c below 1 PASS0.511
speed_pldi09_fig4_2.c below 1 FAIL0.402
speed_pldi09_fig4_4.c below 1 PASS22.475
speed_pldi09_fig4_5.c below 1 PASS0.437
speed_pldi10_ex1.c below 1 PASS1.264
speed_pldi10_ex3.c below 1 PASS0.528
speed_pldi10_ex4.c below 1 PASS0.559
speed_popl10_fig2_1.c below 1 PASS0.471
speed_popl10_fig2_2.c below 1 FAIL0.389
speed_popl10_nested_multiple.c below 1 PASS0.495
speed_popl10_nested_single.c below 1 PASS0.47
speed_popl10_sequential_single.c below 1 PASS0.403
speed_popl10_simple_multiple.c below 1 PASS0.53
speed_popl10_simple_single_2.c below 1 PASS0.644
speed_popl10_simple_single.c below 1 PASS0.385
t07.c below 1 PASS0.448
t08.c below 1 PASS0.406
t09.c below 1 PASS0.409
t10.c below 1 PASS0.372
t11.c below 1 PASS0.477
t13.c below 1 FAIL0.437
t15.c below 1 PASS0.434
t16.c below 1 PASS0.424
t19.c below 1 PASS0.426
t20.c below 1 PASS0.408
t27.c below 1 PASS0.566
t28.c below 1 PASS0.489
t30.c below 1 FAIL0.436
t37.c below 2 PASS0.627
t39.c below 2 PASS0.552
t46.c below 1 PASS0.42
t47.c below 1 FAIL0.568
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 40.785
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.387
qsort_full.c below 4 PASS6.06
rec1-param_safe.c below 2 PASS0.399
rec1-param_unsafe.c below 2 OKAY0.398
rec1_safe.c below 2 PASS0.378
rec1_unsafe.c below 2 OKAY0.377
rec2-param_safe.c below 2 PASS0.379
rec2-param_unsafe.c below 2 OKAY0.385
rec2_safe.c below 2 PASS0.397
rec2_unsafe.c below 2 OKAY0.378
rec-test.c below 2 PASS0.388
sas03_bothbranches.c below 2 PASS0.441
sas03.c below 2 PASS0.807
simulated_lese_recursive.c below 2 PASS0.465
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.639
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.355
count_up_down_unsafe.c below 1 OKAY0.34
divide.c below 1 PASS0.374
factor_unsafe.c below 1 OKAY0.345
for_infinite_loop_1_safe.c below 1 PASS0.34
for_infinite_loop_2_safe.c below 1 PASS0.376
interproc.c below 1 PASS0.347
mult.c below 1 PASS0.344
pointer_arith.c below 1 PASS0.333
quotient.c below 3 PASS0.509
subtract.c below 1 PASS0.331
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.346
sum01_bug02_unsafe.c below 1 OKAY0.615
sum01_real_safe.c below 1 PASS0.355
sum01_safe.c below 1 PASS0.368
sum01_unsafe.c below 1 OKAY0.504
sum02_safe.c below 1 PASS0.37
sum03_safe.c below 1 PASS0.405
sum03_unsafe.c below 1 OKAY0.512
sum04_safe.c below 1 PASS0.361
sum04_unsafe.c below 1 OKAY0.48
terminator_02_safe.c below 1 PASS0.339
terminator_02_unsafe.c below 1 OKAY0.377
terminator_03_safe.c below 1 PASS0.337
terminator_03_unsafe.c below 1 OKAY0.348
token_ring01_safe.c below 4 FAIL76.206
token_ring01_unsafe.c below 4 OKAY163.115
toy_safe.c below EXCEPTION 207.901
trex01_safe.c below 1 PASS0.774
trex01_unsafe.c below 1 OKAY0.386
trex02_safe2.c below 2 PASS0.391
trex02_safe.c below 2 PASS0.393
trex02_unsafe.c below 2 OKAY0.385
trex03_safe.c below 1 PASS0.446
trex03_unsafe.c below 1 OKAY0.448
trex04_safe.c below 1 PASS0.365
while_infinite_loop_1_safe.c below 1 PASS0.325
while_infinite_loop_2_safe.c below 1 PASS0.335
while_infinite_loop_3_safe.c below 1 PASS0.324
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 461.505
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.402
blogger_simplified1.c below 3 PASS1.274
divided_difference2.c below TIMEOUT 300.013
mult-proc.c below 3 PASS0.408
mult-proc-params.c below 3 PASS0.396
popall.c below 1 PASS0.686
simulated_scc.c below 1 PASS0.665
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.844
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.391
degree2_binomial.c below 1 PASS0.824
degree2_monomial.c below 1 PASS0.436
degree3_binomial.c below 1 PASS1.867
degree3_monomial.c below 1 PASS0.461
degree4_binomial.c below 1 PASS4.456
degree4_monomial.c below 1 PASS0.552
degree5_binomial.c below 1 TIMEOUT300.024
degree5_monomial.c below 1 PASS0.893
ICRA Assertions (True) = 8/9
ICRA Assertions (False) = 0/0
ICRA Time = 309.904
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.452
cubic_with_square_interproc.c below 2 PASS0.561
cubic_with_square_nonlinear.c below 1 PASS0.38
cubic_with_square_nonlinear_interproc.c below 2 PASS0.43
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.399
cubic_with_square_unsafe.c below 1 OKAY0.452
multi-input.c below 1 PASS221.946
multi-input_unsafe.c below 1 OKAY0.632
nondet_loop_bound.c below 1 PASS0.372
nondet_loop_bound_quartic.c below 1 PASS0.375
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.369
nondet_loop_bound_unsafe.c below 1 OKAY0.37
nonlinear_stratified.c below 1 TIMEOUT300.036
nonlinear_stratified_unsafe.c below 1 OKAY246.426
quartic_with_cube.c below 1 PASS0.636
quartic_with_cube_nonlinear.c below 1 PASS0.414
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.413
quartic_with_cube_unsafe.c below 1 OKAY0.498
quintic_with_quartic.c below 1 PASS1.082
quintic_with_quartic_nonlinear.c below 1 PASS0.432
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.448
quintic_with_quartic_unsafe.c below 1 OKAY1.092
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 10/10
ICRA Time = 778.215
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.727
degree2_FD_AllAux_AllAssm.c below 1 PASS172.903
degree2_FD_AllAux_FewAssm.c below 1 PASS5.285
degree2_FD_FewAux_FewAssm.c below 1 PASS0.956
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.932
degree3.c below 1 PASS0.658
degree3_FD.c below 1 PASS0.798
degree4.c below 1 PASS0.434
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 182.693
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.428
loop_unsafe.c below 1 OKAY0.447
simulated_lese_parser.c below 1 PASS0.348
simulated_lese_sentinel.c below 1 PASS0.362
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.585
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.368
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.368
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.009
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.009
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.368
array_false-unreach-call2.c below 1 OKAY0.382
array_false-unreach-call3.c below 1 OKAY0.343
array_true-unreach-call1.c below 1 FAIL0.368
array_true-unreach-call2.c below 1 FAIL0.367
array_true-unreach-call3.c below 1 PASS0.355
array_true-unreach-call4.c below 1 FAIL0.339
const_false-unreach-call1.c below 1 OKAY0.363
const_true-unreach-call1.c below 1 PASS0.342
diamond_false-unreach-call1.c below 1 OKAY0.377
diamond_true-unreach-call1.c below 1 PASS0.348
diamond_true-unreach-call2.c below 1 PASS0.396
functions_false-unreach-call1.c below 3 OKAY0.412
functions_true-unreach-call1.c below 3 PASS0.389
multivar_false-unreach-call1.c below 1 OKAY0.366
multivar_true-unreach-call1.c below 1 PASS0.365
nested_false-unreach-call1.c below 1 OKAY0.393
nested_true-unreach-call1.c below 1 PASS0.395
overflow_true-unreach-call1.c below 1 PASS0.326
phases_false-unreach-call1.c below 1 OKAY0.439
phases_false-unreach-call2.c below 1 OKAY0.355
phases_true-unreach-call1.c below 1 PASS0.421
phases_true-unreach-call2.c below 1 PASS0.357
simple_false-unreach-call1.c below 1 OKAY0.348
simple_false-unreach-call2.c below 1 OKAY0.335
simple_false-unreach-call3.c below 1 OKAY0.355
simple_false-unreach-call4.c below 1 OKAY0.347
simple_true-unreach-call1.c below 1 PASS0.345
simple_true-unreach-call2.c below 1 PASS0.342
simple_true-unreach-call3.c below 1 PASS0.347
simple_true-unreach-call4.c below 1 PASS0.333
underapprox_false-unreach-call1.c below 1 OKAY0.354
underapprox_false-unreach-call2.c below 1 OKAY0.38
underapprox_true-unreach-call1.c below 1 FAIL0.366
underapprox_true-unreach-call2.c below 1 PASS0.358
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.776
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.891
apache-get-tag_true-unreach-call.c below 1 FAIL0.466
down_true-unreach-call.c below 1 PASS0.395
fragtest_simple_true-unreach-call.c below 1 PASS0.449
half_2_true-unreach-call.c below 1 PASS0.405
heapsort_true-unreach-call.c below 1 PASS1.328
id_build_true-unreach-call.c below 1 PASS0.349
id_trans_false-unreach-call.c below 1 OKAY0.343
large_const_true-unreach-call.c below 1 PASS0.431
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.388
nested6_true-unreach-call.c below 1 FAIL0.482
nested9_true-unreach-call.c below 1 PASS0.555
nest-if3_true-unreach-call.c below 1 PASS0.499
NetBSD_loop_true-unreach-call.c below 1 PASS0.359
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.416
seq_true-unreach-call.c below 1 PASS0.458
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.616
string_concat-noarr_true-unreach-call.c below 1 PASS0.401
up_true-unreach-call.c below 1 PASS0.399
ICRA Assertions (True) = 15/18
ICRA Assertions (False) = 1/1
ICRA Time = 10.63
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.411
bhmr2007_true-unreach-call.c below 1 PASS0.424
cggmp2005b_true-unreach-call.c below 1 PASS0.509
cggmp2005_true-unreach-call.c below 1 PASS0.366
cggmp2005_variant_true-unreach-call.c below 1 PASS0.395
css2003_true-unreach-call.c below 1 PASS0.799
ddlm2013_true-unreach-call.c below 1 PASS0.545
gcnr2008_false-unreach-call.c below 1 OKAY0.954
gj2007b_true-unreach-call.c below 1 FAIL0.398
gj2007_true-unreach-call.c below 1 PASS0.469
gr2006_true-unreach-call.c below 1 PASS0.469
gsv2008_true-unreach-call.c below 1 PASS0.369
hhk2008_true-unreach-call.c below 1 PASS0.367
jm2006_true-unreach-call.c below 1 PASS0.436
jm2006_variant_true-unreach-call.c below 1 PASS0.508
mcmillan2006_true-unreach-call.c below 1 FAIL0.386
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.805
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.343
count_by_1_variant_true-unreach-call.c below 1 PASS0.41
count_by_2_true-unreach-call.c below 1 PASS0.356
count_by_k_true-unreach-call.c below 1 PASS0.365
count_by_nondet_true-unreach-call.c below 1 FAIL0.382
gauss_sum_true-unreach-call.c below 1 PASS0.389
half_true-unreach-call.c below 1 FAIL0.377
nested_true-unreach-call.c below 1 PASS0.454
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.076
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.396
array_true-unreach-call.c below 1 FAIL0.398
bubble_sort_false-unreach-call.c below 4 OKAY53.827
bubble_sort_true-unreach-call.c below 1 PASS3.701
compact_false-unreach-call.c below 1 OKAY0.39
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.367
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.383
eureka_01_false-unreach-call.c below 1 OKAY2.385
eureka_01_true-unreach-call.c below 1 FAIL1.783
eureka_05_true-unreach-call.c below TIMEOUT 300.005
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.372
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.35
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.357
heavy_false-unreach-call.c below 1 OKAY0.492
heavy_true-unreach-call.c below 1 PASS0.49
insertion_sort_false-unreach-call.c below 1 OKAY1.688
insertion_sort_true-unreach-call.c below 1 FAIL0.597
invert_string_false-unreach-call.c below 1 OKAY0.533
invert_string_true-unreach-call.c below 1 FAIL0.556
linear_sea.ch_true-unreach-call.c below 1 FAIL0.414
linear_search_false-unreach-call.c below 1 OKAY0.428
lu.cmp_true-unreach-call.c below 3 PASS28.02
ludcmp_false-unreach-call.c below 3 OKAY28.479
matrix_false-unreach-call_true-termination.c below 1 OKAY1.108
matrix_true-unreach-call_true-termination.c below 1 FAIL0.427
n.c11_true-unreach-call.c below 3 FAIL0.418
n.c24_false-unreach-call.c below 3 OKAY2.808
n.c40_true-unreach-call.c below 1 FAIL0.362
nec11_false-unreach-call.c below 1 OKAY0.349
nec20_false-unreach-call.c below 1 OKAY0.402
nec40_true-unreach-call.c below 1 FAIL0.381
string_false-unreach-call.c below 1 OKAY0.624
string_true-unreach-call.c below 1 FAIL0.614
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.608
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.357
sum01_false-unreach-call_true-termination.c below 1 OKAY0.468
sum01_true-unreach-call_true-termination.c below 1 PASS0.374
sum03_false-unreach-call_true-termination.c below 1 OKAY0.518
sum03_true-unreach-call_false-termination.c below 1 PASS0.455
sum04_false-unreach-call_true-termination.c below 1 OKAY0.483
sum04_true-unreach-call_true-termination.c below 1 PASS0.382
sum_array_false-unreach-call.c below 1 OKAY0.569
sum_array_true-unreach-call.c below 1 FAIL0.662
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.351
terminator_02_false-unreach-call_true-termination.c below 2 OKAY0.423
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.376
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.364
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.363
trex01_false-unreach-call_true-termination.c below 3 OKAY0.476
trex01_true-unreach-call.c below 3 PASS0.712
trex02_false-unreach-call_true-termination.c below 2 OKAY0.393
trex02_true-unreach-call_true-termination.c below 2 PASS0.381
trex03_false-unreach-call_true-termination.c below 2 OKAY0.58
trex03_true-unreach-call.c below 2 PASS0.606
trex04_true-unreach-call_false-termination.c below 1 PASS0.417
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.362
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.739
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.385
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.378
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY4.098
vogal_false-unreach-call.c below 1 OKAY0.862
vogal_true-unreach-call.c below 1 FAIL0.715
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.336
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.327
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.326
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.329
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 458.079
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.995
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.972
Ackermann03_true-unreach-call.c below 7 FAIL1.006
Ackermann04_true-unreach-call.c below 7 FAIL1.199
Addition01_true-unreach-call_true-termination.c below 2 PASS2.334
Addition02_false-unreach-call_false-termination.c below 2 OKAY3.503
Addition03_false-no-overflow.c below 2 PASS0.572
Addition03_true-unreach-call.c below 2 PASS0.563
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.484
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.438
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.457
Fibonacci01_true-unreach-call.c below 7 FAIL0.798
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.787
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.824
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.829
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.802
gcd01_true-unreach-call_true-termination.c below 2 PASS0.567
gcd02_true-unreach-call.c below 2 FAIL0.989
McCarthy91_false-unreach-call_false-termination.c below 4 OKAY0.575
McCarthy91_true-unreach-call.c below 4 PASS0.534
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.569
Primes_true-unreach-call.c below 2 FAIL1.278
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.646
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.409
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.403
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 7/7
ICRA Time = 23.533
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.442
afterrec_2calls_true-unreach-call.c below 2 PASS0.434
afterrec_false-unreach-call.c below 2 OKAY0.398
afterrec_true-unreach-call.c below 2 PASS0.396
fibo_10_false-unreach-call.c below 7 OKAY0.819
fibo_10_true-unreach-call.c below 7 FAIL0.819
fibo_15_false-unreach-call.c below 7 OKAY0.835
fibo_15_true-unreach-call.c below 7 FAIL0.793
fibo_20_false-unreach-call.c below 7 OKAY0.795
fibo_20_true-unreach-call.c below 7 FAIL0.795
fibo_25_false-unreach-call.c below 7 OKAY0.785
fibo_25_true-unreach-call.c below 7 FAIL0.8
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.004
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.004
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.004
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.004
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.007
fibo_5_false-unreach-call.c below 7 OKAY0.78
fibo_5_true-unreach-call.c below 7 FAIL0.812
fibo_7_false-unreach-call.c below 7 OKAY0.775
fibo_7_true-unreach-call.c below 7 FAIL0.782
id2_b2_o3_true-unreach-call.c below 2 PASS0.624
id2_b3_o2_false-unreach-call.c below 2 OKAY0.668
id2_b3_o5_true-unreach-call.c below 2 PASS0.642
id2_b5_o10_true-unreach-call.c below 2 PASS0.64
id2_i5_o5_false-unreach-call.c below 2 OKAY0.416
id2_i5_o5_true-unreach-call.c below 2 PASS0.42
id_b2_o3_true-unreach-call.c below 2 PASS0.562
id_b3_o2_false-unreach-call.c below 2 OKAY0.566
id_b3_o5_true-unreach-call.c below 2 PASS0.538
id_b5_o10_true-unreach-call.c below 2 PASS0.556
id_i10_o10_false-unreach-call.c below 2 OKAY0.383
id_i10_o10_true-unreach-call.c below 2 PASS0.391
id_i15_o15_false-unreach-call.c below 2 OKAY0.392
id_i15_o15_true-unreach-call.c below 2 PASS0.389
id_i20_o20_false-unreach-call.c below 2 OKAY0.41
id_i20_o20_true-unreach-call.c below 2 PASS0.389
id_i25_o25_false-unreach-call.c below 2 OKAY0.399
id_i25_o25_true-unreach-call.c below 2 PASS0.375
id_i5_o5_false-unreach-call.c below 2 OKAY0.397
id_i5_o5_true-unreach-call.c below 2 PASS0.397
id_o1000_false-unreach-call.c below 2 OKAY0.382
id_o100_false-unreach-call.c below 2 OKAY0.406
id_o10_false-unreach-call.c below 2 OKAY0.382
id_o200_false-unreach-call.c below 2 OKAY0.389
id_o20_false-unreach-call.c below 2 OKAY0.382
id_o3_false-unreach-call.c below 2 OKAY0.374
sum_10x0_false-unreach-call.c below 2 OKAY0.426
sum_10x0_true-unreach-call.c below 2 PASS0.4
sum_15x0_false-unreach-call.c below 2 OKAY0.431
sum_15x0_true-unreach-call.c below 2 PASS0.422
sum_20x0_false-unreach-call.c below 2 OKAY0.412
sum_20x0_true-unreach-call.c below 2 PASS0.422
sum_25x0_false-unreach-call.c below 2 OKAY0.423
sum_25x0_true-unreach-call.c below 2 PASS0.414
sum_2x3_false-unreach-call.c below 2 OKAY0.427
sum_2x3_true-unreach-call.c below 2 PASS0.421
sum_non_eq_false-unreach-call.c below 2 OKAY0.429
sum_non_eq_true-unreach-call.c below 2 PASS0.398
sum_non_false-unreach-call.c below 2 OKAY0.418
sum_non_true-unreach-call.c below 2 PASS0.42
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5429.086
/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.425
rec-bhmr2007_true-unreach-call.c below 2 PASS0.414
rec-cggmp2005b_true-unreach-call.c below 2 PASS0.557
rec-cggmp2005_true-unreach-call.c below 2 PASS0.391
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.416
rec-css2003_true-unreach-call.c below 2 PASS0.975
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.102
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.763
rec-gj2007b_true-unreach-call.c below 2 FAIL0.389
rec-gj2007_true-unreach-call.c below 2 FAIL0.486
rec-gr2006_true-unreach-call.c below 2 FAIL0.47
rec-gsv2008_true-unreach-call.c below 2 PASS0.436
rec-hhk2008_true-unreach-call.c below 2 PASS0.415
rec-jm2006_true-unreach-call.c below 2 PASS0.446
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.497
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.419
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.601
/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.38
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.419
rec-count_by_2_true-unreach-call.c below 2 PASS0.372
rec-count_by_k_true-unreach-call.c below 2 PASS0.417
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.406
rec-gauss_sum_true-unreach-call.c below 2 PASS0.415
rec-half_true-unreach-call.c below 2 FAIL0.401
rec-nested_true-unreach-call.c below 3 FAIL0.515
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.325
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.524
edit_distance_bottom_up.c below 3 FAIL139.228
edit_distance_top_down.c below 3 FAIL2.838
log_log_n_solution.c below 2 FAIL0.444
log_n_solution.c below 2 FAIL0.475
multivariate_1.c below TIMEOUT 300.167
multivariate_higher_order.c below 2 PASS0.818
n_cubed_solution.c below EXCEPTION 0.392
n_log_n_solution.c below 2 PASS0.519
n_squared_two_base_case_even.c below 2 PASS0.491
n_squared_two_base_case_odd.c below 2 PASS0.486
pascals_dynamic.c below 3 FAIL3.612
pascals_iterative.c below 1 FAIL3.68
pascals_recursive.c below 8 FAIL20.726
squared_solution.c below 2 PASS0.529
two_n_even.c below 2 PASS0.403
two_n_odd.c below 2 PASS0.402
two_to_n_over_two_even.c below 2 PASS0.436
two_to_n_over_two_odd.c below 2 PASS0.442
two_to_n_squared.c below 5 FAIL10.365
two_to_two_to_n.c below 2 PASS0.454
ICRA Assertions (True) = 11/21
ICRA Assertions (False) = 0/0
ICRA Time = 487.431
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.384
binary_search_array_tree.c below 1 FAIL0.688
exp_add_loop_rec.c below 1 FAIL0.368
exp_add_loop_variable.c below 1 PASS0.409
exp_with_linear_inner_loop.c below 1 FAIL0.493
halving_log1.c below 1 FAIL0.534
linear_two_to_n.c below 2 FAIL0.479
loop_five_to_n.c below 1 PASS0.405
non_loop_five_to_n.c below 2 FAIL0.669
power_log.c below 1 PASS0.482
power_log_modified.c below 1 PASS0.507
simple_exponential.c below 1 PASS0.413
simple_exponential_for.c below 1 PASS0.39
two_to_n_minus_n.c below 2 FAIL0.523
two_to_n_minus_n_loop.c below EXCEPTION 1.948
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 0/0
ICRA Time = 8.692