[Version Information]
WALi-OpenNWA version: eeaa6a4c577535d1bcb47a13ddf1230e2f98e207 (2017-05-19 15:05:02 -0500) "Two small niceties in NewtonCompare.cpp"
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.356
kmp.c below 1 PASS1.321
qsort.c below 5 PASS3.419
speed_pldi09_fig1.c below 1 PASS0.375
speed_pldi09_fig4_2.c below 1 FAIL0.398
speed_pldi09_fig4_4.c below 1 PASS0.445
speed_pldi09_fig4_5.c below 1 PASS0.374
speed_pldi10_ex1.c below 1 PASS3.897
speed_pldi10_ex3.c below 1 PASS0.461
speed_pldi10_ex4.c below EXCEPTION 0.404
speed_popl10_fig2_1.c below 1 PASS0.387
speed_popl10_fig2_2.c below 1 FAIL0.369
speed_popl10_nested_multiple.c below 1 PASS0.429
speed_popl10_nested_single.c below 1 PASS0.398
speed_popl10_sequential_single.c below 1 PASS0.362
speed_popl10_simple_multiple.c below 1 PASS0.396
speed_popl10_simple_single_2.c below 1 PASS0.415
speed_popl10_simple_single.c below 1 PASS0.343
t07.c below 1 PASS0.376
t08.c below 1 PASS0.351
t09.c below 1 PASS0.357
t10.c below 1 PASS0.363
t11.c below 1 PASS0.388
t13.c below 1 FAIL0.393
t15.c below 1 PASS0.367
t16.c below 1 PASS0.36
t19.c below 1 PASS0.348
t20.c below 1 PASS0.342
t27.c below 1 PASS0.416
t28.c below 1 PASS0.382
t30.c below 1 FAIL0.353
t37.c below 2 PASS0.468
t39.c below 2 PASS0.501
t46.c below 1 PASS0.354
t47.c below 1 PASS0.37
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 21.038
/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.009
rec1-param_safe.c below 2 PASS0.35
rec1-param_unsafe.c below 2 OKAY0.346
rec1_safe.c below 2 PASS0.339
rec1_unsafe.c below 2 OKAY0.334
rec2-param_safe.c below 2 PASS0.352
rec2-param_unsafe.c below 2 OKAY0.356
rec2_safe.c below 2 PASS0.337
rec2_unsafe.c below 2 OKAY0.353
rec-test.c below 2 PASS0.361
sas03_bothbranches.c below 7 PASS1.292
sas03.c below 2 PASS0.793
simulated_lese_recursive.c below 2 PASS0.382
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 4/4
ICRA Time = 305.996
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.326
count_up_down_unsafe.c below 1 OKAY0.317
divide.c below 1 PASS0.318
factor_unsafe.c below 1 OKAY0.321
for_infinite_loop_1_safe.c below 1 PASS0.33
for_infinite_loop_2_safe.c below 1 PASS0.326
interproc.c below 1 PASS0.326
mult.c below 1 PASS0.325
pointer_arith.c below 1 PASS0.315
quotient.c below 3 PASS0.445
subtract.c below 1 PASS0.316
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.331
sum01_bug02_unsafe.c below 1 OKAY0.417
sum01_real_safe.c below 1 PASS0.331
sum01_safe.c below 1 PASS0.324
sum01_unsafe.c below 1 OKAY0.371
sum02_safe.c below 1 PASS0.327
sum03_safe.c below 1 PASS0.337
sum03_unsafe.c below 1 OKAY0.411
sum04_safe.c below 1 PASS0.322
sum04_unsafe.c below 1 OKAY0.357
terminator_02_safe.c below 1 PASS0.324
terminator_02_unsafe.c below 1 OKAY0.363
terminator_03_safe.c below 1 PASS0.326
terminator_03_unsafe.c below 1 OKAY0.314
token_ring01_safe.c below TIMEOUT 300.006
token_ring01_unsafe.c below TIMEOUT 300.008
toy_safe.c below EXCEPTION 158.945
trex01_safe.c below 1 PASS0.738
trex01_unsafe.c below 1 OKAY0.367
trex02_safe2.c below 3 PASS0.384
trex02_safe.c below 3 PASS0.393
trex02_unsafe.c below 3 OKAY0.389
trex03_safe.c below 1 PASS0.477
trex03_unsafe.c below 1 OKAY0.465
trex04_safe.c below 1 PASS0.352
while_infinite_loop_1_safe.c below 1 PASS0.322
while_infinite_loop_2_safe.c below 1 PASS0.324
while_infinite_loop_3_safe.c below 1 PASS0.312
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 772.002
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.441
blogger_simplified1.c below 3 PASS0.975
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.349
mult-proc-params.c below 3 PASS0.399
popall.c below 1 PASS0.412
simulated_scc.c below 1 PASS0.515
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.095
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.349
degree2_binomial.c below 1 PASS0.449
degree2_monomial.c below 1 PASS0.372
degree3_binomial.c below 1 PASS0.883
degree3_monomial.c below 1 PASS0.417
degree4_binomial.c below 1 PASS1.147
degree4_monomial.c below 1 PASS0.509
degree5_binomial.c below 1 PASS1.709
degree5_monomial.c below 1 PASS0.582
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 6.417
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.346
cubic_with_square_interproc.c below 2 PASS0.372
cubic_with_square_nonlinear.c below 1 PASS0.356
cubic_with_square_nonlinear_interproc.c below 2 PASS0.367
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.358
cubic_with_square_unsafe.c below 1 OKAY0.335
multi-input.c below 1 PASS0.41
multi-input_unsafe.c below 1 OKAY0.431
nondet_loop_bound.c below 1 PASS0.35
nondet_loop_bound_quartic.c below 1 PASS0.353
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.362
nondet_loop_bound_unsafe.c below 1 OKAY0.371
nonlinear_stratified.c below 1 FAIL0.347
nonlinear_stratified_unsafe.c below 1 OKAY0.358
quartic_with_cube.c below 1 PASS0.351
quartic_with_cube_nonlinear.c below 1 PASS0.376
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.366
quartic_with_cube_unsafe.c below 1 OKAY0.355
quintic_with_quartic.c below 1 PASS0.354
quintic_with_quartic_nonlinear.c below 1 PASS0.394
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.363
quintic_with_quartic_unsafe.c below 1 OKAY0.356
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 10/10
ICRA Time = 8.031
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.498
degree2_FD_AllAux_AllAssm.c below 1 PASS3.595
degree2_FD_AllAux_FewAssm.c below 1 PASS5.442
degree2_FD_FewAux_FewAssm.c below 1 PASS0.701
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.693
degree3.c below 1 PASS0.545
degree3_FD.c below 1 PASS0.688
degree4.c below 1 PASS0.382
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 12.544
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.396
loop_unsafe.c below 1 OKAY0.41
simulated_lese_parser.c below 1 PASS0.327
simulated_lese_sentinel.c below 1 PASS0.339
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.472
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.333
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.333
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.014
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.014
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.34
array_false-unreach-call2.c below 1 OKAY0.358
array_false-unreach-call3.c below 1 OKAY0.332
array_true-unreach-call1.c below 1 FAIL0.346
array_true-unreach-call2.c below 1 FAIL0.369
array_true-unreach-call3.c below 1 PASS0.337
array_true-unreach-call4.c below 1 FAIL0.333
const_false-unreach-call1.c below 1 OKAY0.313
const_true-unreach-call1.c below 1 PASS0.316
diamond_false-unreach-call1.c below 1 OKAY0.327
diamond_true-unreach-call1.c below 1 PASS0.328
diamond_true-unreach-call2.c below 1 PASS0.364
functions_false-unreach-call1.c below 3 OKAY0.366
functions_true-unreach-call1.c below 3 PASS0.355
multivar_false-unreach-call1.c below 1 OKAY0.309
multivar_true-unreach-call1.c below 1 PASS0.313
nested_false-unreach-call1.c below 1 OKAY0.332
nested_true-unreach-call1.c below 1 PASS0.337
overflow_true-unreach-call1.c below 1 PASS0.316
phases_false-unreach-call1.c below 1 OKAY0.332
phases_false-unreach-call2.c below 1 OKAY0.346
phases_true-unreach-call1.c below 1 PASS0.337
phases_true-unreach-call2.c below 1 PASS0.337
simple_false-unreach-call1.c below 1 OKAY0.324
simple_false-unreach-call2.c below 1 OKAY0.33
simple_false-unreach-call3.c below 1 OKAY0.318
simple_false-unreach-call4.c below 1 OKAY0.313
simple_true-unreach-call1.c below 1 PASS0.314
simple_true-unreach-call2.c below 1 PASS0.311
simple_true-unreach-call3.c below 1 PASS0.329
simple_true-unreach-call4.c below 1 PASS0.338
underapprox_false-unreach-call1.c below 1 OKAY0.322
underapprox_false-unreach-call2.c below 1 OKAY0.32
underapprox_true-unreach-call1.c below 1 FAIL0.353
underapprox_true-unreach-call2.c below 1 PASS0.323
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 11.638
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.842
apache-get-tag_true-unreach-call.c below 1 FAIL0.472
down_true-unreach-call.c below 1 PASS0.34
fragtest_simple_true-unreach-call.c below 1 PASS0.379
half_2_true-unreach-call.c below 1 PASS0.343
heapsort_true-unreach-call.c below 1 TIMEOUT300.15
id_build_true-unreach-call.c below 1 PASS0.334
id_trans_false-unreach-call.c below 1 OKAY0.345
large_const_true-unreach-call.c below 1 PASS0.418
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.364
nested6_true-unreach-call.c below 1 FAIL0.41
nested9_true-unreach-call.c below 1 PASS0.46
nest-if3_true-unreach-call.c below 1 PASS0.405
NetBSD_loop_true-unreach-call.c below 1 PASS0.335
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.377
seq_true-unreach-call.c below 1 PASS0.374
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.107
string_concat-noarr_true-unreach-call.c below 1 PASS0.344
up_true-unreach-call.c below 1 PASS0.322
ICRA Assertions (True) = 13/18
ICRA Assertions (False) = 1/1
ICRA Time = 607.121
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.33
bhmr2007_true-unreach-call.c below 1 PASS0.358
cggmp2005b_true-unreach-call.c below 1 PASS0.398
cggmp2005_true-unreach-call.c below 1 PASS0.33
cggmp2005_variant_true-unreach-call.c below 1 PASS0.333
css2003_true-unreach-call.c below 1 PASS0.481
ddlm2013_true-unreach-call.c below 1 PASS0.372
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.167
gj2007b_true-unreach-call.c below 1 FAIL0.356
gj2007_true-unreach-call.c below 1 PASS0.341
gr2006_true-unreach-call.c below 1 PASS0.343
gsv2008_true-unreach-call.c below 1 PASS0.314
hhk2008_true-unreach-call.c below 1 PASS0.332
jm2006_true-unreach-call.c below 1 PASS0.353
jm2006_variant_true-unreach-call.c below 1 PASS0.364
mcmillan2006_true-unreach-call.c below 1 FAIL0.367
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.539
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.325
count_by_1_variant_true-unreach-call.c below 1 PASS0.321
count_by_2_true-unreach-call.c below 1 PASS0.317
count_by_k_true-unreach-call.c below 1 PASS0.327
count_by_nondet_true-unreach-call.c below 1 FAIL0.343
gauss_sum_true-unreach-call.c below 1 PASS0.328
half_true-unreach-call.c below EXCEPTION 0.33
nested_true-unreach-call.c below 1 PASS0.386
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.677
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.419
array_true-unreach-call.c below 1 FAIL0.427
bubble_sort_false-unreach-call.c below 4 OKAY139.354
bubble_sort_true-unreach-call.c below 1 PASS3.724
compact_false-unreach-call.c below 1 OKAY0.36
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.318
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.33
eureka_01_false-unreach-call.c below 1 OKAY2.189
eureka_01_true-unreach-call.c below 1 FAIL1.935
eureka_05_true-unreach-call.c below 1 FAIL1.101
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.336
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.319
heavy_false-unreach-call.c below 1 OKAY0.527
heavy_true-unreach-call.c below 1 PASS0.505
insertion_sort_false-unreach-call.c below 1 OKAY2.108
insertion_sort_true-unreach-call.c below 1 FAIL0.74
invert_string_false-unreach-call.c below 1 OKAY0.501
invert_string_true-unreach-call.c below 1 FAIL0.483
linear_sea.ch_true-unreach-call.c below 1 FAIL0.38
linear_search_false-unreach-call.c below 1 UNSOUND0.392
lu.cmp_true-unreach-call.c below TIMEOUT 300.252
ludcmp_false-unreach-call.c below TIMEOUT 300.255
matrix_false-unreach-call_true-termination.c below 1 OKAY0.989
matrix_true-unreach-call_true-termination.c below 1 FAIL0.519
n.c11_true-unreach-call.c below 3 FAIL0.476
n.c24_false-unreach-call.c below 3 OKAY23.429
n.c40_true-unreach-call.c below 1 FAIL0.372
nec11_false-unreach-call.c below 1 OKAY0.375
nec20_false-unreach-call.c below 1 OKAY0.348
nec40_true-unreach-call.c below 1 FAIL0.37
string_false-unreach-call.c below 1 OKAY0.643
string_true-unreach-call.c below 1 FAIL0.656
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.349
sum01_false-unreach-call_true-termination.c below 1 OKAY0.359
sum01_true-unreach-call_true-termination.c below 1 PASS0.331
sum03_false-unreach-call_true-termination.c below 1 OKAY0.452
sum03_true-unreach-call_false-termination.c below 1 PASS0.351
sum04_false-unreach-call_true-termination.c below 1 OKAY0.364
sum04_true-unreach-call_true-termination.c below 1 PASS0.313
sum_array_false-unreach-call.c below 1 OKAY0.636
sum_array_true-unreach-call.c below 1 FAIL0.704
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.32
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.404
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.341
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.326
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.32
trex01_false-unreach-call_true-termination.c below 3 OKAY0.425
trex01_true-unreach-call.c below 3 PASS0.764
trex02_false-unreach-call_true-termination.c below 3 OKAY0.389
trex02_true-unreach-call_true-termination.c below 3 PASS0.382
trex03_false-unreach-call_true-termination.c below 3 OKAY0.827
trex03_true-unreach-call.c below 3 PASS0.868
trex04_true-unreach-call_false-termination.c below 1 PASS0.372
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.328
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS24.257
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.359
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.348
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY17.166
vogal_false-unreach-call.c below 1 OKAY0.81
vogal_true-unreach-call.c below 1 FAIL0.827
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.305
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.306
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.317
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.321
ICRA Assertions (True) = 20/34
ICRA Assertions (False) = 30/32
ICRA Time = 840.757
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below TIMEOUT 300.021
Ackermann02_false-unreach-call_false-termination.c below TIMEOUT 300.019
Ackermann03_true-unreach-call.c below TIMEOUT 300.02
Ackermann04_true-unreach-call.c below TIMEOUT 300.019
Addition01_true-unreach-call_true-termination.c below 2 PASS0.552
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.556
Addition03_false-no-overflow.c below 2 PASS0.596
Addition03_true-unreach-call.c below 2 PASS0.569
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.459
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.427
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.414
Fibonacci01_true-unreach-call.c below EXCEPTION 0.937
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.934
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 0.94
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 0.949
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 0.903
gcd01_true-unreach-call_true-termination.c below 2 PASS0.545
gcd02_true-unreach-call.c below 2 FAIL1.315
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.456
McCarthy91_true-unreach-call.c below 7 FAIL1.399
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.657
Primes_true-unreach-call.c below 3 FAIL1.993
recHanoi01_true-unreach-call_true-termination.c below 9 FAIL5.614
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.36
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.364
ICRA Assertions (True) = 5/18
ICRA Assertions (False) = 4/7
ICRA Time = 1222.018
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.41
afterrec_2calls_true-unreach-call.c below 2 PASS0.38
afterrec_false-unreach-call.c below 2 OKAY0.35
afterrec_true-unreach-call.c below 2 PASS0.342
fibo_10_false-unreach-call.c below EXCEPTION 0.941
fibo_10_true-unreach-call.c below EXCEPTION 0.935
fibo_15_false-unreach-call.c below EXCEPTION 0.93
fibo_15_true-unreach-call.c below EXCEPTION 0.934
fibo_20_false-unreach-call.c below EXCEPTION 0.936
fibo_20_true-unreach-call.c below EXCEPTION 0.902
fibo_25_false-unreach-call.c below EXCEPTION 0.933
fibo_25_true-unreach-call.c below EXCEPTION 0.96
fibo_2calls_10_false-unreach-call.c below EXCEPTION 16.926
fibo_2calls_10_true-unreach-call.c below EXCEPTION 17.146
fibo_2calls_15_false-unreach-call.c below EXCEPTION 17.176
fibo_2calls_15_true-unreach-call.c below EXCEPTION 17.038
fibo_2calls_20_false-unreach-call.c below EXCEPTION 17.102
fibo_2calls_20_true-unreach-call.c below EXCEPTION 17.032
fibo_2calls_25_false-unreach-call.c below EXCEPTION 16.927
fibo_2calls_25_true-unreach-call.c below EXCEPTION 17.104
fibo_2calls_2_false-unreach-call.c below EXCEPTION 17.164
fibo_2calls_2_true-unreach-call.c below EXCEPTION 17.185
fibo_2calls_4_false-unreach-call.c below EXCEPTION 17.076
fibo_2calls_4_true-unreach-call.c below EXCEPTION 17.319
fibo_2calls_5_false-unreach-call.c below EXCEPTION 17.233
fibo_2calls_5_true-unreach-call.c below EXCEPTION 17.014
fibo_2calls_6_false-unreach-call.c below EXCEPTION 17.368
fibo_2calls_6_true-unreach-call.c below EXCEPTION 17.045
fibo_2calls_8_false-unreach-call.c below EXCEPTION 17.366
fibo_2calls_8_true-unreach-call.c below EXCEPTION 17.127
fibo_5_false-unreach-call.c below EXCEPTION 0.896
fibo_5_true-unreach-call.c below EXCEPTION 0.91
fibo_7_false-unreach-call.c below EXCEPTION 0.926
fibo_7_true-unreach-call.c below EXCEPTION 0.936
id2_b2_o3_true-unreach-call.c below 2 PASS0.935
id2_b3_o2_false-unreach-call.c below 2 OKAY0.96
id2_b3_o5_true-unreach-call.c below 2 PASS0.954
id2_b5_o10_true-unreach-call.c below 2 PASS0.936
id2_i5_o5_false-unreach-call.c below 2 OKAY0.418
id2_i5_o5_true-unreach-call.c below 2 PASS0.419
id_b2_o3_true-unreach-call.c below 2 PASS0.567
id_b3_o2_false-unreach-call.c below 2 OKAY0.587
id_b3_o5_true-unreach-call.c below 2 PASS0.577
id_b5_o10_true-unreach-call.c below 2 PASS0.588
id_i10_o10_false-unreach-call.c below 2 OKAY0.385
id_i10_o10_true-unreach-call.c below 2 PASS0.378
id_i15_o15_false-unreach-call.c below 2 OKAY0.377
id_i15_o15_true-unreach-call.c below 2 PASS0.382
id_i20_o20_false-unreach-call.c below 2 OKAY0.372
id_i20_o20_true-unreach-call.c below 2 PASS0.385
id_i25_o25_false-unreach-call.c below 2 OKAY0.369
id_i25_o25_true-unreach-call.c below 2 PASS0.367
id_i5_o5_false-unreach-call.c below 2 OKAY0.38
id_i5_o5_true-unreach-call.c below 2 PASS0.375
id_o1000_false-unreach-call.c below 2 OKAY0.377
id_o100_false-unreach-call.c below 2 OKAY0.368
id_o10_false-unreach-call.c below 2 OKAY0.378
id_o200_false-unreach-call.c below 2 OKAY0.382
id_o20_false-unreach-call.c below 2 OKAY0.378
id_o3_false-unreach-call.c below 2 OKAY0.38
sum_10x0_false-unreach-call.c below 2 OKAY0.402
sum_10x0_true-unreach-call.c below 2 PASS0.376
sum_15x0_false-unreach-call.c below 2 OKAY0.392
sum_15x0_true-unreach-call.c below 2 PASS0.379
sum_20x0_false-unreach-call.c below 2 OKAY0.407
sum_20x0_true-unreach-call.c below 2 PASS0.384
sum_25x0_false-unreach-call.c below 2 OKAY0.404
sum_25x0_true-unreach-call.c below 2 PASS0.393
sum_2x3_false-unreach-call.c below 2 OKAY0.397
sum_2x3_true-unreach-call.c below 2 PASS0.376
sum_non_eq_false-unreach-call.c below 2 OKAY0.421
sum_non_eq_true-unreach-call.c below 2 PASS0.399
sum_non_false-unreach-call.c below 2 OKAY0.398
sum_non_true-unreach-call.c below 2 PASS0.373
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 339.444
/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.395
rec-bhmr2007_true-unreach-call.c below 2 PASS0.404
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.729
rec-cggmp2005_true-unreach-call.c below 2 PASS0.341
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.345
rec-css2003_true-unreach-call.c below 2 PASS0.619
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.343
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.842
rec-gj2007b_true-unreach-call.c below 2 FAIL0.389
rec-gj2007_true-unreach-call.c below 2 FAIL0.398
rec-gr2006_true-unreach-call.c below 2 FAIL0.393
rec-gsv2008_true-unreach-call.c below 2 PASS0.351
rec-hhk2008_true-unreach-call.c below 2 PASS0.335
rec-jm2006_true-unreach-call.c below 2 PASS0.378
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.388
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.428
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.078
/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.334
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.345
rec-count_by_2_true-unreach-call.c below 2 PASS0.339
rec-count_by_k_true-unreach-call.c below 2 PASS0.357
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.372
rec-gauss_sum_true-unreach-call.c below 2 PASS0.358
rec-half_true-unreach-call.c below EXCEPTION 0.331
rec-nested_true-unreach-call.c below 3 PASS0.59
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.026
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.528
edit_distance_bottom_up.c below 3 FAIL295.578
edit_distance_top_down.c below 3 FAIL49.765
log_log_n_solution.c below 3 FAIL0.431
log_n_solution.c below 2 FAIL0.441
multivariate_1.c below TIMEOUT 300.007
multivariate_higher_order.c below 7 FAIL25.532
n_cubed_solution.c below EXCEPTION 0.33
n_log_n_solution.c below TIMEOUT 300.038
n_squared_two_base_case_even.c below 2 PASS0.426
n_squared_two_base_case_odd.c below 2 PASS0.578
pascals_dynamic.c below 3 FAIL21.098
pascals_iterative.c below 1 FAIL5.334
pascals_recursive.c below TIMEOUT 300.005
squared_solution.c below TIMEOUT 300.138
two_n_even.c below 2 PASS0.389
two_n_odd.c below 2 PASS0.388
two_to_n_over_two_even.c below TIMEOUT 300.032
two_to_n_over_two_odd.c below TIMEOUT 300.021
two_to_n_squared.c below 8 TIMEOUT 300.005
two_to_two_to_n.c below 7 FAIL1.617
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 0/0
ICRA Time = 2502.681
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.323
exp_add_loop_rec.c below 1 FAIL0.453
exp_add_loop_variable.c below 1 PASS0.41
exp_with_linear_inner_loop.c below 1 FAIL0.444
linear_two_to_n.c below 8 FAIL1.528
loop_five_to_n.c below 1 FAIL0.357
non_loop_five_to_n.c below 8 FAIL10.064
power_log.c below 1 PASS0.413
power_log_modified.c below 1 PASS0.476
simple_exponential.c below 1 PASS0.325
simple_exponential_for.c below 1 PASS0.344
two_to_n_minus_n.c below 8 FAIL1.787
two_to_n_minus_n_loop.c below 8 FAIL2.689
ICRA Assertions (True) = 6/13
ICRA Assertions (False) = 0/0
ICRA Time = 19.613