[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.356
kmp.c below 1 PASS1.29
qsort.c below 5 PASS3.421
speed_pldi09_fig1.c below 1 PASS0.366
speed_pldi09_fig4_2.c below 1 FAIL0.399
speed_pldi09_fig4_4.c below 1 PASS0.453
speed_pldi09_fig4_5.c below 1 PASS0.367
speed_pldi10_ex1.c below 1 PASS3.799
speed_pldi10_ex3.c below 1 PASS0.455
speed_pldi10_ex4.c below EXCEPTION 0.396
speed_popl10_fig2_1.c below 1 PASS0.388
speed_popl10_fig2_2.c below 1 FAIL0.353
speed_popl10_nested_multiple.c below 1 PASS0.445
speed_popl10_nested_single.c below 1 PASS0.388
speed_popl10_sequential_single.c below 1 PASS0.361
speed_popl10_simple_multiple.c below 1 PASS0.4
speed_popl10_simple_single_2.c below 1 PASS0.399
speed_popl10_simple_single.c below 1 PASS0.335
t07.c below 1 PASS0.383
t08.c below 1 PASS0.363
t09.c below 1 PASS0.355
t10.c below 1 PASS0.349
t11.c below 1 PASS0.38
t13.c below 1 FAIL0.386
t15.c below 1 PASS0.361
t16.c below 1 PASS0.363
t19.c below 1 PASS0.353
t20.c below 1 PASS0.339
t27.c below 1 PASS0.424
t28.c below 1 PASS0.377
t30.c below 1 FAIL0.357
t37.c below 2 PASS0.469
t39.c below 2 PASS0.491
t46.c below 1 PASS0.352
t47.c below 1 PASS0.363
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 20.836
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.379
qsort_full.c below 5 TIMEOUT 300.009
rec1-param_safe.c below 2 PASS0.365
rec1-param_unsafe.c below 2 OKAY0.354
rec1_safe.c below 2 PASS0.32
rec1_unsafe.c below 2 OKAY0.33
rec2-param_safe.c below 2 PASS0.343
rec2-param_unsafe.c below 2 OKAY0.344
rec2_safe.c below 2 PASS0.33
rec2_unsafe.c below 2 OKAY0.328
rec-test.c below 2 PASS0.338
sas03_bothbranches.c below 7 PASS1.26
sas03.c below 2 PASS0.833
simulated_lese_recursive.c below 2 PASS0.405
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 4/4
ICRA Time = 305.938
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.314
count_up_down_unsafe.c below 1 OKAY0.324
divide.c below 1 PASS0.318
factor_unsafe.c below 1 OKAY0.321
for_infinite_loop_1_safe.c below 1 PASS0.353
for_infinite_loop_2_safe.c below 1 PASS0.308
interproc.c below 1 PASS0.315
mult.c below 1 PASS0.33
pointer_arith.c below 1 PASS0.302
quotient.c below 3 PASS0.434
subtract.c below 1 PASS0.317
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.333
sum01_bug02_unsafe.c below 1 OKAY0.374
sum01_real_safe.c below 1 PASS0.32
sum01_safe.c below 1 PASS0.325
sum01_unsafe.c below 1 OKAY0.365
sum02_safe.c below 1 PASS0.337
sum03_safe.c below 1 PASS0.349
sum03_unsafe.c below 1 OKAY0.403
sum04_safe.c below 1 PASS0.318
sum04_unsafe.c below 1 OKAY0.354
terminator_02_safe.c below 1 PASS0.331
terminator_02_unsafe.c below 1 OKAY0.34
terminator_03_safe.c below 1 PASS0.323
terminator_03_unsafe.c below 1 OKAY0.334
token_ring01_safe.c below TIMEOUT 300.007
token_ring01_unsafe.c below TIMEOUT 300.006
toy_safe.c below EXCEPTION 166.509
trex01_safe.c below 1 PASS0.725
trex01_unsafe.c below 1 OKAY0.391
trex02_safe2.c below 3 PASS0.383
trex02_safe.c below 3 PASS0.385
trex02_unsafe.c below 3 OKAY0.391
trex03_safe.c below 1 PASS0.456
trex03_unsafe.c below 1 OKAY0.468
trex04_safe.c below 1 PASS0.343
while_infinite_loop_1_safe.c below 1 PASS0.306
while_infinite_loop_2_safe.c below 1 PASS0.32
while_infinite_loop_3_safe.c below 1 PASS0.312
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 779.444
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.447
blogger_simplified1.c below 3 PASS0.984
divided_difference2.c below TIMEOUT 300.006
mult-proc.c below 3 PASS0.358
mult-proc-params.c below 3 PASS0.389
popall.c below 1 PASS0.413
simulated_scc.c below 1 PASS0.52
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.117
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.344
degree2_binomial.c below 1 PASS0.477
degree2_monomial.c below 1 PASS0.372
degree3_binomial.c below 1 PASS0.876
degree3_monomial.c below 1 PASS0.42
degree4_binomial.c below 1 PASS1.165
degree4_monomial.c below 1 PASS0.487
degree5_binomial.c below 1 PASS1.725
degree5_monomial.c below 1 PASS0.553
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 6.419
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.34
cubic_with_square_interproc.c below 2 PASS0.392
cubic_with_square_nonlinear.c below 1 PASS0.343
cubic_with_square_nonlinear_interproc.c below 2 PASS0.377
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.363
cubic_with_square_unsafe.c below 1 OKAY0.351
multi-input.c below 1 PASS0.409
multi-input_unsafe.c below 1 OKAY0.446
nondet_loop_bound.c below 1 PASS0.363
nondet_loop_bound_quartic.c below 1 PASS0.367
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.371
nondet_loop_bound_unsafe.c below 1 OKAY0.381
nonlinear_stratified.c below 1 FAIL0.349
nonlinear_stratified_unsafe.c below 1 OKAY0.368
quartic_with_cube.c below 1 PASS0.355
quartic_with_cube_nonlinear.c below 1 PASS0.364
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.368
quartic_with_cube_unsafe.c below 1 OKAY0.359
quintic_with_quartic.c below 1 PASS0.36
quintic_with_quartic_nonlinear.c below 1 PASS0.395
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.379
quintic_with_quartic_unsafe.c below 1 OKAY0.367
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 10/10
ICRA Time = 8.167
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.516
degree2_FD_AllAux_AllAssm.c below 1 PASS3.684
degree2_FD_AllAux_FewAssm.c below 1 PASS5.428
degree2_FD_FewAux_FewAssm.c below 1 PASS0.705
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.7
degree3.c below 1 PASS0.569
degree3_FD.c below 1 PASS0.728
degree4.c below 1 PASS0.403
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 12.733
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.383
loop_unsafe.c below 1 OKAY0.41
simulated_lese_parser.c below 1 PASS0.313
simulated_lese_sentinel.c below 1 PASS0.342
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.448
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.338
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.338
/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.338
array_false-unreach-call2.c below 1 OKAY0.375
array_false-unreach-call3.c below 1 OKAY0.339
array_true-unreach-call1.c below 1 FAIL0.347
array_true-unreach-call2.c below 1 FAIL0.371
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.32
const_true-unreach-call1.c below 1 PASS0.321
diamond_false-unreach-call1.c below 1 OKAY0.333
diamond_true-unreach-call1.c below 1 PASS0.328
diamond_true-unreach-call2.c below 1 PASS0.377
functions_false-unreach-call1.c below 3 OKAY0.368
functions_true-unreach-call1.c below 3 PASS0.349
multivar_false-unreach-call1.c below 1 OKAY0.318
multivar_true-unreach-call1.c below 1 PASS0.322
nested_false-unreach-call1.c below 1 OKAY0.339
nested_true-unreach-call1.c below 1 PASS0.334
overflow_true-unreach-call1.c below 1 PASS0.354
phases_false-unreach-call1.c below 1 OKAY0.338
phases_false-unreach-call2.c below 1 OKAY0.342
phases_true-unreach-call1.c below 1 PASS0.324
phases_true-unreach-call2.c below 1 PASS0.334
simple_false-unreach-call1.c below 1 OKAY0.318
simple_false-unreach-call2.c below 1 OKAY0.311
simple_false-unreach-call3.c below 1 OKAY0.317
simple_false-unreach-call4.c below 1 OKAY0.327
simple_true-unreach-call1.c below 1 PASS0.334
simple_true-unreach-call2.c below 1 PASS0.32
simple_true-unreach-call3.c below 1 PASS0.313
simple_true-unreach-call4.c below 1 PASS0.311
underapprox_false-unreach-call1.c below 1 OKAY0.334
underapprox_false-unreach-call2.c below 1 OKAY0.328
underapprox_true-unreach-call1.c below 1 FAIL0.329
underapprox_true-unreach-call2.c below 1 PASS0.321
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 11.701
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.837
apache-get-tag_true-unreach-call.c below 1 FAIL0.477
down_true-unreach-call.c below 1 PASS0.343
fragtest_simple_true-unreach-call.c below 1 PASS0.369
half_2_true-unreach-call.c below 1 PASS0.353
heapsort_true-unreach-call.c below 1 TIMEOUT300.141
id_build_true-unreach-call.c below 1 PASS0.338
id_trans_false-unreach-call.c below 1 OKAY0.363
large_const_true-unreach-call.c below 1 PASS0.414
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.374
nested6_true-unreach-call.c below 1 FAIL0.427
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.339
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.397
seq_true-unreach-call.c below 1 PASS0.373
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.11
string_concat-noarr_true-unreach-call.c below 1 PASS0.352
up_true-unreach-call.c below 1 PASS0.335
ICRA Assertions (True) = 13/18
ICRA Assertions (False) = 1/1
ICRA Time = 607.205
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.338
bhmr2007_true-unreach-call.c below 1 PASS0.356
cggmp2005b_true-unreach-call.c below 1 PASS0.398
cggmp2005_true-unreach-call.c below 1 PASS0.334
cggmp2005_variant_true-unreach-call.c below 1 PASS0.329
css2003_true-unreach-call.c below 1 PASS0.477
ddlm2013_true-unreach-call.c below 1 PASS0.387
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.179
gj2007b_true-unreach-call.c below 1 FAIL0.35
gj2007_true-unreach-call.c below 1 PASS0.339
gr2006_true-unreach-call.c below 1 PASS0.351
gsv2008_true-unreach-call.c below 1 PASS0.328
hhk2008_true-unreach-call.c below 1 PASS0.338
jm2006_true-unreach-call.c below 1 PASS0.351
jm2006_variant_true-unreach-call.c below 1 PASS0.381
mcmillan2006_true-unreach-call.c below 1 FAIL0.375
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.611
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.316
count_by_1_variant_true-unreach-call.c below 1 PASS0.341
count_by_2_true-unreach-call.c below 1 PASS0.313
count_by_k_true-unreach-call.c below 1 PASS0.336
count_by_nondet_true-unreach-call.c below 1 FAIL0.345
gauss_sum_true-unreach-call.c below 1 PASS0.345
half_true-unreach-call.c below EXCEPTION 0.33
nested_true-unreach-call.c below 1 PASS0.381
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.707
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.43
array_true-unreach-call.c below 1 FAIL0.423
bubble_sort_false-unreach-call.c below 4 OKAY141.423
bubble_sort_true-unreach-call.c below 1 PASS3.825
compact_false-unreach-call.c below 1 OKAY0.369
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.333
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.329
eureka_01_false-unreach-call.c below 1 OKAY2.208
eureka_01_true-unreach-call.c below 1 FAIL1.922
eureka_05_true-unreach-call.c below 1 FAIL1.052
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.331
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.313
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.317
heavy_false-unreach-call.c below 1 OKAY0.544
heavy_true-unreach-call.c below 1 PASS0.499
insertion_sort_false-unreach-call.c below 1 OKAY2.194
insertion_sort_true-unreach-call.c below 1 FAIL0.747
invert_string_false-unreach-call.c below 1 OKAY0.5
invert_string_true-unreach-call.c below 1 FAIL0.494
linear_sea.ch_true-unreach-call.c below 1 FAIL0.378
linear_search_false-unreach-call.c below 1 UNSOUND0.401
lu.cmp_true-unreach-call.c below TIMEOUT 300.274
ludcmp_false-unreach-call.c below TIMEOUT 300.242
matrix_false-unreach-call_true-termination.c below 1 OKAY0.983
matrix_true-unreach-call_true-termination.c below 1 FAIL0.508
n.c11_true-unreach-call.c below 3 FAIL0.471
n.c24_false-unreach-call.c below 3 OKAY23.43
n.c40_true-unreach-call.c below 1 FAIL0.372
nec11_false-unreach-call.c below 1 OKAY0.378
nec20_false-unreach-call.c below 1 OKAY0.367
nec40_true-unreach-call.c below 1 FAIL0.38
string_false-unreach-call.c below 1 OKAY0.674
string_true-unreach-call.c below 1 FAIL0.632
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.378
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.34
sum01_false-unreach-call_true-termination.c below 1 OKAY0.359
sum01_true-unreach-call_true-termination.c below 1 PASS0.338
sum03_false-unreach-call_true-termination.c below 1 OKAY0.503
sum03_true-unreach-call_false-termination.c below 1 PASS0.352
sum04_false-unreach-call_true-termination.c below 1 OKAY0.357
sum04_true-unreach-call_true-termination.c below 1 PASS0.331
sum_array_false-unreach-call.c below 1 OKAY0.661
sum_array_true-unreach-call.c below 1 FAIL0.679
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.319
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.425
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.34
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.332
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.798
trex02_false-unreach-call_true-termination.c below 3 OKAY0.408
trex02_true-unreach-call_true-termination.c below 3 PASS0.392
trex03_false-unreach-call_true-termination.c below 3 OKAY0.883
trex03_true-unreach-call.c below 3 PASS0.837
trex04_true-unreach-call_false-termination.c below 1 PASS0.391
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.349
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS24.527
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.347
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.349
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY17.053
vogal_false-unreach-call.c below 1 OKAY0.832
vogal_true-unreach-call.c below 1 FAIL0.843
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.297
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.31
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.31
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 = 843.491
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below TIMEOUT 300.031
Ackermann02_false-unreach-call_false-termination.c below TIMEOUT 300.033
Ackermann03_true-unreach-call.c below TIMEOUT 300.022
Ackermann04_true-unreach-call.c below TIMEOUT 300.022
Addition01_true-unreach-call_true-termination.c below 2 PASS0.59
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.586
Addition03_false-no-overflow.c below 2 PASS0.566
Addition03_true-unreach-call.c below 2 PASS0.586
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.452
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.441
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.415
Fibonacci01_true-unreach-call.c below EXCEPTION 0.948
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.94
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 0.958
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 0.984
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 0.955
gcd01_true-unreach-call_true-termination.c below 2 PASS0.574
gcd02_true-unreach-call.c below 2 FAIL1.36
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.445
McCarthy91_true-unreach-call.c below 7 FAIL1.401
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.689
Primes_true-unreach-call.c below 3 FAIL2.111
recHanoi01_true-unreach-call_true-termination.c below 9 FAIL5.767
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.371
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.388
ICRA Assertions (True) = 5/18
ICRA Assertions (False) = 4/7
ICRA Time = 1222.635
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.417
afterrec_2calls_true-unreach-call.c below 2 PASS0.381
afterrec_false-unreach-call.c below 2 OKAY0.356
afterrec_true-unreach-call.c below 2 PASS0.343
fibo_10_false-unreach-call.c below EXCEPTION 0.952
fibo_10_true-unreach-call.c below EXCEPTION 0.991
fibo_15_false-unreach-call.c below EXCEPTION 0.979
fibo_15_true-unreach-call.c below EXCEPTION 0.963
fibo_20_false-unreach-call.c below EXCEPTION 0.992
fibo_20_true-unreach-call.c below EXCEPTION 0.951
fibo_25_false-unreach-call.c below EXCEPTION 0.943
fibo_25_true-unreach-call.c below EXCEPTION 0.958
fibo_2calls_10_false-unreach-call.c below EXCEPTION 16.952
fibo_2calls_10_true-unreach-call.c below EXCEPTION 17.207
fibo_2calls_15_false-unreach-call.c below EXCEPTION 17.216
fibo_2calls_15_true-unreach-call.c below EXCEPTION 17.326
fibo_2calls_20_false-unreach-call.c below EXCEPTION 17.172
fibo_2calls_20_true-unreach-call.c below EXCEPTION 17.247
fibo_2calls_25_false-unreach-call.c below EXCEPTION 17.287
fibo_2calls_25_true-unreach-call.c below EXCEPTION 17.35
fibo_2calls_2_false-unreach-call.c below EXCEPTION 17.183
fibo_2calls_2_true-unreach-call.c below EXCEPTION 17.458
fibo_2calls_4_false-unreach-call.c below EXCEPTION 18.05
fibo_2calls_4_true-unreach-call.c below EXCEPTION 18.222
fibo_2calls_5_false-unreach-call.c below EXCEPTION 17.528
fibo_2calls_5_true-unreach-call.c below EXCEPTION 17.563
fibo_2calls_6_false-unreach-call.c below EXCEPTION 17.587
fibo_2calls_6_true-unreach-call.c below EXCEPTION 17.566
fibo_2calls_8_false-unreach-call.c below EXCEPTION 17.409
fibo_2calls_8_true-unreach-call.c below EXCEPTION 17.626
fibo_5_false-unreach-call.c below EXCEPTION 0.96
fibo_5_true-unreach-call.c below EXCEPTION 0.961
fibo_7_false-unreach-call.c below EXCEPTION 0.996
fibo_7_true-unreach-call.c below EXCEPTION 0.94
id2_b2_o3_true-unreach-call.c below 2 PASS0.94
id2_b3_o2_false-unreach-call.c below 2 OKAY1.025
id2_b3_o5_true-unreach-call.c below 2 PASS0.995
id2_b5_o10_true-unreach-call.c below 2 PASS1.013
id2_i5_o5_false-unreach-call.c below 2 OKAY0.45
id2_i5_o5_true-unreach-call.c below 2 PASS0.426
id_b2_o3_true-unreach-call.c below 2 PASS0.621
id_b3_o2_false-unreach-call.c below 2 OKAY0.601
id_b3_o5_true-unreach-call.c below 2 PASS0.596
id_b5_o10_true-unreach-call.c below 2 PASS0.603
id_i10_o10_false-unreach-call.c below 2 OKAY0.427
id_i10_o10_true-unreach-call.c below 2 PASS0.393
id_i15_o15_false-unreach-call.c below 2 OKAY0.393
id_i15_o15_true-unreach-call.c below 2 PASS0.386
id_i20_o20_false-unreach-call.c below 2 OKAY0.37
id_i20_o20_true-unreach-call.c below 2 PASS0.377
id_i25_o25_false-unreach-call.c below 2 OKAY0.389
id_i25_o25_true-unreach-call.c below 2 PASS0.378
id_i5_o5_false-unreach-call.c below 2 OKAY0.389
id_i5_o5_true-unreach-call.c below 2 PASS0.377
id_o1000_false-unreach-call.c below 2 OKAY0.378
id_o100_false-unreach-call.c below 2 OKAY0.405
id_o10_false-unreach-call.c below 2 OKAY0.374
id_o200_false-unreach-call.c below 2 OKAY0.391
id_o20_false-unreach-call.c below 2 OKAY0.394
id_o3_false-unreach-call.c below 2 OKAY0.385
sum_10x0_false-unreach-call.c below 2 OKAY0.401
sum_10x0_true-unreach-call.c below 2 PASS0.387
sum_15x0_false-unreach-call.c below 2 OKAY0.415
sum_15x0_true-unreach-call.c below 2 PASS0.392
sum_20x0_false-unreach-call.c below 2 OKAY0.411
sum_20x0_true-unreach-call.c below 2 PASS0.38
sum_25x0_false-unreach-call.c below 2 OKAY0.395
sum_25x0_true-unreach-call.c below 2 PASS0.379
sum_2x3_false-unreach-call.c below 2 OKAY0.407
sum_2x3_true-unreach-call.c below 2 PASS0.397
sum_non_eq_false-unreach-call.c below 2 OKAY0.45
sum_non_eq_true-unreach-call.c below 2 PASS0.425
sum_non_false-unreach-call.c below 2 OKAY0.416
sum_non_true-unreach-call.c below 2 PASS0.386
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 346.149
/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.377
rec-bhmr2007_true-unreach-call.c below 2 PASS0.42
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.793
rec-cggmp2005_true-unreach-call.c below 2 PASS0.331
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.353
rec-css2003_true-unreach-call.c below 2 PASS0.619
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.346
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.903
rec-gj2007b_true-unreach-call.c below 2 FAIL0.392
rec-gj2007_true-unreach-call.c below 2 FAIL0.381
rec-gr2006_true-unreach-call.c below 2 FAIL0.41
rec-gsv2008_true-unreach-call.c below 2 PASS0.341
rec-hhk2008_true-unreach-call.c below 2 PASS0.344
rec-jm2006_true-unreach-call.c below 2 PASS0.381
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.397
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.42
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.208
/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.329
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.345
rec-count_by_2_true-unreach-call.c below 2 PASS0.347
rec-count_by_k_true-unreach-call.c below 2 PASS0.368
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.396
rec-gauss_sum_true-unreach-call.c below 2 PASS0.368
rec-half_true-unreach-call.c below EXCEPTION 0.342
rec-nested_true-unreach-call.c below 3 PASS0.6
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.095
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.536
edit_distance_bottom_up.c below 3 TIMEOUT 300.01
edit_distance_top_down.c below 3 FAIL51.673
log_log_n_solution.c below 3 FAIL0.426
log_n_solution.c below 2 FAIL0.441
multivariate_1.c below TIMEOUT 300.007
multivariate_higher_order.c below 7 FAIL26.643
n_cubed_solution.c below EXCEPTION 0.34
n_log_n_solution.c below TIMEOUT 300.027
n_squared_two_base_case_even.c below 2 PASS0.385
n_squared_two_base_case_odd.c below 2 PASS0.387
pascals_dynamic.c below 3 FAIL20.127
pascals_iterative.c below 1 FAIL5.501
pascals_recursive.c below TIMEOUT 300.005
squared_solution.c below TIMEOUT 300.138
two_n_even.c below 2 PASS0.386
two_n_odd.c below 2 PASS0.367
two_to_n_over_two_even.c below TIMEOUT 300.034
two_to_n_over_two_odd.c below TIMEOUT 300.024
two_to_n_squared.c below 8 TIMEOUT 300.005
two_to_two_to_n.c below 7 FAIL1.67
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 0/0
ICRA Time = 2509.132
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.315
exp_add_loop_rec.c below 1 FAIL0.357
exp_add_loop_variable.c below 1 PASS0.351
exp_with_linear_inner_loop.c below 1 FAIL0.418
linear_two_to_n.c below 8 FAIL1.525
loop_five_to_n.c below 1 FAIL0.358
non_loop_five_to_n.c below 8 FAIL10.055
power_log.c below 1 PASS0.424
power_log_modified.c below 1 PASS0.49
simple_exponential.c below 1 PASS0.339
simple_exponential_for.c below 1 PASS0.347
two_to_n_minus_n.c below 8 FAIL1.817
two_to_n_minus_n_loop.c below 8 FAIL2.751
ICRA Assertions (True) = 6/13
ICRA Assertions (False) = 0/0
ICRA Time = 19.547