[Version Information]
WALi-OpenNWA version: 9042782a9a5ed8987eef2dfeec4e384ee950f24c (2017-05-01 17:41:53 -0500) "Adding benchmarks for model of malware analyzer."
duet version: 05dc712315a9f1a66cd0a3c927666793fd03610e (2017-04-27 22:38:51 -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-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
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               20170323  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.365
kmp.c below 1 PASS1.313
qsort.c below 4 PASS2.579
speed_pldi09_fig1.c below 1 PASS0.371
speed_pldi09_fig4_2.c below 1 FAIL0.404
speed_pldi09_fig4_4.c below 1 PASS0.447
speed_pldi09_fig4_5.c below 1 PASS0.37
speed_pldi10_ex1.c below 1 PASS3.767
speed_pldi10_ex3.c below 1 PASS0.451
speed_pldi10_ex4.c below EXCEPTION 0.415
speed_popl10_fig2_1.c below 1 PASS0.371
speed_popl10_fig2_2.c below 1 FAIL0.354
speed_popl10_nested_multiple.c below 1 PASS0.428
speed_popl10_nested_single.c below 1 PASS0.398
speed_popl10_sequential_single.c below 1 PASS0.344
speed_popl10_simple_multiple.c below 1 PASS0.384
speed_popl10_simple_single_2.c below 1 PASS0.407
speed_popl10_simple_single.c below 1 PASS0.339
t07.c below 1 PASS0.364
t08.c below 1 PASS0.342
t09.c below 1 PASS0.336
t10.c below 1 PASS0.354
t11.c below 1 PASS0.39
t13.c below 1 FAIL0.395
t15.c below 1 PASS0.369
t16.c below 1 PASS0.369
t19.c below 1 PASS0.342
t20.c below 1 PASS0.336
t27.c below 1 PASS0.425
t28.c below 1 PASS0.39
t30.c below 1 FAIL0.353
t37.c below 2 PASS0.465
t39.c below 2 PASS0.478
t46.c below 1 PASS0.347
t47.c below 1 PASS0.356
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 19.918
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.386
qsort_full.c below 4 TIMEOUT 300.005
rec1-param_safe.c below 2 PASS0.352
rec1-param_unsafe.c below 2 OKAY0.355
rec1_safe.c below 2 PASS0.338
rec1_unsafe.c below 2 OKAY0.333
rec2-param_safe.c below 2 PASS0.338
rec2-param_unsafe.c below 2 OKAY0.35
rec2_safe.c below 2 PASS0.338
rec2_unsafe.c below 2 OKAY0.339
rec-test.c below 2 PASS0.337
sas03_bothbranches.c below 7 PASS1.276
sas03.c below 2 PASS0.782
simulated_lese_recursive.c below 2 PASS0.371
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 4/4
ICRA Time = 305.9
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.317
count_up_down_unsafe.c below 1 OKAY0.34
divide.c below 1 PASS0.342
factor_unsafe.c below TIMEOUT 300.004
for_infinite_loop_1_safe.c below 1 PASS0.326
for_infinite_loop_2_safe.c below 1 PASS0.323
interproc.c below 1 PASS0.302
mult.c below 1 PASS0.317
pointer_arith.c below 1 PASS0.297
quotient.c below 3 PASS0.41
subtract.c below 1 PASS0.33
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.36
sum01_bug02_unsafe.c below 1 OKAY0.391
sum01_real_safe.c below 1 PASS0.326
sum01_safe.c below 1 PASS0.332
sum01_unsafe.c below 1 OKAY0.37
sum02_safe.c below 1 PASS0.335
sum03_safe.c below 1 PASS0.322
sum03_unsafe.c below 1 OKAY0.4
sum04_safe.c below 1 PASS0.322
sum04_unsafe.c below 1 OKAY0.356
terminator_02_safe.c below 1 PASS0.329
terminator_02_unsafe.c below 1 OKAY0.348
terminator_03_safe.c below 1 PASS0.311
terminator_03_unsafe.c below 1 OKAY0.324
token_ring01_safe.c below TIMEOUT 300.007
token_ring01_unsafe.c below TIMEOUT 300.006
toy_safe.c below EXCEPTION 178.652
trex01_safe.c below 1 PASS0.681
trex01_unsafe.c below 1 OKAY0.375
trex02_safe2.c below 3 PASS0.385
trex02_safe.c below 3 PASS0.381
trex02_unsafe.c below 3 OKAY0.383
trex03_safe.c below 1 PASS0.452
trex03_unsafe.c below 1 OKAY0.453
trex04_safe.c below 1 PASS0.355
while_infinite_loop_1_safe.c below 1 PASS0.305
while_infinite_loop_2_safe.c below 1 PASS0.313
while_infinite_loop_3_safe.c below 1 PASS0.307
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 11/13
ICRA Time = 1091.189
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.453
blogger_simplified1.c below 3 PASS1.036
divided_difference2.c below TIMEOUT 300.006
mult-proc.c below 3 PASS0.358
mult-proc-params.c below 3 PASS0.397
popall.c below 1 PASS0.407
simulated_scc.c below 1 PASS0.505
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.162
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.322
degree2_binomial.c below 1 PASS0.469
degree2_monomial.c below 1 PASS0.363
degree3_binomial.c below 1 PASS0.892
degree3_monomial.c below 1 PASS0.408
degree4_binomial.c below 1 PASS1.148
degree4_monomial.c below 1 PASS0.488
degree5_binomial.c below 1 PASS1.713
degree5_monomial.c below 1 PASS0.56
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 6.363
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.344
cubic_with_square_interproc.c below 2 PASS0.373
cubic_with_square_nonlinear.c below 1 PASS0.336
cubic_with_square_nonlinear_interproc.c below 2 PASS0.368
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.348
cubic_with_square_unsafe.c below 1 OKAY0.363
multi-input.c below 1 PASS0.395
multi-input_unsafe.c below 1 OKAY0.428
nondet_loop_bound.c below 1 PASS0.352
nondet_loop_bound_quartic.c below 1 PASS0.362
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.348
nondet_loop_bound_unsafe.c below 1 OKAY0.389
nonlinear_stratified.c below 1 FAIL0.393
nonlinear_stratified_unsafe.c below 1 OKAY0.362
quartic_with_cube.c below 1 PASS0.356
quartic_with_cube_nonlinear.c below 1 PASS0.37
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.373
quartic_with_cube_unsafe.c below 1 OKAY0.351
quintic_with_quartic.c below 1 PASS0.346
quintic_with_quartic_nonlinear.c below 1 PASS0.38
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.391
quintic_with_quartic_unsafe.c below 1 OKAY0.351
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 10/10
ICRA Time = 8.079
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.496
degree2_FD_AllAux_AllAssm.c below 1 PASS3.602
degree2_FD_AllAux_FewAssm.c below 1 PASS5.447
degree2_FD_FewAux_FewAssm.c below 1 PASS0.686
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.711
degree3.c below 1 PASS0.56
degree3_FD.c below 1 PASS0.729
degree4.c below 1 PASS0.388
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 12.619
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.389
loop_unsafe.c below 1 OKAY0.405
simulated_lese_parser.c below 1 PASS0.318
simulated_lese_sentinel.c below 1 PASS0.337
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.449
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.337
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.337
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.013
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.013
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.337
array_false-unreach-call2.c below 1 OKAY0.365
array_false-unreach-call3.c below 1 OKAY0.33
array_true-unreach-call1.c below 1 FAIL0.34
array_true-unreach-call2.c below 1 FAIL0.373
array_true-unreach-call3.c below 1 PASS0.324
array_true-unreach-call4.c below 1 FAIL0.332
const_false-unreach-call1.c below 1 OKAY0.315
const_true-unreach-call1.c below 1 PASS0.315
diamond_false-unreach-call1.c below 1 OKAY0.34
diamond_true-unreach-call1.c below 1 PASS0.334
diamond_true-unreach-call2.c below 1 PASS0.371
functions_false-unreach-call1.c below 3 OKAY0.347
functions_true-unreach-call1.c below 3 PASS0.35
multivar_false-unreach-call1.c below 1 OKAY0.333
multivar_true-unreach-call1.c below 1 PASS0.338
nested_false-unreach-call1.c below 1 OKAY0.335
nested_true-unreach-call1.c below 1 PASS0.331
overflow_true-unreach-call1.c below 1 PASS0.317
phases_false-unreach-call1.c below 1 OKAY0.338
phases_false-unreach-call2.c below 1 OKAY0.348
phases_true-unreach-call1.c below 1 PASS0.341
phases_true-unreach-call2.c below 1 PASS0.346
simple_false-unreach-call1.c below 1 OKAY0.33
simple_false-unreach-call2.c below 1 OKAY0.342
simple_false-unreach-call3.c below 1 OKAY0.309
simple_false-unreach-call4.c below 1 OKAY0.314
simple_true-unreach-call1.c below 1 PASS0.314
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.308
underapprox_false-unreach-call1.c below 1 OKAY0.315
underapprox_false-unreach-call2.c below 1 OKAY0.323
underapprox_true-unreach-call1.c below 1 FAIL0.323
underapprox_true-unreach-call2.c below 1 PASS0.324
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 11.643
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.844
apache-get-tag_true-unreach-call.c below 1 FAIL0.439
down_true-unreach-call.c below 1 PASS0.323
fragtest_simple_true-unreach-call.c below 1 PASS0.379
half_2_true-unreach-call.c below 1 PASS0.328
heapsort_true-unreach-call.c below 1 TIMEOUT300.14
id_build_true-unreach-call.c below 1 PASS0.321
id_trans_false-unreach-call.c below 1 OKAY0.332
large_const_true-unreach-call.c below 1 PASS0.387
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.365
nested6_true-unreach-call.c below 1 FAIL0.413
nested9_true-unreach-call.c below 1 PASS0.448
nest-if3_true-unreach-call.c below 1 PASS0.428
NetBSD_loop_true-unreach-call.c below 1 PASS0.34
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.384
seq_true-unreach-call.c below 1 PASS0.368
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.107
string_concat-noarr_true-unreach-call.c below 1 PASS0.338
up_true-unreach-call.c below 1 PASS0.333
ICRA Assertions (True) = 13/18
ICRA Assertions (False) = 1/1
ICRA Time = 607.017
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.331
bhmr2007_true-unreach-call.c below 1 PASS0.357
cggmp2005b_true-unreach-call.c below 1 PASS0.392
cggmp2005_true-unreach-call.c below 1 PASS0.315
cggmp2005_variant_true-unreach-call.c below 1 PASS0.327
css2003_true-unreach-call.c below 1 PASS0.461
ddlm2013_true-unreach-call.c below 1 PASS0.398
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.153
gj2007b_true-unreach-call.c below 1 FAIL0.363
gj2007_true-unreach-call.c below 1 PASS0.341
gr2006_true-unreach-call.c below 1 PASS0.325
gsv2008_true-unreach-call.c below 1 PASS0.319
hhk2008_true-unreach-call.c below 1 PASS0.322
jm2006_true-unreach-call.c below 1 PASS0.352
jm2006_variant_true-unreach-call.c below 1 PASS0.361
mcmillan2006_true-unreach-call.c below 1 FAIL0.383
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.5
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.313
count_by_1_variant_true-unreach-call.c below 1 PASS0.334
count_by_2_true-unreach-call.c below 1 PASS0.319
count_by_k_true-unreach-call.c below 1 PASS0.34
count_by_nondet_true-unreach-call.c below 1 FAIL0.342
gauss_sum_true-unreach-call.c below 1 PASS0.352
half_true-unreach-call.c below EXCEPTION 0.331
nested_true-unreach-call.c below 1 PASS0.383
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.714
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.422
array_true-unreach-call.c below 1 FAIL0.429
bubble_sort_false-unreach-call.c below EXCEPTION 106.535
bubble_sort_true-unreach-call.c below TIMEOUT 300.005
compact_false-unreach-call.c below 1 OKAY0.373
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.333
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.318
eureka_01_false-unreach-call.c below 1 OKAY2.196
eureka_01_true-unreach-call.c below 1 FAIL1.946
eureka_05_true-unreach-call.c below 1 FAIL1.059
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.321
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.319
heavy_false-unreach-call.c below 1 OKAY0.522
heavy_true-unreach-call.c below 1 PASS0.491
insertion_sort_false-unreach-call.c below 1 OKAY2.144
insertion_sort_true-unreach-call.c below 1 FAIL0.734
invert_string_false-unreach-call.c below 1 OKAY0.492
invert_string_true-unreach-call.c below 1 FAIL0.492
linear_sea.ch_true-unreach-call.c below 1 FAIL0.362
linear_search_false-unreach-call.c below 1 UNSOUND0.414
lu.cmp_true-unreach-call.c below TIMEOUT 300.239
ludcmp_false-unreach-call.c below TIMEOUT 300.245
matrix_false-unreach-call_true-termination.c below 1 OKAY1.004
matrix_true-unreach-call_true-termination.c below 1 FAIL0.532
n.c11_true-unreach-call.c below 3 FAIL0.472
n.c24_false-unreach-call.c below 3 OKAY22.798
n.c40_true-unreach-call.c below 1 FAIL0.363
nec11_false-unreach-call.c below 1 OKAY0.377
nec20_false-unreach-call.c below 1 OKAY0.363
nec40_true-unreach-call.c below 1 FAIL0.372
string_false-unreach-call.c below 1 OKAY0.652
string_true-unreach-call.c below 1 FAIL0.648
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.391
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.375
sum01_true-unreach-call_true-termination.c below 1 PASS0.339
sum03_false-unreach-call_true-termination.c below 1 OKAY0.465
sum03_true-unreach-call_false-termination.c below 1 PASS0.359
sum04_false-unreach-call_true-termination.c below 1 OKAY0.377
sum04_true-unreach-call_true-termination.c below 1 PASS0.328
sum_array_false-unreach-call.c below 1 OKAY0.621
sum_array_true-unreach-call.c below 1 FAIL0.695
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.32
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.423
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.346
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.327
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.326
trex01_false-unreach-call_true-termination.c below 3 OKAY0.471
trex01_true-unreach-call.c below 3 PASS0.773
trex02_false-unreach-call_true-termination.c below 3 OKAY0.38
trex02_true-unreach-call_true-termination.c below 3 PASS0.398
trex03_false-unreach-call_true-termination.c below 3 OKAY0.892
trex03_true-unreach-call.c below 3 PASS0.868
trex04_true-unreach-call_false-termination.c below 1 PASS0.373
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.327
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS24.048
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.355
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.346
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY17.203
vogal_false-unreach-call.c below 1 OKAY0.9
vogal_true-unreach-call.c below 1 FAIL0.896
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.295
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.323
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.322
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.313
ICRA Assertions (True) = 19/34
ICRA Assertions (False) = 29/32
ICRA Time = 1103.845
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below TIMEOUT 300.021
Ackermann02_false-unreach-call_false-termination.c below TIMEOUT 300.02
Ackermann03_true-unreach-call.c below TIMEOUT 300.02
Ackermann04_true-unreach-call.c below TIMEOUT 300.02
Addition01_true-unreach-call_true-termination.c below 2 PASS0.586
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.58
Addition03_false-no-overflow.c below 2 PASS0.591
Addition03_true-unreach-call.c below 2 PASS0.58
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.448
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.408
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.432
Fibonacci01_true-unreach-call.c below EXCEPTION 0.95
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.933
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 0.963
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 0.983
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 0.958
gcd01_true-unreach-call_true-termination.c below 2 PASS0.544
gcd02_true-unreach-call.c below 2 FAIL1.369
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.442
McCarthy91_true-unreach-call.c below 7 FAIL1.476
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.699
Primes_true-unreach-call.c below 3 FAIL2.158
recHanoi01_true-unreach-call_true-termination.c below 9 FAIL5.908
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.366
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.394
ICRA Assertions (True) = 5/18
ICRA Assertions (False) = 4/7
ICRA Time = 1222.849
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.432
afterrec_2calls_true-unreach-call.c below 2 PASS0.393
afterrec_false-unreach-call.c below 2 OKAY0.376
afterrec_true-unreach-call.c below 2 PASS0.34
fibo_10_false-unreach-call.c below EXCEPTION 0.989
fibo_10_true-unreach-call.c below EXCEPTION 0.962
fibo_15_false-unreach-call.c below EXCEPTION 0.961
fibo_15_true-unreach-call.c below EXCEPTION 0.946
fibo_20_false-unreach-call.c below EXCEPTION 0.949
fibo_20_true-unreach-call.c below EXCEPTION 0.936
fibo_25_false-unreach-call.c below EXCEPTION 0.924
fibo_25_true-unreach-call.c below EXCEPTION 0.942
fibo_2calls_10_false-unreach-call.c below EXCEPTION 17.212
fibo_2calls_10_true-unreach-call.c below EXCEPTION 17.482
fibo_2calls_15_false-unreach-call.c below EXCEPTION 17.11
fibo_2calls_15_true-unreach-call.c below EXCEPTION 17.396
fibo_2calls_20_false-unreach-call.c below EXCEPTION 17.203
fibo_2calls_20_true-unreach-call.c below EXCEPTION 17.577
fibo_2calls_25_false-unreach-call.c below EXCEPTION 17.236
fibo_2calls_25_true-unreach-call.c below EXCEPTION 17.583
fibo_2calls_2_false-unreach-call.c below EXCEPTION 17.406
fibo_2calls_2_true-unreach-call.c below EXCEPTION 17.356
fibo_2calls_4_false-unreach-call.c below EXCEPTION 17.478
fibo_2calls_4_true-unreach-call.c below EXCEPTION 17.524
fibo_2calls_5_false-unreach-call.c below EXCEPTION 17.559
fibo_2calls_5_true-unreach-call.c below EXCEPTION 17.505
fibo_2calls_6_false-unreach-call.c below EXCEPTION 17.472
fibo_2calls_6_true-unreach-call.c below EXCEPTION 17.209
fibo_2calls_8_false-unreach-call.c below EXCEPTION 17.282
fibo_2calls_8_true-unreach-call.c below EXCEPTION 17.268
fibo_5_false-unreach-call.c below EXCEPTION 0.954
fibo_5_true-unreach-call.c below EXCEPTION 0.938
fibo_7_false-unreach-call.c below EXCEPTION 0.979
fibo_7_true-unreach-call.c below EXCEPTION 0.94
id2_b2_o3_true-unreach-call.c below 2 PASS0.981
id2_b3_o2_false-unreach-call.c below 2 OKAY0.989
id2_b3_o5_true-unreach-call.c below 2 PASS0.956
id2_b5_o10_true-unreach-call.c below 2 PASS0.97
id2_i5_o5_false-unreach-call.c below 2 OKAY0.432
id2_i5_o5_true-unreach-call.c below 2 PASS0.423
id_b2_o3_true-unreach-call.c below 2 PASS0.583
id_b3_o2_false-unreach-call.c below 2 OKAY0.603
id_b3_o5_true-unreach-call.c below 2 PASS0.565
id_b5_o10_true-unreach-call.c below 2 PASS0.557
id_i10_o10_false-unreach-call.c below 2 OKAY0.367
id_i10_o10_true-unreach-call.c below 2 PASS0.371
id_i15_o15_false-unreach-call.c below 2 OKAY0.364
id_i15_o15_true-unreach-call.c below 2 PASS0.373
id_i20_o20_false-unreach-call.c below 2 OKAY0.373
id_i20_o20_true-unreach-call.c below 2 PASS0.358
id_i25_o25_false-unreach-call.c below 2 OKAY0.379
id_i25_o25_true-unreach-call.c below 2 PASS0.363
id_i5_o5_false-unreach-call.c below 2 OKAY0.371
id_i5_o5_true-unreach-call.c below 2 PASS0.376
id_o1000_false-unreach-call.c below 2 OKAY0.381
id_o100_false-unreach-call.c below 2 OKAY0.37
id_o10_false-unreach-call.c below 2 OKAY0.372
id_o200_false-unreach-call.c below 2 OKAY0.379
id_o20_false-unreach-call.c below 2 OKAY0.365
id_o3_false-unreach-call.c below 2 OKAY0.383
sum_10x0_false-unreach-call.c below 2 OKAY0.393
sum_10x0_true-unreach-call.c below 2 PASS0.385
sum_15x0_false-unreach-call.c below 2 OKAY0.38
sum_15x0_true-unreach-call.c below 2 PASS0.367
sum_20x0_false-unreach-call.c below 2 OKAY0.396
sum_20x0_true-unreach-call.c below 2 PASS0.374
sum_25x0_false-unreach-call.c below 2 OKAY0.401
sum_25x0_true-unreach-call.c below 2 PASS0.385
sum_2x3_false-unreach-call.c below 2 OKAY0.404
sum_2x3_true-unreach-call.c below 2 PASS0.388
sum_non_eq_false-unreach-call.c below 2 OKAY0.433
sum_non_eq_true-unreach-call.c below 2 PASS0.422
sum_non_false-unreach-call.c below 2 OKAY0.396
sum_non_true-unreach-call.c below 2 PASS0.385
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 344.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.379
rec-bhmr2007_true-unreach-call.c below 2 PASS0.403
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.759
rec-cggmp2005_true-unreach-call.c below 2 PASS0.348
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.346
rec-css2003_true-unreach-call.c below 2 PASS0.626
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.351
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.856
rec-gj2007b_true-unreach-call.c below 2 FAIL0.396
rec-gj2007_true-unreach-call.c below 2 FAIL0.383
rec-gr2006_true-unreach-call.c below 2 FAIL0.393
rec-gsv2008_true-unreach-call.c below 2 PASS0.351
rec-hhk2008_true-unreach-call.c below 2 PASS0.351
rec-jm2006_true-unreach-call.c below 2 PASS0.37
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.386
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.42
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.118
/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.335
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.352
rec-count_by_2_true-unreach-call.c below 2 PASS0.338
rec-count_by_k_true-unreach-call.c below 2 PASS0.354
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.372
rec-gauss_sum_true-unreach-call.c below 2 PASS0.37
rec-half_true-unreach-call.c below EXCEPTION 0.341
rec-nested_true-unreach-call.c below 3 PASS0.631
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.093
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.51
edit_distance_bottom_up.c below 3 TIMEOUT 300.009
edit_distance_top_down.c below 3 FAIL50.732
log_log_n_solution.c below 3 FAIL0.429
log_n_solution.c below 2 FAIL0.442
multivariate_1.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL26.221
n_cubed_solution.c below EXCEPTION 0.338
n_log_n_solution.c below TIMEOUT 300.034
n_squared_two_base_case_even.c below 2 PASS0.382
n_squared_two_base_case_odd.c below 2 PASS0.396
pascals_dynamic.c below 3 FAIL19.803
pascals_iterative.c below 1 FAIL5.38
pascals_recursive.c below TIMEOUT 300.005
squared_solution.c below TIMEOUT 300.137
two_n_even.c below 2 PASS0.369
two_n_odd.c below 2 PASS0.376
two_to_n_over_two_even.c below TIMEOUT 300.034
two_to_n_over_two_odd.c below TIMEOUT 300.029
two_to_n_squared.c below 5 FAIL208.029
two_to_two_to_n.c below 7 FAIL1.684
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 0/0
ICRA Time = 2415.345
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.323
exp_add_loop_rec.c below 1 FAIL0.363
exp_add_loop_variable.c below 1 PASS0.356
exp_with_linear_inner_loop.c below 1 FAIL0.414
linear_two_to_n.c below 8 FAIL1.574
loop_five_to_n.c below 1 FAIL0.355
non_loop_five_to_n.c below 8 FAIL9.8
power_log.c below 1 PASS0.414
power_log_modified.c below 1 PASS0.478
simple_exponential.c below 1 PASS0.348
simple_exponential_for.c below 1 PASS0.355
two_to_n_minus_n.c below 8 FAIL1.816
two_to_n_minus_n_loop.c below 8 FAIL2.693
ICRA Assertions (True) = 6/13
ICRA Assertions (False) = 0/0
ICRA Time = 19.289