[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.341
kmp.c below 1 PASS0.974
qsort.c below 5 PASS1.804
speed_pldi09_fig1.c below 1 PASS0.373
speed_pldi09_fig4_2.c below 1 FAIL0.368
speed_pldi09_fig4_4.c below 1 PASS0.412
speed_pldi09_fig4_5.c below 1 PASS0.35
speed_pldi10_ex1.c below 1 PASS3.238
speed_pldi10_ex3.c below 1 PASS0.409
speed_pldi10_ex4.c below 1 PASS0.41
speed_popl10_fig2_1.c below 1 PASS0.357
speed_popl10_fig2_2.c below 1 FAIL0.368
speed_popl10_nested_multiple.c below 1 PASS0.4
speed_popl10_nested_single.c below 1 PASS0.374
speed_popl10_sequential_single.c below 1 PASS0.336
speed_popl10_simple_multiple.c below 1 PASS0.356
speed_popl10_simple_single_2.c below 1 PASS0.374
speed_popl10_simple_single.c below 1 PASS0.323
t07.c below 1 PASS0.351
t08.c below 1 PASS0.34
t09.c below 1 PASS0.327
t10.c below 1 PASS0.33
t11.c below 1 PASS0.363
t13.c below 1 FAIL0.365
t15.c below 1 PASS0.352
t16.c below 1 PASS0.347
t19.c below 1 PASS0.35
t20.c below 1 PASS0.332
t27.c below 1 PASS0.393
t28.c below 1 PASS0.372
t30.c below 1 FAIL0.336
t37.c below 2 PASS0.439
t39.c below 2 PASS0.43
t46.c below 1 PASS0.353
t47.c below 1 PASS0.336
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 17.683
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.358
qsort_full.c below 7 TIMEOUT 300.005
rec1-param_safe.c below 2 PASS0.328
rec1-param_unsafe.c below 2 OKAY0.328
rec1_safe.c below 2 PASS0.328
rec1_unsafe.c below 2 OKAY0.336
rec2-param_safe.c below 2 PASS0.332
rec2-param_unsafe.c below 2 OKAY0.337
rec2_safe.c below 2 PASS0.321
rec2_unsafe.c below 2 OKAY0.337
rec-test.c below 2 PASS0.319
sas03_bothbranches.c below 7 PASS0.787
sas03.c below 2 PASS0.64
simulated_lese_recursive.c below 2 PASS0.347
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 4/4
ICRA Time = 305.103
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.311
count_up_down_unsafe.c below 1 OKAY0.325
divide.c below 1 PASS0.303
factor_unsafe.c below 1 OKAY0.311
for_infinite_loop_1_safe.c below 1 PASS0.298
for_infinite_loop_2_safe.c below 1 PASS0.318
interproc.c below 1 PASS0.313
mult.c below 1 PASS0.308
pointer_arith.c below 1 PASS0.308
quotient.c below 3 PASS0.379
subtract.c below 1 PASS0.312
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.317
sum01_bug02_unsafe.c below 1 OKAY0.351
sum01_real_safe.c below 1 PASS0.315
sum01_safe.c below 1 PASS0.305
sum01_unsafe.c below 1 OKAY0.337
sum02_safe.c below 1 PASS0.32
sum03_safe.c below 1 PASS0.332
sum03_unsafe.c below 1 OKAY0.361
sum04_safe.c below 1 PASS0.306
sum04_unsafe.c below 1 OKAY0.343
terminator_02_safe.c below 1 PASS0.32
terminator_02_unsafe.c below 1 OKAY0.332
terminator_03_safe.c below 1 PASS0.305
terminator_03_unsafe.c below 1 OKAY0.31
token_ring01_safe.c below TIMEOUT 300.006
token_ring01_unsafe.c below TIMEOUT 300.005
toy_safe.c below EXCEPTION 164.694
trex01_safe.c below 1 PASS0.514
trex01_unsafe.c below 1 OKAY0.347
trex02_safe2.c below 3 PASS0.353
trex02_safe.c below 3 PASS0.372
trex02_unsafe.c below 3 OKAY0.357
trex03_safe.c below 1 PASS0.404
trex03_unsafe.c below 1 OKAY0.415
trex04_safe.c below 1 PASS0.33
while_infinite_loop_1_safe.c below 1 PASS0.31
while_infinite_loop_2_safe.c below 1 PASS0.3
while_infinite_loop_3_safe.c below 1 PASS0.314
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 776.761
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.373
blogger_simplified1.c below 3 PASS0.71
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.338
mult-proc-params.c below 3 PASS0.374
popall.c below 1 PASS0.372
simulated_scc.c below 1 PASS0.456
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 302.627
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.332
degree2_binomial.c below 1 PASS0.404
degree2_monomial.c below 1 PASS0.361
degree3_binomial.c below 1 PASS1.145
degree3_monomial.c below 1 PASS0.378
degree4_binomial.c below 1 PASS4.461
degree4_monomial.c below 1 PASS0.421
degree5_binomial.c below 1 TIMEOUT300.005
degree5_monomial.c below 1 PASS0.501
ICRA Assertions (True) = 8/9
ICRA Assertions (False) = 0/0
ICRA Time = 308.008
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.324
cubic_with_square_interproc.c below 2 PASS0.361
cubic_with_square_nonlinear.c below 1 PASS0.335
cubic_with_square_nonlinear_interproc.c below 2 PASS0.35
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.348
cubic_with_square_unsafe.c below 1 OKAY0.327
multi-input.c below 1 PASS0.4
multi-input_unsafe.c below 1 OKAY0.424
nondet_loop_bound.c below 1 PASS0.344
nondet_loop_bound_quartic.c below 1 PASS0.353
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.335
nondet_loop_bound_unsafe.c below 1 OKAY0.359
nonlinear_stratified.c below 1 FAIL0.347
nonlinear_stratified_unsafe.c below 1 OKAY0.339
quartic_with_cube.c below 1 PASS0.342
quartic_with_cube_nonlinear.c below 1 PASS0.345
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.346
quintic_with_quartic_nonlinear.c below 1 PASS0.368
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.36
quintic_with_quartic_unsafe.c below 1 OKAY0.349
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.433
degree2_FD_AllAux_AllAssm.c below 1 PASS2.416
degree2_FD_AllAux_FewAssm.c below 1 PASS4.178
degree2_FD_FewAux_FewAssm.c below 1 PASS0.571
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.589
degree3.c below 1 PASS0.475
degree3_FD.c below 1 PASS0.564
degree4.c below 1 PASS0.361
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 9.587
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.375
loop_unsafe.c below 1 OKAY0.38
simulated_lese_parser.c below 1 PASS0.314
simulated_lese_sentinel.c below 1 PASS0.33
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.399
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.328
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.328
/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.331
array_false-unreach-call2.c below 1 OKAY0.34
array_false-unreach-call3.c below 1 OKAY0.331
array_true-unreach-call1.c below 1 FAIL0.329
array_true-unreach-call2.c below 1 FAIL0.338
array_true-unreach-call3.c below 1 PASS0.335
array_true-unreach-call4.c below 1 FAIL0.332
const_false-unreach-call1.c below 1 OKAY0.314
const_true-unreach-call1.c below 1 PASS0.303
diamond_false-unreach-call1.c below 1 OKAY0.309
diamond_true-unreach-call1.c below 1 PASS0.333
diamond_true-unreach-call2.c below 1 PASS0.342
functions_false-unreach-call1.c below 3 OKAY0.338
functions_true-unreach-call1.c below 3 PASS0.332
multivar_false-unreach-call1.c below 1 OKAY0.311
multivar_true-unreach-call1.c below 1 PASS0.326
nested_false-unreach-call1.c below 1 OKAY0.324
nested_true-unreach-call1.c below 1 PASS0.317
overflow_true-unreach-call1.c below 1 PASS0.298
phases_false-unreach-call1.c below 1 OKAY0.32
phases_false-unreach-call2.c below 1 OKAY0.321
phases_true-unreach-call1.c below 1 PASS0.311
phases_true-unreach-call2.c below 1 PASS0.332
simple_false-unreach-call1.c below 1 OKAY0.305
simple_false-unreach-call2.c below 1 OKAY0.308
simple_false-unreach-call3.c below 1 OKAY0.311
simple_false-unreach-call4.c below 1 OKAY0.304
simple_true-unreach-call1.c below 1 PASS0.303
simple_true-unreach-call2.c below 1 PASS0.313
simple_true-unreach-call3.c below 1 PASS0.316
simple_true-unreach-call4.c below 1 PASS0.306
underapprox_false-unreach-call1.c below 1 OKAY0.312
underapprox_false-unreach-call2.c below 1 OKAY0.308
underapprox_true-unreach-call1.c below 1 FAIL0.308
underapprox_true-unreach-call2.c below 1 PASS0.309
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 11.17
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.715
apache-get-tag_true-unreach-call.c below 1 FAIL0.42
down_true-unreach-call.c below 1 PASS0.32
fragtest_simple_true-unreach-call.c below 1 PASS0.351
half_2_true-unreach-call.c below 1 PASS0.328
heapsort_true-unreach-call.c below 1 PASS11.488
id_build_true-unreach-call.c below 1 PASS0.314
id_trans_false-unreach-call.c below 1 OKAY0.32
large_const_true-unreach-call.c below 1 PASS0.381
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.341
nested6_true-unreach-call.c below 1 FAIL0.388
nested9_true-unreach-call.c below 1 PASS0.43
nest-if3_true-unreach-call.c below 1 PASS0.359
NetBSD_loop_true-unreach-call.c below 1 PASS0.326
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.351
seq_true-unreach-call.c below 1 PASS0.36
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.099
string_concat-noarr_true-unreach-call.c below 1 PASS0.321
up_true-unreach-call.c below 1 PASS0.328
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 317.94
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.312
bhmr2007_true-unreach-call.c below 1 PASS0.337
cggmp2005b_true-unreach-call.c below 1 PASS0.384
cggmp2005_true-unreach-call.c below 1 PASS0.301
cggmp2005_variant_true-unreach-call.c below 1 PASS0.313
css2003_true-unreach-call.c below 1 PASS0.412
ddlm2013_true-unreach-call.c below 1 PASS0.354
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.167
gj2007b_true-unreach-call.c below 1 FAIL0.346
gj2007_true-unreach-call.c below 1 PASS0.332
gr2006_true-unreach-call.c below 1 PASS0.324
gsv2008_true-unreach-call.c below 1 PASS0.311
hhk2008_true-unreach-call.c below 1 PASS0.312
jm2006_true-unreach-call.c below 1 PASS0.339
jm2006_variant_true-unreach-call.c below 1 PASS0.347
mcmillan2006_true-unreach-call.c below 1 FAIL0.363
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.254
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.307
count_by_1_variant_true-unreach-call.c below 1 PASS0.316
count_by_2_true-unreach-call.c below 1 PASS0.302
count_by_k_true-unreach-call.c below 1 PASS0.317
count_by_nondet_true-unreach-call.c below 1 FAIL0.322
gauss_sum_true-unreach-call.c below 1 PASS0.303
half_true-unreach-call.c below EXCEPTION 0.317
nested_true-unreach-call.c below 1 PASS0.364
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.548
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.373
array_true-unreach-call.c below 1 FAIL0.371
bubble_sort_false-unreach-call.c below 4 OKAY97.251
bubble_sort_true-unreach-call.c below 1 PASS2.067
compact_false-unreach-call.c below 1 OKAY0.342
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.302
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.296
eureka_01_false-unreach-call.c below 1 OKAY1.477
eureka_01_true-unreach-call.c below 1 FAIL1.31
eureka_05_true-unreach-call.c below 1 FAIL0.679
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.312
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.305
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.316
heavy_false-unreach-call.c below 1 OKAY0.443
heavy_true-unreach-call.c below 1 PASS0.424
insertion_sort_false-unreach-call.c below 1 OKAY1.254
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.42
linear_sea.ch_true-unreach-call.c below 1 FAIL0.358
linear_search_false-unreach-call.c below 1 UNSOUND0.39
lu.cmp_true-unreach-call.c below TIMEOUT 300.252
ludcmp_false-unreach-call.c below TIMEOUT 300.254
matrix_false-unreach-call_true-termination.c below 1 OKAY0.782
matrix_true-unreach-call_true-termination.c below 1 FAIL0.423
n.c11_true-unreach-call.c below 3 FAIL0.404
n.c24_false-unreach-call.c below 3 OKAY11.197
n.c40_true-unreach-call.c below 1 FAIL0.352
nec11_false-unreach-call.c below 1 OKAY0.353
nec20_false-unreach-call.c below 1 OKAY0.349
nec40_true-unreach-call.c below 1 FAIL0.355
string_false-unreach-call.c below 1 OKAY0.521
string_true-unreach-call.c below 1 FAIL0.523
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.36
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.335
sum01_false-unreach-call_true-termination.c below 1 OKAY0.357
sum01_true-unreach-call_true-termination.c below 1 PASS0.325
sum03_false-unreach-call_true-termination.c below 1 OKAY0.41
sum03_true-unreach-call_false-termination.c below 1 PASS0.34
sum04_false-unreach-call_true-termination.c below 1 OKAY0.35
sum04_true-unreach-call_true-termination.c below 1 PASS0.309
sum_array_false-unreach-call.c below 1 OKAY0.507
sum_array_true-unreach-call.c below 1 FAIL0.534
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.32
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.392
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.334
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.321
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.314
trex01_false-unreach-call_true-termination.c below 3 OKAY0.408
trex01_true-unreach-call.c below 3 PASS0.723
trex02_false-unreach-call_true-termination.c below 3 OKAY0.371
trex02_true-unreach-call_true-termination.c below 3 PASS0.374
trex03_false-unreach-call_true-termination.c below 3 OKAY0.65
trex03_true-unreach-call.c below 3 PASS0.653
trex04_true-unreach-call_false-termination.c below 1 PASS0.355
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.339
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS12.053
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.337
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.33
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY7.611
vogal_false-unreach-call.c below 1 OKAY0.661
vogal_true-unreach-call.c below 1 FAIL0.676
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.298
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.294
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.297
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.303
ICRA Assertions (True) = 20/34
ICRA Assertions (False) = 30/32
ICRA Time = 757.673
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below TIMEOUT 300.028
Ackermann02_false-unreach-call_false-termination.c below TIMEOUT 300.022
Ackermann03_true-unreach-call.c below TIMEOUT 300.02
Ackermann04_true-unreach-call.c below TIMEOUT 300.021
Addition01_true-unreach-call_true-termination.c below 2 PASS0.469
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.457
Addition03_false-no-overflow.c below 2 PASS0.465
Addition03_true-unreach-call.c below 2 PASS0.451
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.388
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.399
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.387
Fibonacci01_true-unreach-call.c below EXCEPTION 0.701
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.667
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 0.668
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 0.699
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 0.644
gcd01_true-unreach-call_true-termination.c below 2 PASS0.442
gcd02_true-unreach-call.c below 2 FAIL0.852
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.88
McCarthy91_true-unreach-call.c below 7 FAIL0.874
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.49
Primes_true-unreach-call.c below 3 FAIL1.297
recHanoi01_true-unreach-call_true-termination.c below TIMEOUT 300.006
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.348
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.354
ICRA Assertions (True) = 5/18
ICRA Assertions (False) = 4/7
ICRA Time = 1512.029
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.369
afterrec_2calls_true-unreach-call.c below 2 PASS0.374
afterrec_false-unreach-call.c below 2 OKAY0.331
afterrec_true-unreach-call.c below 2 PASS0.345
fibo_10_false-unreach-call.c below EXCEPTION 0.652
fibo_10_true-unreach-call.c below EXCEPTION 0.661
fibo_15_false-unreach-call.c below EXCEPTION 0.66
fibo_15_true-unreach-call.c below EXCEPTION 0.64
fibo_20_false-unreach-call.c below EXCEPTION 0.671
fibo_20_true-unreach-call.c below EXCEPTION 0.655
fibo_25_false-unreach-call.c below EXCEPTION 0.652
fibo_25_true-unreach-call.c below EXCEPTION 0.653
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.163
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.174
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.145
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.161
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.161
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.146
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.163
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.171
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.082
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.145
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.16
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.161
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.163
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.173
fibo_5_false-unreach-call.c below EXCEPTION 0.659
fibo_5_true-unreach-call.c below EXCEPTION 0.673
fibo_7_false-unreach-call.c below EXCEPTION 0.667
fibo_7_true-unreach-call.c below EXCEPTION 0.644
id2_b2_o3_true-unreach-call.c below 2 PASS0.608
id2_b3_o2_false-unreach-call.c below 2 OKAY0.653
id2_b3_o5_true-unreach-call.c below 2 PASS0.644
id2_b5_o10_true-unreach-call.c below 2 PASS0.633
id2_i5_o5_false-unreach-call.c below 2 OKAY0.381
id2_i5_o5_true-unreach-call.c below 2 PASS0.371
id_b2_o3_true-unreach-call.c below 2 PASS0.454
id_b3_o2_false-unreach-call.c below 2 OKAY0.46
id_b3_o5_true-unreach-call.c below 2 PASS0.478
id_b5_o10_true-unreach-call.c below 2 PASS0.471
id_i10_o10_false-unreach-call.c below 2 OKAY0.339
id_i10_o10_true-unreach-call.c below 2 PASS0.354
id_i15_o15_false-unreach-call.c below 2 OKAY0.343
id_i15_o15_true-unreach-call.c below 2 PASS0.345
id_i20_o20_false-unreach-call.c below 2 OKAY0.335
id_i20_o20_true-unreach-call.c below 2 PASS0.333
id_i25_o25_false-unreach-call.c below 2 OKAY0.344
id_i25_o25_true-unreach-call.c below 2 PASS0.348
id_i5_o5_false-unreach-call.c below 2 OKAY0.345
id_i5_o5_true-unreach-call.c below 2 PASS0.355
id_o1000_false-unreach-call.c below 2 OKAY0.362
id_o100_false-unreach-call.c below 2 OKAY0.346
id_o10_false-unreach-call.c below 2 OKAY0.343
id_o200_false-unreach-call.c below 2 OKAY0.347
id_o20_false-unreach-call.c below 2 OKAY0.355
id_o3_false-unreach-call.c below 2 OKAY0.37
sum_10x0_false-unreach-call.c below 2 OKAY0.362
sum_10x0_true-unreach-call.c below 2 PASS0.352
sum_15x0_false-unreach-call.c below 2 OKAY0.362
sum_15x0_true-unreach-call.c below 2 PASS0.354
sum_20x0_false-unreach-call.c below 2 OKAY0.355
sum_20x0_true-unreach-call.c below 2 PASS0.362
sum_25x0_false-unreach-call.c below 2 OKAY0.358
sum_25x0_true-unreach-call.c below 2 PASS0.348
sum_2x3_false-unreach-call.c below 2 OKAY0.354
sum_2x3_true-unreach-call.c below 2 PASS0.352
sum_non_eq_false-unreach-call.c below 2 OKAY0.365
sum_non_eq_true-unreach-call.c below 2 PASS0.361
sum_non_false-unreach-call.c below 2 OKAY0.367
sum_non_true-unreach-call.c below 2 PASS0.362
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 5427.849
/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.344
rec-bhmr2007_true-unreach-call.c below 2 PASS0.366
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.568
rec-cggmp2005_true-unreach-call.c below 2 PASS0.326
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.354
rec-css2003_true-unreach-call.c below 2 PASS0.541
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.326
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.652
rec-gj2007b_true-unreach-call.c below 2 FAIL0.361
rec-gj2007_true-unreach-call.c below 2 FAIL0.384
rec-gr2006_true-unreach-call.c below 2 FAIL0.368
rec-gsv2008_true-unreach-call.c below 2 PASS0.322
rec-hhk2008_true-unreach-call.c below 2 PASS0.332
rec-jm2006_true-unreach-call.c below 2 PASS0.348
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.363
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.395
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 6.35
/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.317
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.328
rec-count_by_2_true-unreach-call.c below 2 PASS0.316
rec-count_by_k_true-unreach-call.c below 2 PASS0.338
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.358
rec-gauss_sum_true-unreach-call.c below 2 PASS0.336
rec-half_true-unreach-call.c below EXCEPTION 0.318
rec-nested_true-unreach-call.c below 3 PASS0.51
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.821
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.464
edit_distance_bottom_up.c below 3 FAIL159.719
edit_distance_top_down.c below 3 FAIL17.641
log_log_n_solution.c below 3 FAIL0.395
log_n_solution.c below 2 FAIL0.391
multivariate_1.c below TIMEOUT 300.004
multivariate_higher_order.c below 7 FAIL10.023
n_cubed_solution.c below EXCEPTION 0.339
n_log_n_solution.c below TIMEOUT 300.026
n_squared_two_base_case_even.c below 2 PASS0.346
n_squared_two_base_case_odd.c below 2 PASS0.341
pascals_dynamic.c below 3 FAIL8.991
pascals_iterative.c below 1 FAIL2.919
pascals_recursive.c below TIMEOUT 300.005
squared_solution.c below TIMEOUT 300.129
two_n_even.c below 2 PASS0.343
two_n_odd.c below 2 PASS0.339
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 FAIL171.263
two_to_two_to_n.c below 7 FAIL0.997
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 0/0
ICRA Time = 2174.688
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.305
binary_search_array_tree.c below 1 FAIL0.854
exp_add_loop_rec.c below 1 FAIL0.322
exp_add_loop_variable.c below 1 PASS0.328
exp_with_linear_inner_loop.c below 1 FAIL0.378
halving_log1.c below 1 PASS0.396
linear_two_to_n.c below TIMEOUT 300.005
loop_five_to_n.c below 1 FAIL0.356
non_loop_five_to_n.c below TIMEOUT 300.006
power_log.c below 1 PASS0.398
power_log_modified.c below 1 PASS0.419
simple_exponential.c below 1 PASS0.321
simple_exponential_for.c below 1 PASS0.332
two_to_n_minus_n.c below EXCEPTION 2.615
two_to_n_minus_n_loop.c below EXCEPTION 1.82
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 0/0
ICRA Time = 608.855