[Version Information]
WALi-OpenNWA version: cb66c5d81a7461250a11c7d2e8f839a3ac4b693b (2017-06-01 11:48:21 -0500) "Allow full_icra_rebuild.sh to work with both NewtonICRA duet and Newton-ark2 duet."
duet version: 305dceab9ebfebd6989a176ac545ef407610a0c8 (2017-06-15 22:27:52 -0400) "Fixed newton build target"
# 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               20170614  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.366
kmp.c below 1 PASS1.02
qsort.c below 5 PASS1.892
speed_pldi09_fig1.c below 1 PASS0.351
speed_pldi09_fig4_2.c below 1 FAIL0.37
speed_pldi09_fig4_4.c below 1 PASS0.428
speed_pldi09_fig4_5.c below 1 PASS0.361
speed_pldi10_ex1.c below 1 PASS3.534
speed_pldi10_ex3.c below 1 PASS0.43
speed_pldi10_ex4.c below 1 PASS0.418
speed_popl10_fig2_1.c below 1 PASS0.387
speed_popl10_fig2_2.c below 1 FAIL0.373
speed_popl10_nested_multiple.c below 1 PASS0.402
speed_popl10_nested_single.c below 1 PASS0.384
speed_popl10_sequential_single.c below 1 PASS0.354
speed_popl10_simple_multiple.c below 1 PASS0.388
speed_popl10_simple_single_2.c below 1 PASS0.416
speed_popl10_simple_single.c below 1 PASS0.347
t07.c below 1 PASS0.357
t08.c below 1 PASS0.349
t09.c below 1 PASS0.352
t10.c below 1 PASS0.345
t11.c below 1 PASS0.379
t13.c below 1 FAIL0.387
t15.c below 1 PASS0.366
t16.c below 1 PASS0.353
t19.c below 1 PASS0.343
t20.c below 1 PASS0.343
t27.c below 1 PASS0.402
t28.c below 1 PASS0.374
t30.c below 1 FAIL0.356
t37.c below 2 PASS0.441
t39.c below 2 PASS0.455
t46.c below 1 PASS0.351
t47.c below 1 PASS0.347
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 18.521
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.354
qsort_full.c below 7 TIMEOUT 300.006
rec1-param_safe.c below 2 PASS0.346
rec1-param_unsafe.c below 2 OKAY0.364
rec1_safe.c below 2 PASS0.328
rec1_unsafe.c below 2 OKAY0.331
rec2-param_safe.c below 2 PASS0.343
rec2-param_unsafe.c below 2 OKAY0.342
rec2_safe.c below 2 PASS0.347
rec2_unsafe.c below 2 OKAY0.348
rec-test.c below 2 PASS0.334
sas03_bothbranches.c below 7 PASS0.828
sas03.c below 2 PASS0.668
simulated_lese_recursive.c below 2 PASS0.375
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 4/4
ICRA Time = 305.314
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.329
count_up_down_unsafe.c below 1 OKAY0.323
divide.c below 1 PASS0.337
factor_unsafe.c below 1 OKAY0.326
for_infinite_loop_1_safe.c below 1 PASS0.316
for_infinite_loop_2_safe.c below 1 PASS0.32
interproc.c below 1 PASS0.312
mult.c below 1 PASS0.32
pointer_arith.c below 1 PASS0.324
quotient.c below 3 PASS0.413
subtract.c below 1 PASS0.329
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.339
sum01_bug02_unsafe.c below 1 OKAY0.378
sum01_real_safe.c below 1 PASS0.326
sum01_safe.c below 1 PASS0.336
sum01_unsafe.c below 1 OKAY0.363
sum02_safe.c below 1 PASS0.316
sum03_safe.c below 1 PASS0.319
sum03_unsafe.c below 1 OKAY0.357
sum04_safe.c below 1 PASS0.303
sum04_unsafe.c below 1 OKAY0.354
terminator_02_safe.c below 1 PASS0.315
terminator_02_unsafe.c below 1 OKAY0.35
terminator_03_safe.c below 1 PASS0.341
terminator_03_unsafe.c below 1 OKAY0.342
token_ring01_safe.c below TIMEOUT 300.005
token_ring01_unsafe.c below TIMEOUT 300.004
toy_safe.c below EXCEPTION 184.294
trex01_safe.c below 1 PASS0.556
trex01_unsafe.c below 1 OKAY0.366
trex02_safe2.c below 3 PASS0.379
trex02_safe.c below 3 PASS0.356
trex02_unsafe.c below 3 OKAY0.37
trex03_safe.c below 1 PASS0.44
trex03_unsafe.c below 1 OKAY0.428
trex04_safe.c below 1 PASS0.341
while_infinite_loop_1_safe.c below 1 PASS0.308
while_infinite_loop_2_safe.c below 1 PASS0.298
while_infinite_loop_3_safe.c below 1 PASS0.314
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 796.847
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.384
blogger_simplified1.c below 3 PASS0.715
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.344
mult-proc-params.c below 3 PASS0.39
popall.c below 1 PASS0.375
simulated_scc.c below 1 PASS0.452
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 302.664
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.344
degree2_binomial.c below 1 PASS0.401
degree2_monomial.c below 1 PASS0.349
degree3_binomial.c below 1 PASS1.175
degree3_monomial.c below 1 PASS0.375
degree4_binomial.c below 1 PASS4.533
degree4_monomial.c below 1 PASS0.42
degree5_binomial.c below 1 TIMEOUT300.006
degree5_monomial.c below 1 PASS0.5
ICRA Assertions (True) = 8/9
ICRA Assertions (False) = 0/0
ICRA Time = 308.103
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.348
cubic_with_square_interproc.c below 2 PASS0.38
cubic_with_square_nonlinear.c below 1 PASS0.347
cubic_with_square_nonlinear_interproc.c below 2 PASS0.359
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.349
cubic_with_square_unsafe.c below 1 OKAY0.324
multi-input.c below 1 PASS0.388
multi-input_unsafe.c below 1 OKAY0.41
nondet_loop_bound.c below 1 PASS0.351
nondet_loop_bound_quartic.c below 1 PASS0.359
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.348
nondet_loop_bound_unsafe.c below 1 OKAY0.378
nonlinear_stratified.c below 1 FAIL0.335
nonlinear_stratified_unsafe.c below 1 OKAY0.341
quartic_with_cube.c below 1 PASS0.336
quartic_with_cube_nonlinear.c below 1 PASS0.351
quartic_with_cube_nonlinear_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube_unsafe.c below 1 OKAY0.324
quintic_with_quartic.c below 1 PASS0.341
quintic_with_quartic_nonlinear.c below 1 PASS0.366
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.366
quintic_with_quartic_unsafe.c below 1 OKAY0.35
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 9/10
ICRA Time = 307.455
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.45
degree2_FD_AllAux_AllAssm.c below 1 PASS2.484
degree2_FD_AllAux_FewAssm.c below 1 PASS4.313
degree2_FD_FewAux_FewAssm.c below 1 PASS0.581
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.575
degree3.c below 1 PASS0.472
degree3_FD.c below 1 PASS0.588
degree4.c below 1 PASS0.367
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 9.83
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.367
loop_unsafe.c below 1 OKAY0.379
simulated_lese_parser.c below 1 PASS0.309
simulated_lese_sentinel.c below 1 PASS0.334
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.389
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.321
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.321
/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.323
array_false-unreach-call2.c below 1 OKAY0.343
array_false-unreach-call3.c below 1 OKAY0.329
array_true-unreach-call1.c below 1 FAIL0.328
array_true-unreach-call2.c below 1 FAIL0.337
array_true-unreach-call3.c below 1 PASS0.33
array_true-unreach-call4.c below 1 FAIL0.328
const_false-unreach-call1.c below 1 OKAY0.316
const_true-unreach-call1.c below 1 PASS0.31
diamond_false-unreach-call1.c below 1 OKAY0.325
diamond_true-unreach-call1.c below 1 PASS0.325
diamond_true-unreach-call2.c below 1 PASS0.357
functions_false-unreach-call1.c below 3 OKAY0.337
functions_true-unreach-call1.c below 3 PASS0.338
multivar_false-unreach-call1.c below 1 OKAY0.314
multivar_true-unreach-call1.c below 1 PASS0.311
nested_false-unreach-call1.c below 1 OKAY0.327
nested_true-unreach-call1.c below 1 PASS0.326
overflow_true-unreach-call1.c below 1 PASS0.304
phases_false-unreach-call1.c below 1 OKAY0.323
phases_false-unreach-call2.c below 1 OKAY0.325
phases_true-unreach-call1.c below 1 PASS0.326
phases_true-unreach-call2.c below 1 PASS0.331
simple_false-unreach-call1.c below 1 OKAY0.316
simple_false-unreach-call2.c below 1 OKAY0.308
simple_false-unreach-call3.c below 1 OKAY0.308
simple_false-unreach-call4.c below 1 OKAY0.309
simple_true-unreach-call1.c below 1 PASS0.304
simple_true-unreach-call2.c below 1 PASS0.302
simple_true-unreach-call3.c below 1 PASS0.319
simple_true-unreach-call4.c below 1 PASS0.313
underapprox_false-unreach-call1.c below 1 OKAY0.313
underapprox_false-unreach-call2.c below 1 OKAY0.321
underapprox_true-unreach-call1.c below 1 FAIL0.322
underapprox_true-unreach-call2.c below 1 PASS0.31
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 11.258
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.733
apache-get-tag_true-unreach-call.c below 1 FAIL0.435
down_true-unreach-call.c below 1 PASS0.323
fragtest_simple_true-unreach-call.c below 1 PASS0.362
half_2_true-unreach-call.c below 1 PASS0.349
heapsort_true-unreach-call.c below 1 PASS11.446
id_build_true-unreach-call.c below 1 PASS0.319
id_trans_false-unreach-call.c below 1 OKAY0.32
large_const_true-unreach-call.c below 1 PASS0.384
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.353
nested6_true-unreach-call.c below 1 FAIL0.385
nested9_true-unreach-call.c below 1 PASS0.424
nest-if3_true-unreach-call.c below 1 PASS0.375
NetBSD_loop_true-unreach-call.c below 1 PASS0.321
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.363
seq_true-unreach-call.c below 1 PASS0.369
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.095
string_concat-noarr_true-unreach-call.c below 1 PASS0.335
up_true-unreach-call.c below 1 PASS0.324
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 318.015
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.31
bhmr2007_true-unreach-call.c below 1 PASS0.334
cggmp2005b_true-unreach-call.c below 1 PASS0.378
cggmp2005_true-unreach-call.c below 1 PASS0.315
cggmp2005_variant_true-unreach-call.c below 1 PASS0.319
css2003_true-unreach-call.c below 1 PASS0.43
ddlm2013_true-unreach-call.c below 1 PASS0.357
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.17
gj2007b_true-unreach-call.c below 1 FAIL0.332
gj2007_true-unreach-call.c below 1 PASS0.334
gr2006_true-unreach-call.c below 1 PASS0.325
gsv2008_true-unreach-call.c below 1 PASS0.312
hhk2008_true-unreach-call.c below 1 PASS0.31
jm2006_true-unreach-call.c below 1 PASS0.334
jm2006_variant_true-unreach-call.c below 1 PASS0.345
mcmillan2006_true-unreach-call.c below 1 FAIL0.36
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.265
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.304
count_by_1_variant_true-unreach-call.c below 1 PASS0.317
count_by_2_true-unreach-call.c below 1 PASS0.31
count_by_k_true-unreach-call.c below 1 PASS0.318
count_by_nondet_true-unreach-call.c below 1 FAIL0.326
gauss_sum_true-unreach-call.c below 1 PASS0.322
half_true-unreach-call.c below EXCEPTION 0.325
nested_true-unreach-call.c below 1 PASS0.361
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.583
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.366
array_true-unreach-call.c below 1 FAIL0.379
bubble_sort_false-unreach-call.c below 4 OKAY99.101
bubble_sort_true-unreach-call.c below 1 PASS2.074
compact_false-unreach-call.c below 1 OKAY0.338
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.313
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.314
eureka_01_false-unreach-call.c below 1 OKAY1.482
eureka_01_true-unreach-call.c below 1 FAIL1.32
eureka_05_true-unreach-call.c below 1 FAIL0.71
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.334
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.298
heavy_false-unreach-call.c below 1 OKAY0.45
heavy_true-unreach-call.c below 1 PASS0.426
insertion_sort_false-unreach-call.c below 1 OKAY1.281
insertion_sort_true-unreach-call.c below 1 FAIL0.551
invert_string_false-unreach-call.c below 1 OKAY0.426
invert_string_true-unreach-call.c below 1 FAIL0.433
linear_sea.ch_true-unreach-call.c below 1 FAIL0.361
linear_search_false-unreach-call.c below 1 UNSOUND0.379
lu.cmp_true-unreach-call.c below TIMEOUT 300.252
ludcmp_false-unreach-call.c below TIMEOUT 300.231
matrix_false-unreach-call_true-termination.c below 1 OKAY0.759
matrix_true-unreach-call_true-termination.c below 1 FAIL0.431
n.c11_true-unreach-call.c below 3 FAIL0.423
n.c24_false-unreach-call.c below 3 OKAY11.502
n.c40_true-unreach-call.c below 1 FAIL0.334
nec11_false-unreach-call.c below 1 OKAY0.353
nec20_false-unreach-call.c below 1 OKAY0.359
nec40_true-unreach-call.c below 1 FAIL0.338
string_false-unreach-call.c below 1 OKAY0.539
string_true-unreach-call.c below 1 FAIL0.525
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.373
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.324
sum01_false-unreach-call_true-termination.c below 1 OKAY0.359
sum01_true-unreach-call_true-termination.c below 1 PASS0.32
sum03_false-unreach-call_true-termination.c below 1 OKAY0.397
sum03_true-unreach-call_false-termination.c below 1 PASS0.347
sum04_false-unreach-call_true-termination.c below 1 OKAY0.332
sum04_true-unreach-call_true-termination.c below 1 PASS0.328
sum_array_false-unreach-call.c below 1 OKAY0.499
sum_array_true-unreach-call.c below 1 FAIL0.536
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.327
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.387
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.336
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.323
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.315
trex01_false-unreach-call_true-termination.c below 3 OKAY0.431
trex01_true-unreach-call.c below 3 PASS0.721
trex02_false-unreach-call_true-termination.c below 3 OKAY0.364
trex02_true-unreach-call_true-termination.c below 3 PASS0.362
trex03_false-unreach-call_true-termination.c below 3 OKAY0.673
trex03_true-unreach-call.c below 3 PASS0.653
trex04_true-unreach-call_false-termination.c below 1 PASS0.371
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.341
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS12.536
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.346
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.335
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY7.78
vogal_false-unreach-call.c below 1 OKAY0.66
vogal_true-unreach-call.c below 1 FAIL0.718
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.31
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.297
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.293
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.315
ICRA Assertions (True) = 20/34
ICRA Assertions (False) = 30/32
ICRA Time = 760.702
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below TIMEOUT 300.022
Ackermann02_false-unreach-call_false-termination.c below TIMEOUT 300.027
Ackermann03_true-unreach-call.c below TIMEOUT 300.023
Ackermann04_true-unreach-call.c below TIMEOUT 300.023
Addition01_true-unreach-call_true-termination.c below 2 PASS0.472
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.478
Addition03_false-no-overflow.c below 2 PASS0.491
Addition03_true-unreach-call.c below 2 PASS0.493
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.399
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.411
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.392
Fibonacci01_true-unreach-call.c below EXCEPTION 0.696
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.666
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 0.682
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 0.675
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 0.674
gcd01_true-unreach-call_true-termination.c below 2 PASS0.457
gcd02_true-unreach-call.c below 2 FAIL0.845
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.912
McCarthy91_true-unreach-call.c below 7 FAIL0.88
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.536
Primes_true-unreach-call.c below 3 FAIL1.363
recHanoi01_true-unreach-call_true-termination.c below TIMEOUT 300.005
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.357
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.344
ICRA Assertions (True) = 5/18
ICRA Assertions (False) = 4/7
ICRA Time = 1512.323
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.372
afterrec_2calls_true-unreach-call.c below 2 PASS0.353
afterrec_false-unreach-call.c below 2 OKAY0.334
afterrec_true-unreach-call.c below 2 PASS0.335
fibo_10_false-unreach-call.c below EXCEPTION 0.667
fibo_10_true-unreach-call.c below EXCEPTION 0.64
fibo_15_false-unreach-call.c below EXCEPTION 0.651
fibo_15_true-unreach-call.c below EXCEPTION 0.637
fibo_20_false-unreach-call.c below EXCEPTION 0.647
fibo_20_true-unreach-call.c below EXCEPTION 0.642
fibo_25_false-unreach-call.c below EXCEPTION 0.66
fibo_25_true-unreach-call.c below EXCEPTION 0.648
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.162
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.163
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.163
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.164
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.147
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.161
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.164
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.16
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.17
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.17
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.164
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.162
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.098
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.17
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.158
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.163
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.162
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.16
fibo_5_false-unreach-call.c below EXCEPTION 0.653
fibo_5_true-unreach-call.c below EXCEPTION 0.668
fibo_7_false-unreach-call.c below EXCEPTION 0.645
fibo_7_true-unreach-call.c below EXCEPTION 0.655
id2_b2_o3_true-unreach-call.c below 2 PASS0.636
id2_b3_o2_false-unreach-call.c below 2 OKAY0.648
id2_b3_o5_true-unreach-call.c below 2 PASS0.636
id2_b5_o10_true-unreach-call.c below 2 PASS0.618
id2_i5_o5_false-unreach-call.c below 2 OKAY0.381
id2_i5_o5_true-unreach-call.c below 2 PASS0.363
id_b2_o3_true-unreach-call.c below 2 PASS0.462
id_b3_o2_false-unreach-call.c below 2 OKAY0.461
id_b3_o5_true-unreach-call.c below 2 PASS0.473
id_b5_o10_true-unreach-call.c below 2 PASS0.474
id_i10_o10_false-unreach-call.c below 2 OKAY0.339
id_i10_o10_true-unreach-call.c below 2 PASS0.36
id_i15_o15_false-unreach-call.c below 2 OKAY0.351
id_i15_o15_true-unreach-call.c below 2 PASS0.344
id_i20_o20_false-unreach-call.c below 2 OKAY0.346
id_i20_o20_true-unreach-call.c below 2 PASS0.337
id_i25_o25_false-unreach-call.c below 2 OKAY0.342
id_i25_o25_true-unreach-call.c below 2 PASS0.345
id_i5_o5_false-unreach-call.c below 2 OKAY0.341
id_i5_o5_true-unreach-call.c below 2 PASS0.345
id_o1000_false-unreach-call.c below 2 OKAY0.346
id_o100_false-unreach-call.c below 2 OKAY0.34
id_o10_false-unreach-call.c below 2 OKAY0.347
id_o200_false-unreach-call.c below 2 OKAY0.349
id_o20_false-unreach-call.c below 2 OKAY0.343
id_o3_false-unreach-call.c below 2 OKAY0.357
sum_10x0_false-unreach-call.c below 2 OKAY0.358
sum_10x0_true-unreach-call.c below 2 PASS0.352
sum_15x0_false-unreach-call.c below 2 OKAY0.359
sum_15x0_true-unreach-call.c below 2 PASS0.346
sum_20x0_false-unreach-call.c below 2 OKAY0.359
sum_20x0_true-unreach-call.c below 2 PASS0.354
sum_25x0_false-unreach-call.c below 2 OKAY0.351
sum_25x0_true-unreach-call.c below 2 PASS0.363
sum_2x3_false-unreach-call.c below 2 OKAY0.35
sum_2x3_true-unreach-call.c below 2 PASS0.357
sum_non_eq_false-unreach-call.c below 2 OKAY0.38
sum_non_eq_true-unreach-call.c below 2 PASS0.367
sum_non_false-unreach-call.c below 2 OKAY0.361
sum_non_true-unreach-call.c below 2 PASS0.368
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 5427.777
/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.347
rec-bhmr2007_true-unreach-call.c below 2 PASS0.367
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.568
rec-cggmp2005_true-unreach-call.c below 2 PASS0.327
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.338
rec-css2003_true-unreach-call.c below 2 PASS0.532
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.338
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.647
rec-gj2007b_true-unreach-call.c below 2 FAIL0.353
rec-gj2007_true-unreach-call.c below 2 FAIL0.373
rec-gr2006_true-unreach-call.c below 2 FAIL0.38
rec-gsv2008_true-unreach-call.c below 2 PASS0.34
rec-hhk2008_true-unreach-call.c below 2 PASS0.334
rec-jm2006_true-unreach-call.c below 2 PASS0.358
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.376
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.39
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 6.368
/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.331
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.348
rec-count_by_2_true-unreach-call.c below 2 PASS0.33
rec-count_by_k_true-unreach-call.c below 2 PASS0.346
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.367
rec-gauss_sum_true-unreach-call.c below 2 PASS0.346
rec-half_true-unreach-call.c below EXCEPTION 0.335
rec-nested_true-unreach-call.c below 3 PASS0.484
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.887
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.467
edit_distance_bottom_up.c below 3 FAIL163.46
edit_distance_top_down.c below 3 FAIL17.637
log_log_n_solution.c below 3 FAIL0.385
log_n_solution.c below 2 FAIL0.391
multivariate_1.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL9.917
n_cubed_solution.c below EXCEPTION 0.329
n_log_n_solution.c below TIMEOUT 300.022
n_squared_two_base_case_even.c below 2 PASS0.354
n_squared_two_base_case_odd.c below 2 PASS0.367
pascals_dynamic.c below 3 FAIL9.084
pascals_iterative.c below 1 FAIL2.892
pascals_recursive.c below TIMEOUT 300.006
squared_solution.c below TIMEOUT 300.127
two_n_even.c below 2 PASS0.354
two_n_odd.c below 2 PASS0.344
two_to_n_over_two_even.c below TIMEOUT 300.007
two_to_n_over_two_odd.c below TIMEOUT 300.007
two_to_n_squared.c below 7 FAIL170.319
two_to_two_to_n.c below 7 FAIL0.972
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 0/0
ICRA Time = 2177.446
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.308
binary_search_array_tree.c below 1 FAIL0.826
exp_add_loop_rec.c below 1 FAIL0.326
exp_add_loop_variable.c below 1 PASS0.33
exp_with_linear_inner_loop.c below 1 FAIL0.358
halving_log1.c below 1 PASS0.423
linear_two_to_n.c below TIMEOUT 300.005
loop_five_to_n.c below 1 FAIL0.341
non_loop_five_to_n.c below TIMEOUT 300.007
power_log.c below 1 PASS0.397
power_log_modified.c below 1 PASS0.424
simple_exponential.c below 1 PASS0.335
simple_exponential_for.c below 1 PASS0.324
two_to_n_minus_n.c below EXCEPTION 2.61
two_to_n_minus_n_loop.c below EXCEPTION 1.834
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 0/0
ICRA Time = 608.848