[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.344
kmp.c below 1 PASS0.974
qsort.c below 5 PASS1.829
speed_pldi09_fig1.c below 1 PASS0.359
speed_pldi09_fig4_2.c below 1 FAIL0.367
speed_pldi09_fig4_4.c below 1 PASS0.405
speed_pldi09_fig4_5.c below 1 PASS0.35
speed_pldi10_ex1.c below 1 PASS3.24
speed_pldi10_ex3.c below 1 PASS0.403
speed_pldi10_ex4.c below 1 PASS0.396
speed_popl10_fig2_1.c below 1 PASS0.361
speed_popl10_fig2_2.c below 1 FAIL0.336
speed_popl10_nested_multiple.c below 1 PASS0.385
speed_popl10_nested_single.c below 1 PASS0.372
speed_popl10_sequential_single.c below 1 PASS0.334
speed_popl10_simple_multiple.c below 1 PASS0.358
speed_popl10_simple_single_2.c below 1 PASS0.38
speed_popl10_simple_single.c below 1 PASS0.327
t07.c below 1 PASS0.357
t08.c below 1 PASS0.34
t09.c below 1 PASS0.333
t10.c below 1 PASS0.334
t11.c below 1 PASS0.366
t13.c below 1 FAIL0.37
t15.c below 1 PASS0.36
t16.c below 1 PASS0.345
t19.c below 1 PASS0.328
t20.c below 1 PASS0.329
t27.c below 1 PASS0.392
t28.c below 1 PASS0.381
t30.c below 1 FAIL0.336
t37.c below 2 PASS0.443
t39.c below 2 PASS0.427
t46.c below 1 PASS0.339
t47.c below 1 PASS0.355
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 17.655
/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.33
rec1-param_unsafe.c below 2 OKAY0.333
rec1_safe.c below 2 PASS0.353
rec1_unsafe.c below 2 OKAY0.327
rec2-param_safe.c below 2 PASS0.335
rec2-param_unsafe.c below 2 OKAY0.322
rec2_safe.c below 2 PASS0.326
rec2_unsafe.c below 2 OKAY0.32
rec-test.c below 2 PASS0.328
sas03_bothbranches.c below 7 PASS0.788
sas03.c below 2 PASS0.627
simulated_lese_recursive.c below 2 PASS0.362
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 4/4
ICRA Time = 305.111
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.299
count_up_down_unsafe.c below 1 OKAY0.312
divide.c below 1 PASS0.325
factor_unsafe.c below 1 OKAY0.312
for_infinite_loop_1_safe.c below 1 PASS0.307
for_infinite_loop_2_safe.c below 1 PASS0.3
interproc.c below 1 PASS0.299
mult.c below 1 PASS0.326
pointer_arith.c below 1 PASS0.301
quotient.c below 3 PASS0.393
subtract.c below 1 PASS0.307
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.336
sum01_bug02_unsafe.c below 1 OKAY0.364
sum01_real_safe.c below 1 PASS0.309
sum01_safe.c below 1 PASS0.308
sum01_unsafe.c below 1 OKAY0.341
sum02_safe.c below 1 PASS0.313
sum03_safe.c below 1 PASS0.323
sum03_unsafe.c below 1 OKAY0.362
sum04_safe.c below 1 PASS0.313
sum04_unsafe.c below 1 OKAY0.333
terminator_02_safe.c below 1 PASS0.319
terminator_02_unsafe.c below 1 OKAY0.34
terminator_03_safe.c below 1 PASS0.31
terminator_03_unsafe.c below 1 OKAY0.309
token_ring01_safe.c below TIMEOUT 300.005
token_ring01_unsafe.c below TIMEOUT 300.004
toy_safe.c below EXCEPTION 163.498
trex01_safe.c below 1 PASS0.55
trex01_unsafe.c below 1 OKAY0.36
trex02_safe2.c below 3 PASS0.376
trex02_safe.c below 3 PASS0.354
trex02_unsafe.c below 3 OKAY0.35
trex03_safe.c below 1 PASS0.406
trex03_unsafe.c below 1 OKAY0.419
trex04_safe.c below 1 PASS0.344
while_infinite_loop_1_safe.c below 1 PASS0.293
while_infinite_loop_2_safe.c below 1 PASS0.297
while_infinite_loop_3_safe.c below 1 PASS0.301
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 775.618
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.368
blogger_simplified1.c below 3 PASS0.695
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.338
mult-proc-params.c below 3 PASS0.372
popall.c below 1 PASS0.394
simulated_scc.c below 1 PASS0.466
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 302.637
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.326
degree2_binomial.c below 1 PASS0.425
degree2_monomial.c below 1 PASS0.367
degree3_binomial.c below 1 PASS1.168
degree3_monomial.c below 1 PASS0.38
degree4_binomial.c below 1 PASS4.556
degree4_monomial.c below 1 PASS0.413
degree5_binomial.c below 1 TIMEOUT300.006
degree5_monomial.c below 1 PASS0.479
ICRA Assertions (True) = 8/9
ICRA Assertions (False) = 0/0
ICRA Time = 308.12
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.332
cubic_with_square_interproc.c below 2 PASS0.356
cubic_with_square_nonlinear.c below 1 PASS0.331
cubic_with_square_nonlinear_interproc.c below 2 PASS0.363
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.349
cubic_with_square_unsafe.c below 1 OKAY0.332
multi-input.c below 1 PASS0.389
multi-input_unsafe.c below 1 OKAY0.426
nondet_loop_bound.c below 1 PASS0.343
nondet_loop_bound_quartic.c below 1 PASS0.349
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.349
nondet_loop_bound_unsafe.c below 1 OKAY0.356
nonlinear_stratified.c below 1 FAIL0.343
nonlinear_stratified_unsafe.c below 1 OKAY0.341
quartic_with_cube.c below 1 PASS0.332
quartic_with_cube_nonlinear.c below 1 PASS0.341
quartic_with_cube_nonlinear_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube_unsafe.c below 1 OKAY0.327
quintic_with_quartic.c below 1 PASS0.344
quintic_with_quartic_nonlinear.c below 1 PASS0.36
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.377
quintic_with_quartic_unsafe.c below 1 OKAY0.34
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 9/10
ICRA Time = 307.384
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.432
degree2_FD_AllAux_AllAssm.c below 1 PASS2.434
degree2_FD_AllAux_FewAssm.c below 1 PASS4.272
degree2_FD_FewAux_FewAssm.c below 1 PASS0.583
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.606
degree3.c below 1 PASS0.496
degree3_FD.c below 1 PASS0.592
degree4.c below 1 PASS0.364
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 9.779
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.366
loop_unsafe.c below 1 OKAY0.377
simulated_lese_parser.c below 1 PASS0.322
simulated_lese_sentinel.c below 1 PASS0.331
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.396
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.322
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.322
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.005
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.005
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.318
array_false-unreach-call2.c below 1 OKAY0.349
array_false-unreach-call3.c below 1 OKAY0.326
array_true-unreach-call1.c below 1 FAIL0.321
array_true-unreach-call2.c below 1 FAIL0.341
array_true-unreach-call3.c below 1 PASS0.322
array_true-unreach-call4.c below 1 FAIL0.322
const_false-unreach-call1.c below 1 OKAY0.318
const_true-unreach-call1.c below 1 PASS0.301
diamond_false-unreach-call1.c below 1 OKAY0.329
diamond_true-unreach-call1.c below 1 PASS0.311
diamond_true-unreach-call2.c below 1 PASS0.353
functions_false-unreach-call1.c below 3 OKAY0.341
functions_true-unreach-call1.c below 3 PASS0.331
multivar_false-unreach-call1.c below 1 OKAY0.317
multivar_true-unreach-call1.c below 1 PASS0.313
nested_false-unreach-call1.c below 1 OKAY0.33
nested_true-unreach-call1.c below 1 PASS0.321
overflow_true-unreach-call1.c below 1 PASS0.324
phases_false-unreach-call1.c below 1 OKAY0.326
phases_false-unreach-call2.c below 1 OKAY0.327
phases_true-unreach-call1.c below 1 PASS0.308
phases_true-unreach-call2.c below 1 PASS0.329
simple_false-unreach-call1.c below 1 OKAY0.296
simple_false-unreach-call2.c below 1 OKAY0.305
simple_false-unreach-call3.c below 1 OKAY0.31
simple_false-unreach-call4.c below 1 OKAY0.306
simple_true-unreach-call1.c below 1 PASS0.309
simple_true-unreach-call2.c below 1 PASS0.307
simple_true-unreach-call3.c below 1 PASS0.304
simple_true-unreach-call4.c below 1 PASS0.303
underapprox_false-unreach-call1.c below 1 OKAY0.315
underapprox_false-unreach-call2.c below 1 OKAY0.302
underapprox_true-unreach-call1.c below 1 FAIL0.304
underapprox_true-unreach-call2.c below 1 PASS0.305
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 11.144
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.73
apache-get-tag_true-unreach-call.c below 1 FAIL0.424
down_true-unreach-call.c below 1 PASS0.318
fragtest_simple_true-unreach-call.c below 1 PASS0.352
half_2_true-unreach-call.c below 1 PASS0.334
heapsort_true-unreach-call.c below 1 PASS11.404
id_build_true-unreach-call.c below 1 PASS0.312
id_trans_false-unreach-call.c below 1 OKAY0.325
large_const_true-unreach-call.c below 1 PASS0.369
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.347
nested6_true-unreach-call.c below 1 FAIL0.378
nested9_true-unreach-call.c below 1 PASS0.423
nest-if3_true-unreach-call.c below 1 PASS0.363
NetBSD_loop_true-unreach-call.c below 1 PASS0.312
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.347
seq_true-unreach-call.c below 1 PASS0.376
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.1
string_concat-noarr_true-unreach-call.c below 1 PASS0.346
up_true-unreach-call.c below 1 PASS0.312
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 317.872
/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.333
cggmp2005b_true-unreach-call.c below 1 PASS0.361
cggmp2005_true-unreach-call.c below 1 PASS0.309
cggmp2005_variant_true-unreach-call.c below 1 PASS0.316
css2003_true-unreach-call.c below 1 PASS0.428
ddlm2013_true-unreach-call.c below 1 PASS0.349
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.166
gj2007b_true-unreach-call.c below 1 FAIL0.337
gj2007_true-unreach-call.c below 1 PASS0.338
gr2006_true-unreach-call.c below 1 PASS0.327
gsv2008_true-unreach-call.c below 1 PASS0.311
hhk2008_true-unreach-call.c below 1 PASS0.317
jm2006_true-unreach-call.c below 1 PASS0.333
jm2006_variant_true-unreach-call.c below 1 PASS0.332
mcmillan2006_true-unreach-call.c below 1 FAIL0.361
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.249
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.317
count_by_1_variant_true-unreach-call.c below 1 PASS0.31
count_by_2_true-unreach-call.c below 1 PASS0.31
count_by_k_true-unreach-call.c below 1 PASS0.309
count_by_nondet_true-unreach-call.c below 1 FAIL0.323
gauss_sum_true-unreach-call.c below 1 PASS0.321
half_true-unreach-call.c below EXCEPTION 0.308
nested_true-unreach-call.c below 1 PASS0.357
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.555
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.362
array_true-unreach-call.c below 1 FAIL0.365
bubble_sort_false-unreach-call.c below 4 OKAY96.815
bubble_sort_true-unreach-call.c below 1 PASS2.034
compact_false-unreach-call.c below 1 OKAY0.351
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.327
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.312
eureka_01_false-unreach-call.c below 1 OKAY1.476
eureka_01_true-unreach-call.c below 1 FAIL1.321
eureka_05_true-unreach-call.c below 1 FAIL0.694
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.313
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.297
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.304
heavy_false-unreach-call.c below 1 OKAY0.431
heavy_true-unreach-call.c below 1 PASS0.427
insertion_sort_false-unreach-call.c below 1 OKAY1.243
insertion_sort_true-unreach-call.c below 1 FAIL0.546
invert_string_false-unreach-call.c below 1 OKAY0.44
invert_string_true-unreach-call.c below 1 FAIL0.425
linear_sea.ch_true-unreach-call.c below 1 FAIL0.357
linear_search_false-unreach-call.c below 1 UNSOUND0.377
lu.cmp_true-unreach-call.c below TIMEOUT 300.24
ludcmp_false-unreach-call.c below TIMEOUT 300.246
matrix_false-unreach-call_true-termination.c below 1 OKAY0.774
matrix_true-unreach-call_true-termination.c below 1 FAIL0.414
n.c11_true-unreach-call.c below 3 FAIL0.41
n.c24_false-unreach-call.c below 3 OKAY11.44
n.c40_true-unreach-call.c below 1 FAIL0.338
nec11_false-unreach-call.c below 1 OKAY0.355
nec20_false-unreach-call.c below 1 OKAY0.351
nec40_true-unreach-call.c below 1 FAIL0.356
string_false-unreach-call.c below 1 OKAY0.526
string_true-unreach-call.c below 1 FAIL0.534
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.349
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.314
sum01_false-unreach-call_true-termination.c below 1 OKAY0.364
sum01_true-unreach-call_true-termination.c below 1 PASS0.322
sum03_false-unreach-call_true-termination.c below 1 OKAY0.403
sum03_true-unreach-call_false-termination.c below 1 PASS0.333
sum04_false-unreach-call_true-termination.c below 1 OKAY0.336
sum04_true-unreach-call_true-termination.c below 1 PASS0.316
sum_array_false-unreach-call.c below 1 OKAY0.495
sum_array_true-unreach-call.c below 1 FAIL0.547
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.318
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.38
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.338
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.313
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.323
trex01_false-unreach-call_true-termination.c below 3 OKAY0.406
trex01_true-unreach-call.c below 3 PASS0.729
trex02_false-unreach-call_true-termination.c below 3 OKAY0.376
trex02_true-unreach-call_true-termination.c below 3 PASS0.366
trex03_false-unreach-call_true-termination.c below 3 OKAY0.659
trex03_true-unreach-call.c below 3 PASS0.666
trex04_true-unreach-call_false-termination.c below 1 PASS0.357
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.329
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS12.241
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.332
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.335
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY7.637
vogal_false-unreach-call.c below 1 OKAY0.704
vogal_true-unreach-call.c below 1 FAIL0.642
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.294
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.29
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.313
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.305
ICRA Assertions (True) = 20/34
ICRA Assertions (False) = 30/32
ICRA Time = 757.633
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below TIMEOUT 300.029
Ackermann02_false-unreach-call_false-termination.c below TIMEOUT 300.022
Ackermann03_true-unreach-call.c below TIMEOUT 300.021
Ackermann04_true-unreach-call.c below TIMEOUT 300.021
Addition01_true-unreach-call_true-termination.c below 2 PASS0.459
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.482
Addition03_false-no-overflow.c below 2 PASS0.461
Addition03_true-unreach-call.c below 2 PASS0.468
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.386
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.39
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.375
Fibonacci01_true-unreach-call.c below EXCEPTION 0.655
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.645
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 0.682
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 0.645
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 0.667
gcd01_true-unreach-call_true-termination.c below 2 PASS0.457
gcd02_true-unreach-call.c below 2 FAIL0.854
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.885
McCarthy91_true-unreach-call.c below 7 FAIL0.912
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.52
Primes_true-unreach-call.c below 3 FAIL1.307
recHanoi01_true-unreach-call_true-termination.c below TIMEOUT 300.005
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.349
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.355
ICRA Assertions (True) = 5/18
ICRA Assertions (False) = 4/7
ICRA Time = 1512.052
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.38
afterrec_2calls_true-unreach-call.c below 2 PASS0.357
afterrec_false-unreach-call.c below 2 OKAY0.344
afterrec_true-unreach-call.c below 2 PASS0.324
fibo_10_false-unreach-call.c below EXCEPTION 0.676
fibo_10_true-unreach-call.c below EXCEPTION 0.657
fibo_15_false-unreach-call.c below EXCEPTION 0.666
fibo_15_true-unreach-call.c below EXCEPTION 0.669
fibo_20_false-unreach-call.c below EXCEPTION 0.669
fibo_20_true-unreach-call.c below EXCEPTION 0.653
fibo_25_false-unreach-call.c below EXCEPTION 0.665
fibo_25_true-unreach-call.c below EXCEPTION 0.656
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.168
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.164
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.161
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.162
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.161
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.161
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.143
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.163
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.16
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.161
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.161
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.16
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.084
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.16
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.161
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.146
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.171
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.161
fibo_5_false-unreach-call.c below EXCEPTION 0.659
fibo_5_true-unreach-call.c below EXCEPTION 0.664
fibo_7_false-unreach-call.c below EXCEPTION 0.657
fibo_7_true-unreach-call.c below EXCEPTION 0.643
id2_b2_o3_true-unreach-call.c below 2 PASS0.606
id2_b3_o2_false-unreach-call.c below 2 OKAY0.637
id2_b3_o5_true-unreach-call.c below 2 PASS0.63
id2_b5_o10_true-unreach-call.c below 2 PASS0.638
id2_i5_o5_false-unreach-call.c below 2 OKAY0.37
id2_i5_o5_true-unreach-call.c below 2 PASS0.373
id_b2_o3_true-unreach-call.c below 2 PASS0.468
id_b3_o2_false-unreach-call.c below 2 OKAY0.483
id_b3_o5_true-unreach-call.c below 2 PASS0.457
id_b5_o10_true-unreach-call.c below 2 PASS0.443
id_i10_o10_false-unreach-call.c below 2 OKAY0.343
id_i10_o10_true-unreach-call.c below 2 PASS0.347
id_i15_o15_false-unreach-call.c below 2 OKAY0.344
id_i15_o15_true-unreach-call.c below 2 PASS0.344
id_i20_o20_false-unreach-call.c below 2 OKAY0.337
id_i20_o20_true-unreach-call.c below 2 PASS0.342
id_i25_o25_false-unreach-call.c below 2 OKAY0.348
id_i25_o25_true-unreach-call.c below 2 PASS0.335
id_i5_o5_false-unreach-call.c below 2 OKAY0.357
id_i5_o5_true-unreach-call.c below 2 PASS0.34
id_o1000_false-unreach-call.c below 2 OKAY0.347
id_o100_false-unreach-call.c below 2 OKAY0.342
id_o10_false-unreach-call.c below 2 OKAY0.347
id_o200_false-unreach-call.c below 2 OKAY0.335
id_o20_false-unreach-call.c below 2 OKAY0.345
id_o3_false-unreach-call.c below 2 OKAY0.361
sum_10x0_false-unreach-call.c below 2 OKAY0.359
sum_10x0_true-unreach-call.c below 2 PASS0.35
sum_15x0_false-unreach-call.c below 2 OKAY0.351
sum_15x0_true-unreach-call.c below 2 PASS0.35
sum_20x0_false-unreach-call.c below 2 OKAY0.358
sum_20x0_true-unreach-call.c below 2 PASS0.353
sum_25x0_false-unreach-call.c below 2 OKAY0.359
sum_25x0_true-unreach-call.c below 2 PASS0.348
sum_2x3_false-unreach-call.c below 2 OKAY0.351
sum_2x3_true-unreach-call.c below 2 PASS0.345
sum_non_eq_false-unreach-call.c below 2 OKAY0.383
sum_non_eq_true-unreach-call.c below 2 PASS0.388
sum_non_false-unreach-call.c below 2 OKAY0.364
sum_non_true-unreach-call.c below 2 PASS0.356
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 5427.781
/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.338
rec-bhmr2007_true-unreach-call.c below 2 PASS0.371
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.579
rec-cggmp2005_true-unreach-call.c below 2 PASS0.332
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.367
rec-css2003_true-unreach-call.c below 2 PASS0.538
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.32
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.628
rec-gj2007b_true-unreach-call.c below 2 FAIL0.37
rec-gj2007_true-unreach-call.c below 2 FAIL0.361
rec-gr2006_true-unreach-call.c below 2 FAIL0.358
rec-gsv2008_true-unreach-call.c below 2 PASS0.329
rec-hhk2008_true-unreach-call.c below 2 PASS0.33
rec-jm2006_true-unreach-call.c below 2 PASS0.354
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.368
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.386
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 6.329
/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.328
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.32
rec-count_by_2_true-unreach-call.c below 2 PASS0.318
rec-count_by_k_true-unreach-call.c below 2 PASS0.33
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.344
rec-gauss_sum_true-unreach-call.c below 2 PASS0.33
rec-half_true-unreach-call.c below EXCEPTION 0.318
rec-nested_true-unreach-call.c below 3 PASS0.484
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.772
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.485
edit_distance_bottom_up.c below 3 FAIL163.146
edit_distance_top_down.c below 3 FAIL17.811
log_log_n_solution.c below 3 FAIL0.395
log_n_solution.c below 2 FAIL0.384
multivariate_1.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL9.997
n_cubed_solution.c below EXCEPTION 0.323
n_log_n_solution.c below TIMEOUT 300.021
n_squared_two_base_case_even.c below 2 PASS0.358
n_squared_two_base_case_odd.c below 2 PASS0.356
pascals_dynamic.c below 3 FAIL9.189
pascals_iterative.c below 1 FAIL2.933
pascals_recursive.c below TIMEOUT 300.005
squared_solution.c below TIMEOUT 300.13
two_n_even.c below 2 PASS0.342
two_n_odd.c below 2 PASS0.352
two_to_n_over_two_even.c below TIMEOUT 300.007
two_to_n_over_two_odd.c below TIMEOUT 300.006
two_to_n_squared.c below 7 FAIL172.281
two_to_two_to_n.c below 7 FAIL0.988
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 0/0
ICRA Time = 2179.514
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.302
binary_search_array_tree.c below 1 FAIL0.832
exp_add_loop_rec.c below 1 FAIL0.34
exp_add_loop_variable.c below 1 PASS0.346
exp_with_linear_inner_loop.c below 1 FAIL0.377
halving_log1.c below 1 PASS0.413
linear_two_to_n.c below TIMEOUT 300.006
loop_five_to_n.c below 1 FAIL0.326
non_loop_five_to_n.c below TIMEOUT 300.007
power_log.c below 1 PASS0.398
power_log_modified.c below 1 PASS0.414
simple_exponential.c below 1 PASS0.322
simple_exponential_for.c below 1 PASS0.334
two_to_n_minus_n.c below EXCEPTION 2.597
two_to_n_minus_n_loop.c below EXCEPTION 1.877
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 0/0
ICRA Time = 608.891