[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: 0fa8064dfa94888565bc782359017482a22e6f46 (2017-05-16 08:41:47 -0400) "Fixed build after merge"
# 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.349
kmp.c below 1 PASS1.315
qsort.c below 5 PASS3.525
speed_pldi09_fig1.c below 1 PASS0.405
speed_pldi09_fig4_2.c below 1 FAIL0.39
speed_pldi09_fig4_4.c below 1 PASS0.467
speed_pldi09_fig4_5.c below 1 PASS0.371
speed_pldi10_ex1.c below 1 PASS3.746
speed_pldi10_ex3.c below 1 PASS0.448
speed_pldi10_ex4.c below EXCEPTION 0.412
speed_popl10_fig2_1.c below 1 PASS0.408
speed_popl10_fig2_2.c below 1 FAIL0.358
speed_popl10_nested_multiple.c below 1 PASS0.431
speed_popl10_nested_single.c below 1 PASS0.417
speed_popl10_sequential_single.c below 1 PASS0.351
speed_popl10_simple_multiple.c below 1 PASS0.387
speed_popl10_simple_single_2.c below 1 PASS0.411
speed_popl10_simple_single.c below 1 PASS0.33
t07.c below 1 PASS0.37
t08.c below 1 PASS0.36
t09.c below 1 PASS0.365
t10.c below 1 PASS0.355
t11.c below 1 PASS0.377
t13.c below 1 FAIL0.386
t15.c below 1 PASS0.379
t16.c below 1 PASS0.347
t19.c below 1 PASS0.335
t20.c below 1 PASS0.34
t27.c below 1 PASS0.43
t28.c below 1 PASS0.378
t30.c below 1 FAIL0.345
t37.c below 2 PASS0.483
t39.c below 2 PASS0.501
t46.c below 1 PASS0.362
t47.c below 1 PASS0.363
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 20.997
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.392
qsort_full.c below 5 TIMEOUT 300.005
rec1-param_safe.c below 2 PASS0.333
rec1-param_unsafe.c below 2 OKAY0.359
rec1_safe.c below 2 PASS0.347
rec1_unsafe.c below 2 OKAY0.349
rec2-param_safe.c below 2 PASS0.351
rec2-param_unsafe.c below 2 OKAY0.352
rec2_safe.c below 2 PASS0.324
rec2_unsafe.c below 2 OKAY0.339
rec-test.c below 2 PASS0.332
sas03_bothbranches.c below 7 PASS1.274
sas03.c below 2 PASS0.849
simulated_lese_recursive.c below 2 PASS0.4
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 4/4
ICRA Time = 306.006
/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.32
divide.c below 1 PASS0.344
factor_unsafe.c below 1 OKAY0.339
for_infinite_loop_1_safe.c below 1 PASS0.32
for_infinite_loop_2_safe.c below 1 PASS0.319
interproc.c below 1 PASS0.319
mult.c below 1 PASS0.328
pointer_arith.c below 1 PASS0.315
quotient.c below 3 PASS0.414
subtract.c below 1 PASS0.311
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.35
sum01_bug02_unsafe.c below 1 OKAY0.383
sum01_real_safe.c below 1 PASS0.313
sum01_safe.c below 1 PASS0.327
sum01_unsafe.c below 1 OKAY0.36
sum02_safe.c below 1 PASS0.333
sum03_safe.c below 1 PASS0.345
sum03_unsafe.c below 1 OKAY0.398
sum04_safe.c below 1 PASS0.315
sum04_unsafe.c below 1 OKAY0.347
terminator_02_safe.c below 1 PASS0.326
terminator_02_unsafe.c below 1 OKAY0.356
terminator_03_safe.c below 1 PASS0.339
terminator_03_unsafe.c below 1 OKAY0.327
token_ring01_safe.c below TIMEOUT 300.005
token_ring01_unsafe.c below TIMEOUT 300.007
toy_safe.c below EXCEPTION 143.4
trex01_safe.c below 1 PASS0.731
trex01_unsafe.c below 1 OKAY0.396
trex02_safe2.c below 3 PASS0.39
trex02_safe.c below 3 PASS0.383
trex02_unsafe.c below 3 OKAY0.399
trex03_safe.c below 1 PASS0.486
trex03_unsafe.c below 1 OKAY0.466
trex04_safe.c below 1 PASS0.349
while_infinite_loop_1_safe.c below 1 PASS0.319
while_infinite_loop_2_safe.c below 1 PASS0.312
while_infinite_loop_3_safe.c below 1 PASS0.308
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 756.428
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.448
blogger_simplified1.c below 3 PASS1.015
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.363
mult-proc-params.c below 3 PASS0.407
popall.c below 1 PASS0.406
simulated_scc.c below 1 PASS0.528
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.171
/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.468
degree2_monomial.c below 1 PASS0.369
degree3_binomial.c below 1 PASS0.898
degree3_monomial.c below 1 PASS0.442
degree4_binomial.c below 1 PASS1.173
degree4_monomial.c below 1 PASS0.48
degree5_binomial.c below 1 PASS1.768
degree5_monomial.c below 1 PASS0.578
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 6.508
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.341
cubic_with_square_interproc.c below 2 PASS0.385
cubic_with_square_nonlinear.c below 1 PASS0.35
cubic_with_square_nonlinear_interproc.c below 2 PASS0.381
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.373
cubic_with_square_unsafe.c below 1 OKAY0.355
multi-input.c below 1 PASS0.445
multi-input_unsafe.c below 1 OKAY0.444
nondet_loop_bound.c below 1 PASS0.37
nondet_loop_bound_quartic.c below 1 PASS0.371
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.351
nondet_loop_bound_unsafe.c below 1 OKAY0.382
nonlinear_stratified.c below 1 FAIL0.367
nonlinear_stratified_unsafe.c below 1 OKAY0.37
quartic_with_cube.c below 1 PASS0.352
quartic_with_cube_nonlinear.c below 1 PASS0.361
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.37
quartic_with_cube_unsafe.c below 1 OKAY0.354
quintic_with_quartic.c below 1 PASS0.374
quintic_with_quartic_nonlinear.c below 1 PASS0.391
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.381
quintic_with_quartic_unsafe.c below 1 OKAY0.357
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 10/10
ICRA Time = 8.225
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.518
degree2_FD_AllAux_AllAssm.c below 1 PASS3.676
degree2_FD_AllAux_FewAssm.c below 1 PASS5.493
degree2_FD_FewAux_FewAssm.c below 1 PASS0.695
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.711
degree3.c below 1 PASS0.569
degree3_FD.c below 1 PASS0.701
degree4.c below 1 PASS0.386
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 12.749
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.389
loop_unsafe.c below 1 OKAY0.41
simulated_lese_parser.c below 1 PASS0.335
simulated_lese_sentinel.c below 1 PASS0.337
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.471
/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.015
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.015
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.344
array_false-unreach-call2.c below 1 OKAY0.355
array_false-unreach-call3.c below 1 OKAY0.336
array_true-unreach-call1.c below 1 FAIL0.349
array_true-unreach-call2.c below 1 FAIL0.375
array_true-unreach-call3.c below 1 PASS0.337
array_true-unreach-call4.c below 1 FAIL0.34
const_false-unreach-call1.c below 1 OKAY0.328
const_true-unreach-call1.c below 1 PASS0.319
diamond_false-unreach-call1.c below 1 OKAY0.332
diamond_true-unreach-call1.c below 1 PASS0.338
diamond_true-unreach-call2.c below 1 PASS0.37
functions_false-unreach-call1.c below 3 OKAY0.372
functions_true-unreach-call1.c below 3 PASS0.358
multivar_false-unreach-call1.c below 1 OKAY0.332
multivar_true-unreach-call1.c below 1 PASS0.333
nested_false-unreach-call1.c below 1 OKAY0.33
nested_true-unreach-call1.c below 1 PASS0.332
overflow_true-unreach-call1.c below 1 PASS0.313
phases_false-unreach-call1.c below 1 OKAY0.336
phases_false-unreach-call2.c below 1 OKAY0.34
phases_true-unreach-call1.c below 1 PASS0.327
phases_true-unreach-call2.c below 1 PASS0.35
simple_false-unreach-call1.c below 1 OKAY0.323
simple_false-unreach-call2.c below 1 OKAY0.331
simple_false-unreach-call3.c below 1 OKAY0.336
simple_false-unreach-call4.c below 1 OKAY0.324
simple_true-unreach-call1.c below 1 PASS0.331
simple_true-unreach-call2.c below 1 PASS0.321
simple_true-unreach-call3.c below 1 PASS0.314
simple_true-unreach-call4.c below 1 PASS0.32
underapprox_false-unreach-call1.c below 1 OKAY0.327
underapprox_false-unreach-call2.c below 1 OKAY0.336
underapprox_true-unreach-call1.c below 1 FAIL0.323
underapprox_true-unreach-call2.c below 1 PASS0.319
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 11.751
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.873
apache-get-tag_true-unreach-call.c below 1 FAIL0.46
down_true-unreach-call.c below 1 PASS0.34
fragtest_simple_true-unreach-call.c below 1 PASS0.377
half_2_true-unreach-call.c below 1 PASS0.349
heapsort_true-unreach-call.c below 1 TIMEOUT300.156
id_build_true-unreach-call.c below 1 PASS0.328
id_trans_false-unreach-call.c below 1 OKAY0.327
large_const_true-unreach-call.c below 1 PASS0.422
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.374
nested6_true-unreach-call.c below 1 FAIL0.429
nested9_true-unreach-call.c below 1 PASS0.45
nest-if3_true-unreach-call.c below 1 PASS0.413
NetBSD_loop_true-unreach-call.c below 1 PASS0.34
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.377
seq_true-unreach-call.c below 1 PASS0.366
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.115
string_concat-noarr_true-unreach-call.c below 1 PASS0.343
up_true-unreach-call.c below 1 PASS0.337
ICRA Assertions (True) = 13/18
ICRA Assertions (False) = 1/1
ICRA Time = 607.176
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.345
bhmr2007_true-unreach-call.c below 1 PASS0.361
cggmp2005b_true-unreach-call.c below 1 PASS0.396
cggmp2005_true-unreach-call.c below 1 PASS0.319
cggmp2005_variant_true-unreach-call.c below 1 PASS0.329
css2003_true-unreach-call.c below 1 PASS0.476
ddlm2013_true-unreach-call.c below 1 PASS0.389
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.168
gj2007b_true-unreach-call.c below 1 FAIL0.347
gj2007_true-unreach-call.c below 1 PASS0.338
gr2006_true-unreach-call.c below 1 PASS0.342
gsv2008_true-unreach-call.c below 1 PASS0.325
hhk2008_true-unreach-call.c below 1 PASS0.333
jm2006_true-unreach-call.c below 1 PASS0.351
jm2006_variant_true-unreach-call.c below 1 PASS0.367
mcmillan2006_true-unreach-call.c below 1 FAIL0.39
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.576
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.336
count_by_1_variant_true-unreach-call.c below 1 PASS0.327
count_by_2_true-unreach-call.c below 1 PASS0.318
count_by_k_true-unreach-call.c below 1 PASS0.329
count_by_nondet_true-unreach-call.c below 1 FAIL0.341
gauss_sum_true-unreach-call.c below 1 PASS0.344
half_true-unreach-call.c below EXCEPTION 0.336
nested_true-unreach-call.c below 1 PASS0.38
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.711
/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.415
bubble_sort_false-unreach-call.c below 4 OKAY140.538
bubble_sort_true-unreach-call.c below 1 PASS3.908
compact_false-unreach-call.c below 1 OKAY0.383
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.323
eureka_01_false-unreach-call.c below 1 OKAY2.173
eureka_01_true-unreach-call.c below 1 FAIL1.947
eureka_05_true-unreach-call.c below 1 FAIL1.067
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.326
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.302
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.312
heavy_false-unreach-call.c below 1 OKAY0.534
heavy_true-unreach-call.c below 1 PASS0.513
insertion_sort_false-unreach-call.c below 1 OKAY2.16
insertion_sort_true-unreach-call.c below 1 FAIL0.782
invert_string_false-unreach-call.c below 1 OKAY0.49
invert_string_true-unreach-call.c below 1 FAIL0.498
linear_sea.ch_true-unreach-call.c below 1 FAIL0.367
linear_search_false-unreach-call.c below 1 UNSOUND0.399
lu.cmp_true-unreach-call.c below TIMEOUT 300.271
ludcmp_false-unreach-call.c below TIMEOUT 300.286
matrix_false-unreach-call_true-termination.c below 1 OKAY1.225
matrix_true-unreach-call_true-termination.c below 1 FAIL0.527
n.c11_true-unreach-call.c below 3 FAIL0.482
n.c24_false-unreach-call.c below 3 OKAY23.502
n.c40_true-unreach-call.c below 1 FAIL0.378
nec11_false-unreach-call.c below 1 OKAY0.382
nec20_false-unreach-call.c below 1 OKAY0.365
nec40_true-unreach-call.c below 1 FAIL0.364
string_false-unreach-call.c below 1 OKAY0.658
string_true-unreach-call.c below 1 FAIL0.652
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.385
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.353
sum01_false-unreach-call_true-termination.c below 1 OKAY0.366
sum01_true-unreach-call_true-termination.c below 1 PASS0.324
sum03_false-unreach-call_true-termination.c below 1 OKAY0.461
sum03_true-unreach-call_false-termination.c below 1 PASS0.36
sum04_false-unreach-call_true-termination.c below 1 OKAY0.373
sum04_true-unreach-call_true-termination.c below 1 PASS0.327
sum_array_false-unreach-call.c below 1 OKAY0.66
sum_array_true-unreach-call.c below 1 FAIL0.734
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.337
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.428
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.355
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.342
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.331
trex01_false-unreach-call_true-termination.c below 3 OKAY0.456
trex01_true-unreach-call.c below 3 PASS0.822
trex02_false-unreach-call_true-termination.c below 3 OKAY0.396
trex02_true-unreach-call_true-termination.c below 3 PASS0.398
trex03_false-unreach-call_true-termination.c below 3 OKAY0.875
trex03_true-unreach-call.c below 3 PASS0.848
trex04_true-unreach-call_false-termination.c below 1 PASS0.384
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.335
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS24.934
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.365
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.352
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY17.286
vogal_false-unreach-call.c below 1 OKAY0.883
vogal_true-unreach-call.c below 1 FAIL0.896
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.308
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.324
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.316
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.326
ICRA Assertions (True) = 20/34
ICRA Assertions (False) = 30/32
ICRA Time = 843.918
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below TIMEOUT 300.033
Ackermann02_false-unreach-call_false-termination.c below TIMEOUT 300.033
Ackermann03_true-unreach-call.c below TIMEOUT 300.025
Ackermann04_true-unreach-call.c below TIMEOUT 300.021
Addition01_true-unreach-call_true-termination.c below 2 PASS0.578
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.582
Addition03_false-no-overflow.c below 2 PASS0.566
Addition03_true-unreach-call.c below 2 PASS0.567
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.45
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.425
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.444
Fibonacci01_true-unreach-call.c below EXCEPTION 0.984
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.989
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 1.032
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 0.983
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 0.992
gcd01_true-unreach-call_true-termination.c below 2 PASS0.567
gcd02_true-unreach-call.c below 2 FAIL1.366
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.479
McCarthy91_true-unreach-call.c below 7 FAIL1.432
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.672
Primes_true-unreach-call.c below 3 FAIL2.142
recHanoi01_true-unreach-call_true-termination.c below 9 FAIL6.042
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.375
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.39
ICRA Assertions (True) = 5/18
ICRA Assertions (False) = 4/7
ICRA Time = 1223.169
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.424
afterrec_2calls_true-unreach-call.c below 2 PASS0.373
afterrec_false-unreach-call.c below 2 OKAY0.356
afterrec_true-unreach-call.c below 2 PASS0.348
fibo_10_false-unreach-call.c below EXCEPTION 0.958
fibo_10_true-unreach-call.c below EXCEPTION 0.966
fibo_15_false-unreach-call.c below EXCEPTION 0.976
fibo_15_true-unreach-call.c below EXCEPTION 0.969
fibo_20_false-unreach-call.c below EXCEPTION 0.981
fibo_20_true-unreach-call.c below EXCEPTION 0.955
fibo_25_false-unreach-call.c below EXCEPTION 0.979
fibo_25_true-unreach-call.c below EXCEPTION 0.975
fibo_2calls_10_false-unreach-call.c below EXCEPTION 17.805
fibo_2calls_10_true-unreach-call.c below EXCEPTION 17.728
fibo_2calls_15_false-unreach-call.c below EXCEPTION 17.423
fibo_2calls_15_true-unreach-call.c below EXCEPTION 17.834
fibo_2calls_20_false-unreach-call.c below EXCEPTION 17.611
fibo_2calls_20_true-unreach-call.c below EXCEPTION 17.627
fibo_2calls_25_false-unreach-call.c below EXCEPTION 17.602
fibo_2calls_25_true-unreach-call.c below EXCEPTION 17.617
fibo_2calls_2_false-unreach-call.c below EXCEPTION 17.704
fibo_2calls_2_true-unreach-call.c below EXCEPTION 17.575
fibo_2calls_4_false-unreach-call.c below EXCEPTION 17.41
fibo_2calls_4_true-unreach-call.c below EXCEPTION 17.701
fibo_2calls_5_false-unreach-call.c below EXCEPTION 17.651
fibo_2calls_5_true-unreach-call.c below EXCEPTION 17.68
fibo_2calls_6_false-unreach-call.c below EXCEPTION 17.477
fibo_2calls_6_true-unreach-call.c below EXCEPTION 17.586
fibo_2calls_8_false-unreach-call.c below EXCEPTION 17.641
fibo_2calls_8_true-unreach-call.c below EXCEPTION 17.499
fibo_5_false-unreach-call.c below EXCEPTION 0.947
fibo_5_true-unreach-call.c below EXCEPTION 0.944
fibo_7_false-unreach-call.c below EXCEPTION 0.982
fibo_7_true-unreach-call.c below EXCEPTION 0.92
id2_b2_o3_true-unreach-call.c below 2 PASS0.942
id2_b3_o2_false-unreach-call.c below 2 OKAY1.04
id2_b3_o5_true-unreach-call.c below 2 PASS0.944
id2_b5_o10_true-unreach-call.c below 2 PASS0.979
id2_i5_o5_false-unreach-call.c below 2 OKAY0.44
id2_i5_o5_true-unreach-call.c below 2 PASS0.408
id_b2_o3_true-unreach-call.c below 2 PASS0.582
id_b3_o2_false-unreach-call.c below 2 OKAY0.597
id_b3_o5_true-unreach-call.c below 2 PASS0.595
id_b5_o10_true-unreach-call.c below 2 PASS0.582
id_i10_o10_false-unreach-call.c below 2 OKAY0.383
id_i10_o10_true-unreach-call.c below 2 PASS0.362
id_i15_o15_false-unreach-call.c below 2 OKAY0.383
id_i15_o15_true-unreach-call.c below 2 PASS0.362
id_i20_o20_false-unreach-call.c below 2 OKAY0.362
id_i20_o20_true-unreach-call.c below 2 PASS0.378
id_i25_o25_false-unreach-call.c below 2 OKAY0.375
id_i25_o25_true-unreach-call.c below 2 PASS0.383
id_i5_o5_false-unreach-call.c below 2 OKAY0.385
id_i5_o5_true-unreach-call.c below 2 PASS0.371
id_o1000_false-unreach-call.c below 2 OKAY0.388
id_o100_false-unreach-call.c below 2 OKAY0.377
id_o10_false-unreach-call.c below 2 OKAY0.402
id_o200_false-unreach-call.c below 2 OKAY0.399
id_o20_false-unreach-call.c below 2 OKAY0.394
id_o3_false-unreach-call.c below 2 OKAY0.384
sum_10x0_false-unreach-call.c below 2 OKAY0.395
sum_10x0_true-unreach-call.c below 2 PASS0.389
sum_15x0_false-unreach-call.c below 2 OKAY0.412
sum_15x0_true-unreach-call.c below 2 PASS0.389
sum_20x0_false-unreach-call.c below 2 OKAY0.399
sum_20x0_true-unreach-call.c below 2 PASS0.376
sum_25x0_false-unreach-call.c below 2 OKAY0.382
sum_25x0_true-unreach-call.c below 2 PASS0.388
sum_2x3_false-unreach-call.c below 2 OKAY0.395
sum_2x3_true-unreach-call.c below 2 PASS0.375
sum_non_eq_false-unreach-call.c below 2 OKAY0.444
sum_non_eq_true-unreach-call.c below 2 PASS0.407
sum_non_false-unreach-call.c below 2 OKAY0.397
sum_non_true-unreach-call.c below 2 PASS0.386
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 348.955
/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.387
rec-bhmr2007_true-unreach-call.c below 2 PASS0.401
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.771
rec-cggmp2005_true-unreach-call.c below 2 PASS0.344
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.357
rec-css2003_true-unreach-call.c below 2 PASS0.625
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.35
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.919
rec-gj2007b_true-unreach-call.c below 2 FAIL0.379
rec-gj2007_true-unreach-call.c below 2 FAIL0.367
rec-gr2006_true-unreach-call.c below 2 FAIL0.399
rec-gsv2008_true-unreach-call.c below 2 PASS0.342
rec-hhk2008_true-unreach-call.c below 2 PASS0.354
rec-jm2006_true-unreach-call.c below 2 PASS0.368
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.39
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.422
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.175
/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.327
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.346
rec-count_by_2_true-unreach-call.c below 2 PASS0.334
rec-count_by_k_true-unreach-call.c below 2 PASS0.369
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.389
rec-gauss_sum_true-unreach-call.c below 2 PASS0.355
rec-half_true-unreach-call.c below EXCEPTION 0.337
rec-nested_true-unreach-call.c below 3 PASS0.601
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.058
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.514
edit_distance_bottom_up.c below 3 TIMEOUT 300.008
edit_distance_top_down.c below 3 FAIL50.39
log_log_n_solution.c below 3 FAIL0.446
log_n_solution.c below 2 FAIL0.467
multivariate_1.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL26.566
n_cubed_solution.c below EXCEPTION 0.33
n_log_n_solution.c below TIMEOUT 300.037
n_squared_two_base_case_even.c below 2 PASS0.38
n_squared_two_base_case_odd.c below 2 PASS0.383
pascals_dynamic.c below 3 FAIL20.795
pascals_iterative.c below 1 FAIL5.623
pascals_recursive.c below TIMEOUT 300.005
squared_solution.c below TIMEOUT 300.134
two_n_even.c below 2 PASS0.366
two_n_odd.c below 2 PASS0.375
two_to_n_over_two_even.c below TIMEOUT 300.023
two_to_n_over_two_odd.c below TIMEOUT 300.022
two_to_n_squared.c below 8 TIMEOUT 300.006
two_to_two_to_n.c below 7 FAIL1.66
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 0/0
ICRA Time = 2508.536
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.318
exp_add_loop_rec.c below 1 FAIL0.352
exp_add_loop_variable.c below 1 PASS0.34
exp_with_linear_inner_loop.c below 1 FAIL0.42
linear_two_to_n.c below 8 FAIL1.526
loop_five_to_n.c below 1 FAIL0.346
non_loop_five_to_n.c below 8 FAIL10.153
power_log.c below 1 PASS0.406
power_log_modified.c below 1 PASS0.476
simple_exponential.c below 1 PASS0.342
simple_exponential_for.c below 1 PASS0.338
two_to_n_minus_n.c below 8 FAIL1.758
two_to_n_minus_n_loop.c below 8 FAIL2.88
ICRA Assertions (True) = 6/13
ICRA Assertions (False) = 0/0
ICRA Time = 19.655