[Version Information]
WALi-OpenNWA version: 0f994ef6a5cbe02200899575605ae35f227d9ddb (2017-07-12 11:45:09 -0500) "Added programs and files used for POPL18"
duet version: 37312f93042d9322883c425e7b53f0a32ea6ba3b (2017-07-05 19:03:26 -0400) "Big O bounds in print_hull"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.5.3  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
camlp4               4.02+7  Camlp4 is a system for writing extensible parsers f
cil                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
conf-which                1  Virtual package relying on which
cppo                  1.4.1  Equivalent of the C preprocessor for OCaml programs
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170101  LR(1) parser generator
mlgmpidl              1.2.4  OCaml interface to the GMP library
num                       0  The Num library for arbitrary-precision integer and
oasis                 0.4.8  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.1  A library manager for OCaml
ocamlgraph            1.8.7  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.8  Generate OCaml modules from source files
OCRS             20170627v3  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.348
kmp.c below 1 PASS1.598
qsort.c below 5 PASS0.881
speed_pldi09_fig1.c below 1 PASS0.487
speed_pldi09_fig4_2.c below 1 FAIL0.386
speed_pldi09_fig4_4.c below 1 PASS20.875
speed_pldi09_fig4_5.c below 1 PASS0.402
speed_pldi10_ex1.c below 1 PASS1.183
speed_pldi10_ex3.c below 1 PASS0.508
speed_pldi10_ex4.c below 1 PASS0.54
speed_popl10_fig2_1.c below 1 PASS0.445
speed_popl10_fig2_2.c below 1 FAIL0.371
speed_popl10_nested_multiple.c below 1 PASS0.45
speed_popl10_nested_single.c below 1 PASS0.421
speed_popl10_sequential_single.c below 1 PASS0.379
speed_popl10_simple_multiple.c below 1 PASS0.5
speed_popl10_simple_single_2.c below 1 PASS0.614
speed_popl10_simple_single.c below 1 PASS0.339
t07.c below 1 PASS0.426
t08.c below 1 PASS0.386
t09.c below 1 PASS0.374
t10.c below 1 PASS0.365
t11.c below 1 PASS0.456
t13.c below 1 FAIL0.404
t15.c below 1 PASS0.428
t16.c below 1 PASS0.399
t19.c below 1 PASS0.393
t20.c below 1 PASS0.381
t27.c below 1 PASS0.547
t28.c below 1 PASS0.461
t30.c below 1 FAIL0.413
t37.c below 2 PASS0.589
t39.c below 2 PASS0.554
t46.c below 1 PASS0.388
t47.c below 1 FAIL0.561
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 38.252
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.375
qsort_full.c below 4 PASS5.538
rec1-param_safe.c below 2 PASS0.372
rec1-param_unsafe.c below 2 OKAY0.397
rec1_safe.c below 2 PASS0.378
rec1_unsafe.c below 2 OKAY0.367
rec2-param_safe.c below 2 PASS0.356
rec2-param_unsafe.c below 2 OKAY0.349
rec2_safe.c below 2 PASS0.372
rec2_unsafe.c below 2 OKAY0.372
rec-test.c below 2 PASS0.374
sas03_bothbranches.c below 7 PASS0.688
sas03.c below 2 PASS0.785
simulated_lese_recursive.c below 2 PASS0.441
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.164
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.334
count_up_down_unsafe.c below 1 OKAY0.353
divide.c below 1 PASS0.332
factor_unsafe.c below 1 OKAY0.332
for_infinite_loop_1_safe.c below 1 PASS0.32
for_infinite_loop_2_safe.c below 1 PASS0.309
interproc.c below 1 PASS0.32
mult.c below 1 PASS0.328
pointer_arith.c below 1 PASS0.303
quotient.c below 3 PASS0.487
subtract.c below 1 PASS0.32
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.342
sum01_bug02_unsafe.c below 1 OKAY0.597
sum01_real_safe.c below 1 PASS0.344
sum01_safe.c below 1 PASS0.349
sum01_unsafe.c below 1 OKAY0.463
sum02_safe.c below 1 PASS0.362
sum03_safe.c below 1 PASS0.398
sum03_unsafe.c below 1 OKAY0.509
sum04_safe.c below 1 PASS0.346
sum04_unsafe.c below 1 OKAY0.47
terminator_02_safe.c below 1 PASS0.311
terminator_02_unsafe.c below 1 OKAY0.349
terminator_03_safe.c below 1 PASS0.323
terminator_03_unsafe.c below 1 OKAY0.325
token_ring01_safe.c below 4 FAIL65.427
token_ring01_unsafe.c below 4 OKAY166.429
toy_safe.c below EXCEPTION 164.287
trex01_safe.c below 1 PASS0.746
trex01_unsafe.c below 1 OKAY0.373
trex02_safe2.c below 3 PASS0.396
trex02_safe.c below 3 PASS0.401
trex02_unsafe.c below 3 OKAY0.403
trex03_safe.c below 1 PASS0.416
trex03_unsafe.c below 1 OKAY0.41
trex04_safe.c below 1 PASS0.359
while_infinite_loop_1_safe.c below 1 PASS0.3
while_infinite_loop_2_safe.c below 1 PASS0.302
while_infinite_loop_3_safe.c below 1 PASS0.306
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 409.781
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.371
blogger_simplified1.c below 3 PASS1.044
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.375
mult-proc-params.c below 3 PASS0.392
popall.c below 1 PASS0.652
simulated_scc.c below 1 PASS0.626
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.465
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.355
degree2_binomial.c below 1 PASS0.708
degree2_monomial.c below 1 PASS0.387
degree3_binomial.c below 1 PASS1.329
degree3_monomial.c below 1 PASS0.446
degree4_binomial.c below 1 PASS2.607
degree4_monomial.c below 1 PASS0.496
degree5_binomial.c below 1 PASS7.126
degree5_monomial.c below 1 PASS0.56
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 14.014
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.433
cubic_with_square_interproc.c below 2 PASS0.575
cubic_with_square_nonlinear.c below 1 PASS0.355
cubic_with_square_nonlinear_interproc.c below 2 PASS0.402
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.37
cubic_with_square_unsafe.c below 1 OKAY0.437
multi-input.c below 1 PASS210.625
multi-input_unsafe.c below 1 OKAY0.484
nondet_loop_bound.c below 1 PASS0.338
nondet_loop_bound_quartic.c below 1 PASS0.386
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.387
nondet_loop_bound_unsafe.c below 1 OKAY0.388
nonlinear_stratified.c below 1 PASS78.893
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube.c below 1 PASS0.582
quartic_with_cube_nonlinear.c below 1 PASS0.394
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.385
quartic_with_cube_unsafe.c below 1 OKAY0.482
quintic_with_quartic.c below 1 PASS0.988
quintic_with_quartic_nonlinear.c below 1 PASS0.42
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.429
quintic_with_quartic_unsafe.c below 1 OKAY1.002
ICRA Assertions (True) = 12/12
ICRA Assertions (False) = 9/10
ICRA Time = 598.759
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.671
degree2_FD_AllAux_AllAssm.c below 1 PASS150.012
degree2_FD_AllAux_FewAssm.c below 1 PASS4.8
degree2_FD_FewAux_FewAssm.c below 1 PASS0.864
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.874
degree3.c below 1 PASS0.616
degree3_FD.c below 1 PASS0.809
degree4.c below 1 PASS0.411
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 159.057
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.441
loop_unsafe.c below 1 OKAY0.47
simulated_lese_parser.c below 1 PASS0.361
simulated_lese_sentinel.c below 1 PASS0.379
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.651
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.354
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.354
/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.341
array_false-unreach-call2.c below 1 OKAY0.357
array_false-unreach-call3.c below 1 OKAY0.345
array_true-unreach-call1.c below 1 FAIL0.355
array_true-unreach-call2.c below 1 FAIL0.363
array_true-unreach-call3.c below 1 PASS0.347
array_true-unreach-call4.c below 1 FAIL0.335
const_false-unreach-call1.c below 1 OKAY0.333
const_true-unreach-call1.c below 1 PASS0.325
diamond_false-unreach-call1.c below 1 OKAY0.353
diamond_true-unreach-call1.c below 1 PASS0.354
diamond_true-unreach-call2.c below 1 PASS0.364
functions_false-unreach-call1.c below 3 OKAY0.38
functions_true-unreach-call1.c below 3 PASS0.393
multivar_false-unreach-call1.c below 1 OKAY0.365
multivar_true-unreach-call1.c below 1 PASS0.331
nested_false-unreach-call1.c below 1 OKAY0.365
nested_true-unreach-call1.c below 1 PASS0.372
overflow_true-unreach-call1.c below 1 PASS0.327
phases_false-unreach-call1.c below 1 OKAY0.397
phases_false-unreach-call2.c below 1 OKAY0.333
phases_true-unreach-call1.c below 1 PASS0.382
phases_true-unreach-call2.c below 1 PASS0.348
simple_false-unreach-call1.c below 1 OKAY0.33
simple_false-unreach-call2.c below 1 OKAY0.304
simple_false-unreach-call3.c below 1 OKAY0.311
simple_false-unreach-call4.c below 1 OKAY0.32
simple_true-unreach-call1.c below 1 PASS0.334
simple_true-unreach-call2.c below 1 PASS0.321
simple_true-unreach-call3.c below 1 PASS0.32
simple_true-unreach-call4.c below 1 PASS0.336
underapprox_false-unreach-call1.c below 1 OKAY0.333
underapprox_false-unreach-call2.c below 1 OKAY0.342
underapprox_true-unreach-call1.c below 1 FAIL0.342
underapprox_true-unreach-call2.c below 1 PASS0.345
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.103
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.802
apache-get-tag_true-unreach-call.c below 1 FAIL0.425
down_true-unreach-call.c below 1 PASS0.363
fragtest_simple_true-unreach-call.c below 1 PASS0.455
half_2_true-unreach-call.c below 1 PASS0.386
heapsort_true-unreach-call.c below 1 TIMEOUT300.196
id_build_true-unreach-call.c below 1 PASS0.476
id_trans_false-unreach-call.c below 1 OKAY0.34
large_const_true-unreach-call.c below 1 PASS0.423
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.4
nested6_true-unreach-call.c below 1 FAIL0.497
nested9_true-unreach-call.c below 1 PASS0.486
nest-if3_true-unreach-call.c below 1 PASS0.463
NetBSD_loop_true-unreach-call.c below 1 PASS0.328
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.377
seq_true-unreach-call.c below 1 PASS0.443
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.394
string_concat-noarr_true-unreach-call.c below 1 PASS0.377
up_true-unreach-call.c below 1 PASS0.364
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 308.995
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.362
bhmr2007_true-unreach-call.c below 1 PASS0.377
cggmp2005b_true-unreach-call.c below 1 PASS0.469
cggmp2005_true-unreach-call.c below 1 PASS0.345
cggmp2005_variant_true-unreach-call.c below 1 PASS0.352
css2003_true-unreach-call.c below 1 PASS0.758
ddlm2013_true-unreach-call.c below 1 PASS0.497
gcnr2008_false-unreach-call.c below 1 OKAY0.895
gj2007b_true-unreach-call.c below 1 FAIL0.368
gj2007_true-unreach-call.c below 1 PASS0.412
gr2006_true-unreach-call.c below 1 PASS0.43
gsv2008_true-unreach-call.c below 1 PASS0.329
hhk2008_true-unreach-call.c below 1 PASS0.331
jm2006_true-unreach-call.c below 1 PASS0.402
jm2006_variant_true-unreach-call.c below 1 PASS0.435
mcmillan2006_true-unreach-call.c below 1 FAIL0.359
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.121
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.32
count_by_1_variant_true-unreach-call.c below 1 PASS0.369
count_by_2_true-unreach-call.c below 1 PASS0.32
count_by_k_true-unreach-call.c below 1 PASS0.339
count_by_nondet_true-unreach-call.c below 1 FAIL0.35
gauss_sum_true-unreach-call.c below 1 PASS0.362
half_true-unreach-call.c below 1 FAIL0.361
nested_true-unreach-call.c below 1 PASS0.403
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.824
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.368
array_true-unreach-call.c below 1 FAIL0.372
bubble_sort_false-unreach-call.c below 4 OKAY49.419
bubble_sort_true-unreach-call.c below 1 PASS3.508
compact_false-unreach-call.c below 1 OKAY0.384
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.343
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.356
eureka_01_false-unreach-call.c below 1 OKAY1.978
eureka_01_true-unreach-call.c below 1 FAIL1.414
eureka_05_true-unreach-call.c below TIMEOUT 300.004
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.344
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.327
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.329
heavy_false-unreach-call.c below 1 OKAY0.452
heavy_true-unreach-call.c below 1 PASS0.433
insertion_sort_false-unreach-call.c below 1 OKAY1.528
insertion_sort_true-unreach-call.c below 1 FAIL0.526
invert_string_false-unreach-call.c below 1 OKAY0.493
invert_string_true-unreach-call.c below 1 FAIL0.52
linear_sea.ch_true-unreach-call.c below 1 FAIL0.379
linear_search_false-unreach-call.c below 1 OKAY0.375
lu.cmp_true-unreach-call.c below 3 PASS15.871
ludcmp_false-unreach-call.c below 3 OKAY16.054
matrix_false-unreach-call_true-termination.c below 1 OKAY0.976
matrix_true-unreach-call_true-termination.c below 1 FAIL0.409
n.c11_true-unreach-call.c below 3 FAIL0.421
n.c24_false-unreach-call.c below 3 OKAY2.635
n.c40_true-unreach-call.c below 1 FAIL0.349
nec11_false-unreach-call.c below 1 OKAY0.355
nec20_false-unreach-call.c below 1 OKAY0.387
nec40_true-unreach-call.c below 1 FAIL0.351
string_false-unreach-call.c below 1 OKAY0.584
string_true-unreach-call.c below 1 FAIL0.602
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.607
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.346
sum01_false-unreach-call_true-termination.c below 1 OKAY0.452
sum01_true-unreach-call_true-termination.c below 1 PASS0.344
sum03_false-unreach-call_true-termination.c below 1 OKAY0.484
sum03_true-unreach-call_false-termination.c below 1 PASS0.433
sum04_false-unreach-call_true-termination.c below 1 OKAY0.467
sum04_true-unreach-call_true-termination.c below 1 PASS0.341
sum_array_false-unreach-call.c below 1 OKAY0.574
sum_array_true-unreach-call.c below 1 FAIL0.597
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.318
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.433
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.337
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.329
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.342
trex01_false-unreach-call_true-termination.c below 3 OKAY0.435
trex01_true-unreach-call.c below 3 PASS0.67
trex02_false-unreach-call_true-termination.c below 3 OKAY0.381
trex02_true-unreach-call_true-termination.c below 3 PASS0.389
trex03_false-unreach-call_true-termination.c below 3 OKAY0.633
trex03_true-unreach-call.c below 3 PASS0.655
trex04_true-unreach-call_false-termination.c below 1 PASS0.367
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.337
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.401
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.373
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.354
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY3.752
vogal_false-unreach-call.c below 1 OKAY0.749
vogal_true-unreach-call.c below 1 FAIL0.742
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.307
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.303
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.299
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 425.707
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.901
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.906
Ackermann03_true-unreach-call.c below 7 FAIL0.961
Ackermann04_true-unreach-call.c below 7 FAIL0.957
Addition01_true-unreach-call_true-termination.c below 2 PASS0.533
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.53
Addition03_false-no-overflow.c below 2 PASS0.511
Addition03_true-unreach-call.c below 2 PASS0.554
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.461
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.401
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.412
Fibonacci01_true-unreach-call.c below 7 FAIL0.68
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.685
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.667
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.656
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.692
gcd01_true-unreach-call_true-termination.c below 2 PASS0.514
gcd02_true-unreach-call.c below 2 FAIL0.918
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY6.884
McCarthy91_true-unreach-call.c below 7 PASS6.857
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.545
Primes_true-unreach-call.c below 3 FAIL1.356
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.665
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.369
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.379
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 7/7
ICRA Time = 29.994
/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.385
afterrec_false-unreach-call.c below 2 OKAY0.371
afterrec_true-unreach-call.c below 2 PASS0.378
fibo_10_false-unreach-call.c below 7 OKAY0.7
fibo_10_true-unreach-call.c below 7 FAIL0.663
fibo_15_false-unreach-call.c below 7 OKAY0.676
fibo_15_true-unreach-call.c below 7 FAIL0.688
fibo_20_false-unreach-call.c below 7 OKAY0.653
fibo_20_true-unreach-call.c below 7 FAIL0.664
fibo_25_false-unreach-call.c below 7 OKAY0.683
fibo_25_true-unreach-call.c below 7 FAIL0.689
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.028
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.008
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.01
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.01
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.008
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.009
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.01
fibo_5_false-unreach-call.c below 7 OKAY0.667
fibo_5_true-unreach-call.c below 7 FAIL0.657
fibo_7_false-unreach-call.c below 7 OKAY0.661
fibo_7_true-unreach-call.c below 7 FAIL0.653
id2_b2_o3_true-unreach-call.c below 2 PASS0.618
id2_b3_o2_false-unreach-call.c below 2 OKAY0.662
id2_b3_o5_true-unreach-call.c below 2 PASS0.603
id2_b5_o10_true-unreach-call.c below 2 PASS0.613
id2_i5_o5_false-unreach-call.c below 2 OKAY0.395
id2_i5_o5_true-unreach-call.c below 2 PASS0.395
id_b2_o3_true-unreach-call.c below 2 PASS0.534
id_b3_o2_false-unreach-call.c below 2 OKAY0.511
id_b3_o5_true-unreach-call.c below 2 PASS0.521
id_b5_o10_true-unreach-call.c below 2 PASS0.523
id_i10_o10_false-unreach-call.c below 2 OKAY0.367
id_i10_o10_true-unreach-call.c below 2 PASS0.365
id_i15_o15_false-unreach-call.c below 2 OKAY0.36
id_i15_o15_true-unreach-call.c below 2 PASS0.374
id_i20_o20_false-unreach-call.c below 2 OKAY0.388
id_i20_o20_true-unreach-call.c below 2 PASS0.385
id_i25_o25_false-unreach-call.c below 2 OKAY0.384
id_i25_o25_true-unreach-call.c below 2 PASS0.361
id_i5_o5_false-unreach-call.c below 2 OKAY0.37
id_i5_o5_true-unreach-call.c below 2 PASS0.378
id_o1000_false-unreach-call.c below 2 OKAY0.371
id_o100_false-unreach-call.c below 2 OKAY0.36
id_o10_false-unreach-call.c below 2 OKAY0.373
id_o200_false-unreach-call.c below 2 OKAY0.375
id_o20_false-unreach-call.c below 2 OKAY0.371
id_o3_false-unreach-call.c below 2 OKAY0.373
sum_10x0_false-unreach-call.c below 2 OKAY0.413
sum_10x0_true-unreach-call.c below 2 PASS0.414
sum_15x0_false-unreach-call.c below 2 OKAY0.404
sum_15x0_true-unreach-call.c below 2 PASS0.411
sum_20x0_false-unreach-call.c below 2 OKAY0.407
sum_20x0_true-unreach-call.c below 2 PASS0.424
sum_25x0_false-unreach-call.c below 2 OKAY0.392
sum_25x0_true-unreach-call.c below 2 PASS0.417
sum_2x3_false-unreach-call.c below 2 OKAY0.396
sum_2x3_true-unreach-call.c below 2 PASS0.408
sum_non_eq_false-unreach-call.c below 2 OKAY0.392
sum_non_eq_true-unreach-call.c below 2 PASS0.4
sum_non_false-unreach-call.c below 2 OKAY0.421
sum_non_true-unreach-call.c below 2 PASS0.418
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5426.856
/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.417
rec-bhmr2007_true-unreach-call.c below 2 PASS0.392
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.611
rec-cggmp2005_true-unreach-call.c below 2 PASS0.382
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.414
rec-css2003_true-unreach-call.c below 2 PASS0.978
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.084
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.731
rec-gj2007b_true-unreach-call.c below 2 FAIL0.356
rec-gj2007_true-unreach-call.c below 2 FAIL0.46
rec-gr2006_true-unreach-call.c below 2 FAIL0.458
rec-gsv2008_true-unreach-call.c below 2 PASS0.435
rec-hhk2008_true-unreach-call.c below 2 PASS0.378
rec-jm2006_true-unreach-call.c below 2 PASS0.446
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.512
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.405
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.459
/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.374
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.396
rec-count_by_2_true-unreach-call.c below 2 PASS0.35
rec-count_by_k_true-unreach-call.c below 2 PASS0.387
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.389
rec-gauss_sum_true-unreach-call.c below 2 PASS0.397
rec-half_true-unreach-call.c below 2 FAIL0.396
rec-nested_true-unreach-call.c below 3 FAIL0.526
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.215
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.496
cubic_polynomial_unsafe.c below 2 OKAY0.487
edit_distance_bottom_up.c below 3 FAIL124.899
edit_distance_top_down.c below 3 FAIL2.602
log_log_n_solution.c below 3 FAIL0.417
log_log_n_solution_unsafe.c below 3 OKAY0.432
log_n_solution.c below 2 FAIL0.441
log_n_solution_unsafe.c below 2 OKAY0.427
multivariate_1.c below TIMEOUT 300.004
multivariate_1_unsafe.c below TIMEOUT 300.004
multivariate_higher_order.c below 7 FAIL18.777
multivariate_higher_order_unsafe.c below 7 OKAY18.593
n_cubed_solution.c below EXCEPTION 45.472
n_cubed_solution_unsafe.c below EXCEPTION 0.025
n_log_n_solution.c below TIMEOUT 300.051
n_log_n_solution_unsafe.c below TIMEOUT 300.05
n_squared_two_base_case_even.c below 2 PASS0.47
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.473
n_squared_two_base_case_odd.c below 2 PASS0.467
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.479
pascals_dynamic.c below 3 FAIL2.368
pascals_dynamic_unsafe.c below 3 OKAY2.413
pascals_iterative.c below 1 FAIL3.568
pascals_iterative_unsafe.c below 1 OKAY3.537
pascals_recursive.c below 8 FAIL9.407
pascals_recursive_unsafe.c below 8 OKAY9.459
squared_solution.c below TIMEOUT 300.004
squared_solution_unsafe.c below TIMEOUT 300.004
two_n_even.c below 2 PASS0.392
two_n_even_unsafe.c below 2 OKAY0.41
two_n_odd.c below 2 PASS0.407
two_n_odd_unsafe.c below 2 OKAY0.42
two_to_n_over_two_even.c below TIMEOUT 300.004
two_to_n_over_two_even_unsafe.c below TIMEOUT 300.004
two_to_n_over_two_odd.c below TIMEOUT 300.004
two_to_n_over_two_odd_unsafe.c below TIMEOUT 300.004
two_to_n_squared.c below 8 FAIL20.355
two_to_n_squared_unsafe.c below 8 OKAY20.875
two_to_two_to_n.c below 7 FAIL0.818
two_to_two_to_n_unsafe.c below 7 OKAY0.864
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 13/19
ICRA Time = 3290.383
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.359
adding_and_mult_unsafe.c below 1 OKAY0.379
binary_search_array_tree.c below 1 FAIL0.646
exp_add_linear.c below 1 PASS0.42
exp_add_linear_unsafe.c below 1 OKAY0.433
exp_add_loop_rec.c below 1 FAIL0.347
exp_add_loop_rec_unsafe.c below 1 OKAY0.364
exp_add_loop_variable.c below 1 PASS0.411
exp_add_loop_variable_unsafe.c below 1 OKAY0.416
exp_with_linear_inner_loop.c below 1 FAIL0.487
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.486
halving_log1.c below 1 FAIL0.514
linear_two_to_n.c below 8 FAIL1.122
linear_two_to_n_unsafe.c below 8 OKAY1.075
loop_five_to_n.c below 1 PASS0.409
loop_five_to_n_unsafe.c below 1 OKAY0.401
non_loop_five_to_n.c below TIMEOUT 300.032
non_loop_five_to_n_unsafe.c below TIMEOUT 300.028
power_log.c below 1 PASS0.48
power_log_modified.c below 1 PASS0.49
simple_exponential.c below 1 PASS0.39
simple_exponential_for.c below 1 PASS0.388
simple_exponential_for_unsafe.c below 1 OKAY0.394
simple_exponential_unsafe.c below 1 OKAY0.404
two_to_n_minus_n.c below 7 FAIL1.159
two_to_n_minus_n_loop.c below 7 FAIL1.594
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.612
two_to_n_minus_n_unsafe.c below 7 OKAY1.143
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 616.383