[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: 3f3626cb91d25fac166f7330b2ef6994712067de (2017-06-14 18:23:52 -0400) "Merge remote-tracking branch 'origin/ark2' into Newton-ark2"
# 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
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.391
kmp.c below 1 PASS1.421
qsort.c below 5 PASS3.73
speed_pldi09_fig1.c below 1 PASS0.39
speed_pldi09_fig4_2.c below 1 FAIL0.41
speed_pldi09_fig4_4.c below 1 PASS0.484
speed_pldi09_fig4_5.c below 1 PASS0.404
speed_pldi10_ex1.c below 1 PASS4.019
speed_pldi10_ex3.c below 1 PASS0.485
speed_pldi10_ex4.c below EXCEPTION 0.442
speed_popl10_fig2_1.c below 1 PASS0.405
speed_popl10_fig2_2.c below 1 FAIL0.381
speed_popl10_nested_multiple.c below 1 PASS0.461
speed_popl10_nested_single.c below 1 PASS0.404
speed_popl10_sequential_single.c below 1 PASS0.356
speed_popl10_simple_multiple.c below 1 PASS0.407
speed_popl10_simple_single_2.c below 1 PASS0.42
speed_popl10_simple_single.c below 1 PASS0.345
t07.c below 1 PASS0.37
t08.c below 1 PASS0.363
t09.c below 1 PASS0.386
t10.c below 1 PASS0.376
t11.c below 1 PASS0.412
t13.c below 1 FAIL0.432
t15.c below 1 PASS0.406
t16.c below 1 PASS0.399
t19.c below 1 PASS0.386
t20.c below 1 PASS0.363
t27.c below 1 PASS0.438
t28.c below 1 PASS0.433
t30.c below 1 FAIL0.367
t37.c below 2 PASS0.526
t39.c below 2 PASS0.497
t46.c below 1 PASS0.385
t47.c below 1 PASS0.4
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.294
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.39
qsort_full.c below 5 TIMEOUT 300.006
rec1-param_safe.c below 2 PASS0.371
rec1-param_unsafe.c below 2 OKAY0.379
rec1_safe.c below 2 PASS0.362
rec1_unsafe.c below 2 OKAY0.353
rec2-param_safe.c below 2 PASS0.35
rec2-param_unsafe.c below 2 OKAY0.359
rec2_safe.c below 2 PASS0.359
rec2_unsafe.c below 2 OKAY0.345
rec-test.c below 2 PASS0.363
sas03_bothbranches.c below 7 PASS1.323
sas03.c below 2 PASS0.849
simulated_lese_recursive.c below 2 PASS0.417
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 4/4
ICRA Time = 306.226
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.347
count_up_down_unsafe.c below 1 OKAY0.338
divide.c below 1 PASS0.345
factor_unsafe.c below 1 OKAY0.355
for_infinite_loop_1_safe.c below 1 PASS0.329
for_infinite_loop_2_safe.c below 1 PASS0.321
interproc.c below 1 PASS0.34
mult.c below 1 PASS0.348
pointer_arith.c below 1 PASS0.325
quotient.c below 3 PASS0.44
subtract.c below 1 PASS0.342
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.357
sum01_bug02_unsafe.c below 1 OKAY0.391
sum01_real_safe.c below 1 PASS0.338
sum01_safe.c below 1 PASS0.349
sum01_unsafe.c below 1 OKAY0.384
sum02_safe.c below 1 PASS0.329
sum03_safe.c below 1 PASS0.353
sum03_unsafe.c below 1 OKAY0.417
sum04_safe.c below 1 PASS0.333
sum04_unsafe.c below 1 OKAY0.389
terminator_02_safe.c below 1 PASS0.351
terminator_02_unsafe.c below 1 OKAY0.363
terminator_03_safe.c below 1 PASS0.351
terminator_03_unsafe.c below 1 OKAY0.354
token_ring01_safe.c below TIMEOUT 300.008
token_ring01_unsafe.c below TIMEOUT 300.008
toy_safe.c below EXCEPTION 209.077
trex01_safe.c below 1 PASS0.58
trex01_unsafe.c below 1 OKAY0.372
trex02_safe2.c below 3 PASS0.415
trex02_safe.c below 3 PASS0.411
trex02_unsafe.c below 3 OKAY0.408
trex03_safe.c below 1 PASS0.493
trex03_unsafe.c below 1 OKAY0.479
trex04_safe.c below 1 PASS0.371
while_infinite_loop_1_safe.c below 1 PASS0.34
while_infinite_loop_2_safe.c below 1 PASS0.343
while_infinite_loop_3_safe.c below 1 PASS0.328
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 822.522
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.474
blogger_simplified1.c below 3 PASS0.988
divided_difference2.c below TIMEOUT 300.006
mult-proc.c below 3 PASS0.39
mult-proc-params.c below 3 PASS0.441
popall.c below 1 PASS0.437
simulated_scc.c below 1 PASS0.575
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.311
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.368
degree2_binomial.c below 1 PASS0.501
degree2_monomial.c below 1 PASS0.37
degree3_binomial.c below 1 PASS0.909
degree3_monomial.c below 1 PASS0.446
degree4_binomial.c below 1 PASS1.249
degree4_monomial.c below 1 PASS0.522
degree5_binomial.c below 1 PASS1.887
degree5_monomial.c below 1 PASS0.569
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 6.821
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.365
cubic_with_square_interproc.c below 2 PASS0.385
cubic_with_square_nonlinear.c below 1 PASS0.38
cubic_with_square_nonlinear_interproc.c below 2 PASS0.389
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.369
cubic_with_square_unsafe.c below 1 OKAY0.368
multi-input.c below 1 PASS0.415
multi-input_unsafe.c below 1 OKAY0.466
nondet_loop_bound.c below 1 PASS0.383
nondet_loop_bound_quartic.c below 1 PASS0.392
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.379
nondet_loop_bound_unsafe.c below 1 OKAY0.388
nonlinear_stratified.c below 1 FAIL0.387
nonlinear_stratified_unsafe.c below 1 OKAY0.383
quartic_with_cube.c below 1 PASS0.361
quartic_with_cube_nonlinear.c below 1 PASS0.377
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.357
quartic_with_cube_unsafe.c below 1 OKAY0.386
quintic_with_quartic.c below 1 PASS0.377
quintic_with_quartic_nonlinear.c below 1 PASS0.392
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.398
quintic_with_quartic_unsafe.c below 1 OKAY0.389
ICRA Assertions (True) = 11/12
ICRA Assertions (False) = 10/10
ICRA Time = 8.486
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.541
degree2_FD_AllAux_AllAssm.c below 1 PASS3.774
degree2_FD_AllAux_FewAssm.c below 1 PASS5.708
degree2_FD_FewAux_FewAssm.c below 1 PASS0.722
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.75
degree3.c below 1 PASS0.565
degree3_FD.c below 1 PASS0.752
degree4.c below 1 PASS0.413
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 13.225
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.393
loop_unsafe.c below 1 OKAY0.419
simulated_lese_parser.c below 1 PASS0.351
simulated_lese_sentinel.c below 1 PASS0.366
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.529
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.375
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.375
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.016
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.016
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.357
array_false-unreach-call2.c below 1 OKAY0.38
array_false-unreach-call3.c below 1 OKAY0.362
array_true-unreach-call1.c below 1 FAIL0.366
array_true-unreach-call2.c below 1 FAIL0.37
array_true-unreach-call3.c below 1 PASS0.355
array_true-unreach-call4.c below 1 FAIL0.35
const_false-unreach-call1.c below 1 OKAY0.33
const_true-unreach-call1.c below 1 PASS0.322
diamond_false-unreach-call1.c below 1 OKAY0.357
diamond_true-unreach-call1.c below 1 PASS0.346
diamond_true-unreach-call2.c below 1 PASS0.387
functions_false-unreach-call1.c below 3 OKAY0.399
functions_true-unreach-call1.c below 3 PASS0.386
multivar_false-unreach-call1.c below 1 OKAY0.329
multivar_true-unreach-call1.c below 1 PASS0.331
nested_false-unreach-call1.c below 1 OKAY0.335
nested_true-unreach-call1.c below 1 PASS0.346
overflow_true-unreach-call1.c below 1 PASS0.329
phases_false-unreach-call1.c below 1 OKAY0.35
phases_false-unreach-call2.c below 1 OKAY0.359
phases_true-unreach-call1.c below 1 PASS0.343
phases_true-unreach-call2.c below 1 PASS0.356
simple_false-unreach-call1.c below 1 OKAY0.327
simple_false-unreach-call2.c below 1 OKAY0.328
simple_false-unreach-call3.c below 1 OKAY0.344
simple_false-unreach-call4.c below 1 OKAY0.338
simple_true-unreach-call1.c below 1 PASS0.334
simple_true-unreach-call2.c below 1 PASS0.342
simple_true-unreach-call3.c below 1 PASS0.344
simple_true-unreach-call4.c below 1 PASS0.344
underapprox_false-unreach-call1.c below 1 OKAY0.331
underapprox_false-unreach-call2.c below 1 OKAY0.345
underapprox_true-unreach-call1.c below 1 FAIL0.355
underapprox_true-unreach-call2.c below 1 PASS0.336
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.213
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.909
apache-get-tag_true-unreach-call.c below 1 FAIL0.466
down_true-unreach-call.c below 1 PASS0.353
fragtest_simple_true-unreach-call.c below 1 PASS0.393
half_2_true-unreach-call.c below 1 PASS0.37
heapsort_true-unreach-call.c below 1 TIMEOUT300.138
id_build_true-unreach-call.c below 1 PASS0.356
id_trans_false-unreach-call.c below 1 OKAY0.366
large_const_true-unreach-call.c below 1 PASS0.442
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.381
nested6_true-unreach-call.c below 1 FAIL0.42
nested9_true-unreach-call.c below 1 PASS0.457
nest-if3_true-unreach-call.c below 1 PASS0.443
NetBSD_loop_true-unreach-call.c below 1 PASS0.361
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.397
seq_true-unreach-call.c below 1 PASS0.394
SpamAssassin-loop_true-unreach-call.c below TIMEOUT 300.123
string_concat-noarr_true-unreach-call.c below 1 PASS0.384
up_true-unreach-call.c below 1 PASS0.374
ICRA Assertions (True) = 13/18
ICRA Assertions (False) = 1/1
ICRA Time = 607.527
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.367
bhmr2007_true-unreach-call.c below 1 PASS0.381
cggmp2005b_true-unreach-call.c below 1 PASS0.428
cggmp2005_true-unreach-call.c below 1 PASS0.342
cggmp2005_variant_true-unreach-call.c below 1 PASS0.351
css2003_true-unreach-call.c below 1 PASS0.502
ddlm2013_true-unreach-call.c below 1 PASS0.396
gcnr2008_false-unreach-call.c below 1 TIMEOUT300.181
gj2007b_true-unreach-call.c below 1 FAIL0.392
gj2007_true-unreach-call.c below 1 PASS0.375
gr2006_true-unreach-call.c below 1 PASS0.373
gsv2008_true-unreach-call.c below 1 PASS0.347
hhk2008_true-unreach-call.c below 1 PASS0.36
jm2006_true-unreach-call.c below 1 PASS0.389
jm2006_variant_true-unreach-call.c below 1 PASS0.404
mcmillan2006_true-unreach-call.c below 1 FAIL0.401
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 0/1
ICRA Time = 305.989
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.346
count_by_1_variant_true-unreach-call.c below 1 PASS0.347
count_by_2_true-unreach-call.c below 1 PASS0.312
count_by_k_true-unreach-call.c below 1 PASS0.335
count_by_nondet_true-unreach-call.c below 1 FAIL0.372
gauss_sum_true-unreach-call.c below 1 PASS0.376
half_true-unreach-call.c below EXCEPTION 0.368
nested_true-unreach-call.c below 1 PASS0.422
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.878
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.437
array_true-unreach-call.c below 1 FAIL0.453
bubble_sort_false-unreach-call.c below 4 OKAY199.077
bubble_sort_true-unreach-call.c below 1 PASS4.094
compact_false-unreach-call.c below 1 OKAY0.359
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.341
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.355
eureka_01_false-unreach-call.c below 1 OKAY2.387
eureka_01_true-unreach-call.c below 1 FAIL2.168
eureka_05_true-unreach-call.c below 1 FAIL1.099
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.348
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.326
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.343
heavy_false-unreach-call.c below 1 OKAY0.555
heavy_true-unreach-call.c below 1 PASS0.566
insertion_sort_false-unreach-call.c below 1 OKAY2.393
insertion_sort_true-unreach-call.c below 1 FAIL0.796
invert_string_false-unreach-call.c below 1 OKAY0.543
invert_string_true-unreach-call.c below 1 FAIL0.534
linear_sea.ch_true-unreach-call.c below 1 FAIL0.387
linear_search_false-unreach-call.c below 1 UNSOUND0.41
lu.cmp_true-unreach-call.c below TIMEOUT 300.261
ludcmp_false-unreach-call.c below TIMEOUT 300.251
matrix_false-unreach-call_true-termination.c below 1 OKAY1.042
matrix_true-unreach-call_true-termination.c below 1 FAIL0.489
n.c11_true-unreach-call.c below 3 FAIL0.452
n.c24_false-unreach-call.c below 3 OKAY25.401
n.c40_true-unreach-call.c below 1 FAIL0.395
nec11_false-unreach-call.c below 1 OKAY0.407
nec20_false-unreach-call.c below 1 OKAY0.401
nec40_true-unreach-call.c below 1 FAIL0.393
string_false-unreach-call.c below 1 OKAY0.639
string_true-unreach-call.c below 1 FAIL0.645
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.413
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.341
sum01_false-unreach-call_true-termination.c below 1 OKAY0.381
sum01_true-unreach-call_true-termination.c below 1 PASS0.348
sum03_false-unreach-call_true-termination.c below 1 OKAY0.506
sum03_true-unreach-call_false-termination.c below 1 PASS0.396
sum04_false-unreach-call_true-termination.c below 1 OKAY0.363
sum04_true-unreach-call_true-termination.c below 1 PASS0.34
sum_array_false-unreach-call.c below 1 OKAY0.656
sum_array_true-unreach-call.c below 1 FAIL0.731
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.342
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.447
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.344
trex01_false-unreach-call_true-termination.c below 3 OKAY0.493
trex01_true-unreach-call.c below 3 PASS0.827
trex02_false-unreach-call_true-termination.c below 3 OKAY0.414
trex02_true-unreach-call_true-termination.c below 3 PASS0.405
trex03_false-unreach-call_true-termination.c below 3 OKAY0.906
trex03_true-unreach-call.c below 3 PASS0.837
trex04_true-unreach-call_false-termination.c below 1 PASS0.384
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.346
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS26.381
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.371
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY18.464
vogal_false-unreach-call.c below 1 OKAY0.911
vogal_true-unreach-call.c below 1 FAIL0.936
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.306
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.319
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.327
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.334
ICRA Assertions (True) = 20/34
ICRA Assertions (False) = 30/32
ICRA Time = 908.342
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below TIMEOUT 300.034
Ackermann02_false-unreach-call_false-termination.c below TIMEOUT 300.032
Ackermann03_true-unreach-call.c below TIMEOUT 300.029
Ackermann04_true-unreach-call.c below TIMEOUT 300.032
Addition01_true-unreach-call_true-termination.c below 2 PASS0.59
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.596
Addition03_false-no-overflow.c below 2 PASS0.62
Addition03_true-unreach-call.c below 2 PASS0.616
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.485
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.463
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.452
Fibonacci01_true-unreach-call.c below EXCEPTION 1.015
Fibonacci02_true-unreach-call_true-termination.c below EXCEPTION 0.973
Fibonacci03_true-unreach-call_true-termination.c below EXCEPTION 1.061
Fibonacci04_false-unreach-call_true-termination.c below EXCEPTION 1.02
Fibonacci05_false-unreach-call_true-termination.c below EXCEPTION 1.043
gcd01_true-unreach-call_true-termination.c below 2 PASS0.549
gcd02_true-unreach-call.c below 2 FAIL1.504
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.547
McCarthy91_true-unreach-call.c below 7 FAIL1.495
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.753
Primes_true-unreach-call.c below 3 FAIL2.263
recHanoi01_true-unreach-call_true-termination.c below 9 FAIL6.459
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.411
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.409
ICRA Assertions (True) = 5/18
ICRA Assertions (False) = 4/7
ICRA Time = 1224.451
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.435
afterrec_2calls_true-unreach-call.c below 2 PASS0.407
afterrec_false-unreach-call.c below 2 OKAY0.364
afterrec_true-unreach-call.c below 2 PASS0.355
fibo_10_false-unreach-call.c below EXCEPTION 1.055
fibo_10_true-unreach-call.c below EXCEPTION 0.981
fibo_15_false-unreach-call.c below EXCEPTION 1.054
fibo_15_true-unreach-call.c below EXCEPTION 1.011
fibo_20_false-unreach-call.c below EXCEPTION 1.048
fibo_20_true-unreach-call.c below EXCEPTION 1.03
fibo_25_false-unreach-call.c below EXCEPTION 1.009
fibo_25_true-unreach-call.c below EXCEPTION 0.962
fibo_2calls_10_false-unreach-call.c below EXCEPTION 18.404
fibo_2calls_10_true-unreach-call.c below EXCEPTION 18.022
fibo_2calls_15_false-unreach-call.c below EXCEPTION 18.215
fibo_2calls_15_true-unreach-call.c below EXCEPTION 18.159
fibo_2calls_20_false-unreach-call.c below EXCEPTION 17.987
fibo_2calls_20_true-unreach-call.c below EXCEPTION 18.195
fibo_2calls_25_false-unreach-call.c below EXCEPTION 18.118
fibo_2calls_25_true-unreach-call.c below EXCEPTION 18.289
fibo_2calls_2_false-unreach-call.c below EXCEPTION 18.013
fibo_2calls_2_true-unreach-call.c below EXCEPTION 18.269
fibo_2calls_4_false-unreach-call.c below EXCEPTION 18.102
fibo_2calls_4_true-unreach-call.c below EXCEPTION 18.049
fibo_2calls_5_false-unreach-call.c below EXCEPTION 18.193
fibo_2calls_5_true-unreach-call.c below EXCEPTION 18.253
fibo_2calls_6_false-unreach-call.c below EXCEPTION 18.183
fibo_2calls_6_true-unreach-call.c below EXCEPTION 18.278
fibo_2calls_8_false-unreach-call.c below EXCEPTION 18.05
fibo_2calls_8_true-unreach-call.c below EXCEPTION 18.01
fibo_5_false-unreach-call.c below EXCEPTION 0.992
fibo_5_true-unreach-call.c below EXCEPTION 0.997
fibo_7_false-unreach-call.c below EXCEPTION 0.998
fibo_7_true-unreach-call.c below EXCEPTION 0.986
id2_b2_o3_true-unreach-call.c below 2 PASS0.988
id2_b3_o2_false-unreach-call.c below 2 OKAY1.031
id2_b3_o5_true-unreach-call.c below 2 PASS0.99
id2_b5_o10_true-unreach-call.c below 2 PASS1.02
id2_i5_o5_false-unreach-call.c below 2 OKAY0.469
id2_i5_o5_true-unreach-call.c below 2 PASS0.427
id_b2_o3_true-unreach-call.c below 2 PASS0.614
id_b3_o2_false-unreach-call.c below 2 OKAY0.582
id_b3_o5_true-unreach-call.c below 2 PASS0.587
id_b5_o10_true-unreach-call.c below 2 PASS0.586
id_i10_o10_false-unreach-call.c below 2 OKAY0.39
id_i10_o10_true-unreach-call.c below 2 PASS0.385
id_i15_o15_false-unreach-call.c below 2 OKAY0.39
id_i15_o15_true-unreach-call.c below 2 PASS0.385
id_i20_o20_false-unreach-call.c below 2 OKAY0.375
id_i20_o20_true-unreach-call.c below 2 PASS0.379
id_i25_o25_false-unreach-call.c below 2 OKAY0.374
id_i25_o25_true-unreach-call.c below 2 PASS0.393
id_i5_o5_false-unreach-call.c below 2 OKAY0.403
id_i5_o5_true-unreach-call.c below 2 PASS0.399
id_o1000_false-unreach-call.c below 2 OKAY0.383
id_o100_false-unreach-call.c below 2 OKAY0.391
id_o10_false-unreach-call.c below 2 OKAY0.387
id_o200_false-unreach-call.c below 2 OKAY0.406
id_o20_false-unreach-call.c below 2 OKAY0.396
id_o3_false-unreach-call.c below 2 OKAY0.395
sum_10x0_false-unreach-call.c below 2 OKAY0.413
sum_10x0_true-unreach-call.c below 2 PASS0.405
sum_15x0_false-unreach-call.c below 2 OKAY0.41
sum_15x0_true-unreach-call.c below 2 PASS0.39
sum_20x0_false-unreach-call.c below 2 OKAY0.429
sum_20x0_true-unreach-call.c below 2 PASS0.399
sum_25x0_false-unreach-call.c below 2 OKAY0.405
sum_25x0_true-unreach-call.c below 2 PASS0.407
sum_2x3_false-unreach-call.c below 2 OKAY0.41
sum_2x3_true-unreach-call.c below 2 PASS0.399
sum_non_eq_false-unreach-call.c below 2 OKAY0.436
sum_non_eq_true-unreach-call.c below 2 PASS0.447
sum_non_false-unreach-call.c below 2 OKAY0.423
sum_non_true-unreach-call.c below 2 PASS0.42
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 359.791
/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.389
rec-bhmr2007_true-unreach-call.c below 2 PASS0.437
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.772
rec-cggmp2005_true-unreach-call.c below 2 PASS0.345
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.372
rec-css2003_true-unreach-call.c below 2 PASS0.638
rec-ddlm2013_true-unreach-call.c below EXCEPTION 0.379
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.928
rec-gj2007b_true-unreach-call.c below 2 FAIL0.411
rec-gj2007_true-unreach-call.c below 2 FAIL0.397
rec-gr2006_true-unreach-call.c below 2 FAIL0.419
rec-gsv2008_true-unreach-call.c below 2 PASS0.372
rec-hhk2008_true-unreach-call.c below 2 PASS0.386
rec-jm2006_true-unreach-call.c below 2 PASS0.385
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.414
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.436
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.48
/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.355
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.368
rec-count_by_2_true-unreach-call.c below 2 PASS0.355
rec-count_by_k_true-unreach-call.c below 2 PASS0.377
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.406
rec-gauss_sum_true-unreach-call.c below 2 PASS0.378
rec-half_true-unreach-call.c below EXCEPTION 0.352
rec-nested_true-unreach-call.c below 3 PASS0.604
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.195
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.524
edit_distance_bottom_up.c below 3 TIMEOUT 300.008
edit_distance_top_down.c below 3 FAIL53.133
log_log_n_solution.c below 3 FAIL0.472
log_n_solution.c below 2 FAIL0.473
multivariate_1.c below TIMEOUT 300.007
multivariate_higher_order.c below 7 FAIL28.242
n_cubed_solution.c below EXCEPTION 0.356
n_log_n_solution.c below TIMEOUT 300.039
n_squared_two_base_case_even.c below 2 PASS0.423
n_squared_two_base_case_odd.c below 2 PASS0.393
pascals_dynamic.c below 3 FAIL20.963
pascals_iterative.c below 1 FAIL5.754
pascals_recursive.c below TIMEOUT 300.007
squared_solution.c below TIMEOUT 300.143
two_n_even.c below 2 PASS0.407
two_n_odd.c below 2 PASS0.377
two_to_n_over_two_even.c below TIMEOUT 300.022
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.748
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 0/0
ICRA Time = 2513.519
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.329
binary_search_array_tree.c below 1 FAIL1.458
exp_add_loop_rec.c below 1 FAIL0.372
exp_add_loop_variable.c below 1 PASS0.364
exp_with_linear_inner_loop.c below 1 FAIL0.443
halving_log1.c below 1 PASS0.479
linear_two_to_n.c below 8 FAIL1.635
loop_five_to_n.c below 1 FAIL0.366
non_loop_five_to_n.c below 8 FAIL10.788
power_log.c below 1 PASS0.432
power_log_modified.c below 1 PASS0.499
simple_exponential.c below 1 PASS0.376
simple_exponential_for.c below 1 PASS0.362
two_to_n_minus_n.c below 8 FAIL1.876
two_to_n_minus_n_loop.c below 8 FAIL2.92
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 0/0
ICRA Time = 22.699