[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.369
kmp.c below 1 PASS1.651
qsort.c below 5 PASS0.872
speed_pldi09_fig1.c below 1 PASS0.494
speed_pldi09_fig4_2.c below 1 FAIL0.405
speed_pldi09_fig4_4.c below 1 PASS21.144
speed_pldi09_fig4_5.c below 1 PASS0.394
speed_pldi10_ex1.c below 1 PASS1.167
speed_pldi10_ex3.c below 1 PASS0.495
speed_pldi10_ex4.c below 1 PASS0.518
speed_popl10_fig2_1.c below 1 PASS0.458
speed_popl10_fig2_2.c below 1 FAIL0.358
speed_popl10_nested_multiple.c below 1 PASS0.446
speed_popl10_nested_single.c below 1 PASS0.44
speed_popl10_sequential_single.c below 1 PASS0.376
speed_popl10_simple_multiple.c below 1 PASS0.537
speed_popl10_simple_single_2.c below 1 PASS0.631
speed_popl10_simple_single.c below 1 PASS0.36
t07.c below 1 PASS0.426
t08.c below 1 PASS0.409
t09.c below 1 PASS0.394
t10.c below 1 PASS0.355
t11.c below 1 PASS0.453
t13.c below 1 FAIL0.406
t15.c below 1 PASS0.435
t16.c below 1 PASS0.394
t19.c below 1 PASS0.389
t20.c below 1 PASS0.374
t27.c below 1 PASS0.556
t28.c below 1 PASS0.443
t30.c below 1 FAIL0.409
t37.c below 2 PASS0.603
t39.c below 2 PASS0.544
t46.c below 1 PASS0.413
t47.c below 1 FAIL0.551
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 38.669
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.377
qsort_full.c below 4 PASS5.593
rec1-param_safe.c below 2 PASS0.38
rec1-param_unsafe.c below 2 OKAY0.403
rec1_safe.c below 2 PASS0.372
rec1_unsafe.c below 2 OKAY0.398
rec2-param_safe.c below 2 PASS0.373
rec2-param_unsafe.c below 2 OKAY0.362
rec2_safe.c below 2 PASS0.368
rec2_unsafe.c below 2 OKAY0.361
rec-test.c below 2 PASS0.364
sas03_bothbranches.c below 7 PASS0.672
sas03.c below 2 PASS0.815
simulated_lese_recursive.c below 2 PASS0.438
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.276
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.331
count_up_down_unsafe.c below 1 OKAY0.342
divide.c below 1 PASS0.341
factor_unsafe.c below 1 OKAY0.337
for_infinite_loop_1_safe.c below 1 PASS0.377
for_infinite_loop_2_safe.c below 1 PASS0.311
interproc.c below 1 PASS0.311
mult.c below 1 PASS0.332
pointer_arith.c below 1 PASS0.297
quotient.c below 3 PASS0.482
subtract.c below 1 PASS0.326
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.356
sum01_bug02_unsafe.c below 1 OKAY0.589
sum01_real_safe.c below 1 PASS0.323
sum01_safe.c below 1 PASS0.339
sum01_unsafe.c below 1 OKAY0.462
sum02_safe.c below 1 PASS0.35
sum03_safe.c below 1 PASS0.393
sum03_unsafe.c below 1 OKAY0.479
sum04_safe.c below 1 PASS0.348
sum04_unsafe.c below 1 OKAY0.459
terminator_02_safe.c below 1 PASS0.336
terminator_02_unsafe.c below 1 OKAY0.352
terminator_03_safe.c below 1 PASS0.329
terminator_03_unsafe.c below 1 OKAY0.342
token_ring01_safe.c below 4 FAIL68.882
token_ring01_unsafe.c below 4 OKAY233.29
toy_safe.c below EXCEPTION 169.39
trex01_safe.c below 1 PASS0.572
trex01_unsafe.c below 1 OKAY0.368
trex02_safe2.c below 3 PASS0.384
trex02_safe.c below 3 PASS0.387
trex02_unsafe.c below 3 OKAY0.403
trex03_safe.c below 1 PASS0.431
trex03_unsafe.c below 1 OKAY0.439
trex04_safe.c below 1 PASS0.347
while_infinite_loop_1_safe.c below 1 PASS0.304
while_infinite_loop_2_safe.c below 1 PASS0.308
while_infinite_loop_3_safe.c below 1 PASS0.317
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 485.066
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.371
blogger_simplified1.c below 3 PASS1.042
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.368
mult-proc-params.c below 3 PASS0.383
popall.c below 1 PASS0.665
simulated_scc.c below 1 PASS0.636
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.469
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.361
degree2_binomial.c below 1 PASS0.73
degree2_monomial.c below 1 PASS0.399
degree3_binomial.c below 1 PASS1.398
degree3_monomial.c below 1 PASS0.426
degree4_binomial.c below 1 PASS2.696
degree4_monomial.c below 1 PASS0.499
degree5_binomial.c below 1 PASS7.178
degree5_monomial.c below 1 PASS0.572
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 14.259
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.444
cubic_with_square_interproc.c below 2 PASS0.565
cubic_with_square_nonlinear.c below 1 PASS0.375
cubic_with_square_nonlinear_interproc.c below 2 PASS0.4
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.383
cubic_with_square_unsafe.c below 1 OKAY0.443
multi-input.c below 1 PASS214.021
multi-input_unsafe.c below 1 OKAY0.488
nondet_loop_bound.c below 1 PASS0.366
nondet_loop_bound_quartic.c below 1 PASS0.386
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.371
nondet_loop_bound_unsafe.c below 1 OKAY0.365
nonlinear_stratified.c below 1 PASS79.422
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube.c below 1 PASS0.583
quartic_with_cube_nonlinear.c below 1 PASS0.373
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.394
quartic_with_cube_unsafe.c below 1 OKAY0.483
quintic_with_quartic.c below 1 PASS1.043
quintic_with_quartic_nonlinear.c below 1 PASS0.424
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.42
quintic_with_quartic_unsafe.c below 1 OKAY1.052
ICRA Assertions (True) = 12/12
ICRA Assertions (False) = 9/10
ICRA Time = 602.805
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.674
degree2_FD_AllAux_AllAssm.c below 1 PASS158.329
degree2_FD_AllAux_FewAssm.c below 1 PASS4.949
degree2_FD_FewAux_FewAssm.c below 1 PASS0.906
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.878
degree3.c below 1 PASS0.621
degree3_FD.c below 1 PASS0.823
degree4.c below 1 PASS0.424
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 167.604
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.423
loop_unsafe.c below 1 OKAY0.45
simulated_lese_parser.c below 1 PASS0.346
simulated_lese_sentinel.c below 1 PASS0.343
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.562
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.355
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.355
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.004
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.004
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.348
array_false-unreach-call2.c below 1 OKAY0.364
array_false-unreach-call3.c below 1 OKAY0.353
array_true-unreach-call1.c below 1 FAIL0.354
array_true-unreach-call2.c below 1 FAIL0.367
array_true-unreach-call3.c below 1 PASS0.35
array_true-unreach-call4.c below 1 FAIL0.346
const_false-unreach-call1.c below 1 OKAY0.345
const_true-unreach-call1.c below 1 PASS0.345
diamond_false-unreach-call1.c below 1 OKAY0.36
diamond_true-unreach-call1.c below 1 PASS0.355
diamond_true-unreach-call2.c below 1 PASS0.386
functions_false-unreach-call1.c below 3 OKAY0.379
functions_true-unreach-call1.c below 3 PASS0.382
multivar_false-unreach-call1.c below 1 OKAY0.361
multivar_true-unreach-call1.c below 1 PASS0.345
nested_false-unreach-call1.c below 1 OKAY0.378
nested_true-unreach-call1.c below 1 PASS0.379
overflow_true-unreach-call1.c below 1 PASS0.324
phases_false-unreach-call1.c below 1 OKAY0.405
phases_false-unreach-call2.c below 1 OKAY0.343
phases_true-unreach-call1.c below 1 PASS0.392
phases_true-unreach-call2.c below 1 PASS0.34
simple_false-unreach-call1.c below 1 OKAY0.321
simple_false-unreach-call2.c below 1 OKAY0.317
simple_false-unreach-call3.c below 1 OKAY0.315
simple_false-unreach-call4.c below 1 OKAY0.336
simple_true-unreach-call1.c below 1 PASS0.324
simple_true-unreach-call2.c below 1 PASS0.324
simple_true-unreach-call3.c below 1 PASS0.323
simple_true-unreach-call4.c below 1 PASS0.323
underapprox_false-unreach-call1.c below 1 OKAY0.344
underapprox_false-unreach-call2.c below 1 OKAY0.347
underapprox_true-unreach-call1.c below 1 FAIL0.342
underapprox_true-unreach-call2.c below 1 PASS0.341
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.258
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.84
apache-get-tag_true-unreach-call.c below 1 FAIL0.438
down_true-unreach-call.c below 1 PASS0.373
fragtest_simple_true-unreach-call.c below 1 PASS0.441
half_2_true-unreach-call.c below 1 PASS0.383
heapsort_true-unreach-call.c below 1 TIMEOUT300.218
id_build_true-unreach-call.c below 1 PASS0.527
id_trans_false-unreach-call.c below 1 OKAY0.338
large_const_true-unreach-call.c below 1 PASS0.409
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.38
nested6_true-unreach-call.c below 1 FAIL0.494
nested9_true-unreach-call.c below 1 PASS0.512
nest-if3_true-unreach-call.c below 1 PASS0.478
NetBSD_loop_true-unreach-call.c below 1 PASS0.345
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.377
seq_true-unreach-call.c below 1 PASS0.429
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.477
string_concat-noarr_true-unreach-call.c below 1 PASS0.393
up_true-unreach-call.c below 1 PASS0.373
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 309.225
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.375
bhmr2007_true-unreach-call.c below 1 PASS0.386
cggmp2005b_true-unreach-call.c below 1 PASS0.503
cggmp2005_true-unreach-call.c below 1 PASS0.352
cggmp2005_variant_true-unreach-call.c below 1 PASS0.356
css2003_true-unreach-call.c below 1 PASS0.775
ddlm2013_true-unreach-call.c below 1 PASS0.525
gcnr2008_false-unreach-call.c below 1 OKAY0.89
gj2007b_true-unreach-call.c below 1 FAIL0.37
gj2007_true-unreach-call.c below 1 PASS0.43
gr2006_true-unreach-call.c below 1 PASS0.424
gsv2008_true-unreach-call.c below 1 PASS0.339
hhk2008_true-unreach-call.c below 1 PASS0.329
jm2006_true-unreach-call.c below 1 PASS0.412
jm2006_variant_true-unreach-call.c below 1 PASS0.447
mcmillan2006_true-unreach-call.c below 1 FAIL0.378
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.291
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.336
count_by_1_variant_true-unreach-call.c below 1 PASS0.373
count_by_2_true-unreach-call.c below 1 PASS0.316
count_by_k_true-unreach-call.c below 1 PASS0.333
count_by_nondet_true-unreach-call.c below 1 FAIL0.343
gauss_sum_true-unreach-call.c below 1 PASS0.363
half_true-unreach-call.c below 1 FAIL0.368
nested_true-unreach-call.c below 1 PASS0.416
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.848
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.374
array_true-unreach-call.c below 1 FAIL0.434
bubble_sort_false-unreach-call.c below 4 OKAY48.808
bubble_sort_true-unreach-call.c below 1 PASS3.592
compact_false-unreach-call.c below 1 OKAY0.4
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.344
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.355
eureka_01_false-unreach-call.c below 1 OKAY1.982
eureka_01_true-unreach-call.c below 1 FAIL1.422
eureka_05_true-unreach-call.c below TIMEOUT 300.004
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.33
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.32
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.334
heavy_false-unreach-call.c below 1 OKAY0.454
heavy_true-unreach-call.c below 1 PASS0.443
insertion_sort_false-unreach-call.c below 1 OKAY1.575
insertion_sort_true-unreach-call.c below 1 FAIL0.563
invert_string_false-unreach-call.c below 1 OKAY0.507
invert_string_true-unreach-call.c below 1 FAIL0.529
linear_sea.ch_true-unreach-call.c below 1 FAIL0.382
linear_search_false-unreach-call.c below 1 OKAY0.392
lu.cmp_true-unreach-call.c below 3 PASS16.156
ludcmp_false-unreach-call.c below 3 OKAY16.483
matrix_false-unreach-call_true-termination.c below 1 OKAY1.036
matrix_true-unreach-call_true-termination.c below 1 FAIL0.41
n.c11_true-unreach-call.c below 3 FAIL0.436
n.c24_false-unreach-call.c below 3 OKAY2.6
n.c40_true-unreach-call.c below 1 FAIL0.354
nec11_false-unreach-call.c below 1 OKAY0.356
nec20_false-unreach-call.c below 1 OKAY0.385
nec40_true-unreach-call.c below 1 FAIL0.359
string_false-unreach-call.c below 1 OKAY0.614
string_true-unreach-call.c below 1 FAIL0.599
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.595
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.331
sum01_false-unreach-call_true-termination.c below 1 OKAY0.461
sum01_true-unreach-call_true-termination.c below 1 PASS0.35
sum03_false-unreach-call_true-termination.c below 1 OKAY0.484
sum03_true-unreach-call_false-termination.c below 1 PASS0.425
sum04_false-unreach-call_true-termination.c below 1 OKAY0.5
sum04_true-unreach-call_true-termination.c below 1 PASS0.339
sum_array_false-unreach-call.c below 1 OKAY0.565
sum_array_true-unreach-call.c below 1 FAIL0.619
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.332
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.446
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.353
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.342
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.343
trex01_false-unreach-call_true-termination.c below 3 OKAY0.447
trex01_true-unreach-call.c below 3 PASS0.653
trex02_false-unreach-call_true-termination.c below 3 OKAY0.389
trex02_true-unreach-call_true-termination.c below 3 PASS0.403
trex03_false-unreach-call_true-termination.c below 3 OKAY0.681
trex03_true-unreach-call.c below 3 PASS0.647
trex04_true-unreach-call_false-termination.c below 1 PASS0.382
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.352
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.515
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.368
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.355
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY3.932
vogal_false-unreach-call.c below 1 OKAY0.741
vogal_true-unreach-call.c below 1 FAIL0.738
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.312
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.295
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.318
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.314
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 426.659
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.949
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.898
Ackermann03_true-unreach-call.c below 7 FAIL1.04
Ackermann04_true-unreach-call.c below 7 FAIL1.001
Addition01_true-unreach-call_true-termination.c below 2 PASS0.539
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.57
Addition03_false-no-overflow.c below 2 PASS0.54
Addition03_true-unreach-call.c below 2 PASS0.529
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.472
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.419
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.442
Fibonacci01_true-unreach-call.c below 7 FAIL0.684
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.679
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.685
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.676
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.699
gcd01_true-unreach-call_true-termination.c below 2 PASS0.534
gcd02_true-unreach-call.c below 2 FAIL0.925
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY6.938
McCarthy91_true-unreach-call.c below 7 PASS6.894
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.532
Primes_true-unreach-call.c below 3 FAIL1.348
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.696
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.376
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.384
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 7/7
ICRA Time = 30.449
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.407
afterrec_2calls_true-unreach-call.c below 2 PASS0.404
afterrec_false-unreach-call.c below 2 OKAY0.373
afterrec_true-unreach-call.c below 2 PASS0.36
fibo_10_false-unreach-call.c below 7 OKAY0.692
fibo_10_true-unreach-call.c below 7 FAIL0.668
fibo_15_false-unreach-call.c below 7 OKAY0.653
fibo_15_true-unreach-call.c below 7 FAIL0.682
fibo_20_false-unreach-call.c below 7 OKAY0.656
fibo_20_true-unreach-call.c below 7 FAIL0.653
fibo_25_false-unreach-call.c below 7 OKAY0.677
fibo_25_true-unreach-call.c below 7 FAIL0.672
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.033
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.01
fibo_5_false-unreach-call.c below 7 OKAY0.676
fibo_5_true-unreach-call.c below 7 FAIL0.659
fibo_7_false-unreach-call.c below 7 OKAY0.667
fibo_7_true-unreach-call.c below 7 FAIL0.659
id2_b2_o3_true-unreach-call.c below 2 PASS0.629
id2_b3_o2_false-unreach-call.c below 2 OKAY0.662
id2_b3_o5_true-unreach-call.c below 2 PASS0.625
id2_b5_o10_true-unreach-call.c below 2 PASS0.627
id2_i5_o5_false-unreach-call.c below 2 OKAY0.415
id2_i5_o5_true-unreach-call.c below 2 PASS0.401
id_b2_o3_true-unreach-call.c below 2 PASS0.534
id_b3_o2_false-unreach-call.c below 2 OKAY0.544
id_b3_o5_true-unreach-call.c below 2 PASS0.558
id_b5_o10_true-unreach-call.c below 2 PASS0.558
id_i10_o10_false-unreach-call.c below 2 OKAY0.376
id_i10_o10_true-unreach-call.c below 2 PASS0.378
id_i15_o15_false-unreach-call.c below 2 OKAY0.374
id_i15_o15_true-unreach-call.c below 2 PASS0.384
id_i20_o20_false-unreach-call.c below 2 OKAY0.393
id_i20_o20_true-unreach-call.c below 2 PASS0.374
id_i25_o25_false-unreach-call.c below 2 OKAY0.366
id_i25_o25_true-unreach-call.c below 2 PASS0.387
id_i5_o5_false-unreach-call.c below 2 OKAY0.37
id_i5_o5_true-unreach-call.c below 2 PASS0.384
id_o1000_false-unreach-call.c below 2 OKAY0.39
id_o100_false-unreach-call.c below 2 OKAY0.382
id_o10_false-unreach-call.c below 2 OKAY0.372
id_o200_false-unreach-call.c below 2 OKAY0.394
id_o20_false-unreach-call.c below 2 OKAY0.386
id_o3_false-unreach-call.c below 2 OKAY0.387
sum_10x0_false-unreach-call.c below 2 OKAY0.429
sum_10x0_true-unreach-call.c below 2 PASS0.415
sum_15x0_false-unreach-call.c below 2 OKAY0.42
sum_15x0_true-unreach-call.c below 2 PASS0.417
sum_20x0_false-unreach-call.c below 2 OKAY0.428
sum_20x0_true-unreach-call.c below 2 PASS0.401
sum_25x0_false-unreach-call.c below 2 OKAY0.402
sum_25x0_true-unreach-call.c below 2 PASS0.411
sum_2x3_false-unreach-call.c below 2 OKAY0.407
sum_2x3_true-unreach-call.c below 2 PASS0.418
sum_non_eq_false-unreach-call.c below 2 OKAY0.408
sum_non_eq_true-unreach-call.c below 2 PASS0.402
sum_non_false-unreach-call.c below 2 OKAY0.416
sum_non_true-unreach-call.c below 2 PASS0.402
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5427.227
/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.416
rec-bhmr2007_true-unreach-call.c below 2 PASS0.388
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.631
rec-cggmp2005_true-unreach-call.c below 2 PASS0.384
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.414
rec-css2003_true-unreach-call.c below 2 PASS0.943
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.084
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.752
rec-gj2007b_true-unreach-call.c below 2 FAIL0.392
rec-gj2007_true-unreach-call.c below 2 FAIL0.446
rec-gr2006_true-unreach-call.c below 2 FAIL0.491
rec-gsv2008_true-unreach-call.c below 2 PASS0.436
rec-hhk2008_true-unreach-call.c below 2 PASS0.393
rec-jm2006_true-unreach-call.c below 2 PASS0.449
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.485
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.428
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.532
/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.352
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.391
rec-count_by_2_true-unreach-call.c below 2 PASS0.365
rec-count_by_k_true-unreach-call.c below 2 PASS0.401
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.401
rec-gauss_sum_true-unreach-call.c below 2 PASS0.404
rec-half_true-unreach-call.c below 2 FAIL0.388
rec-nested_true-unreach-call.c below 3 FAIL0.516
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.218
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.505
cubic_polynomial_unsafe.c below 2 OKAY0.493
edit_distance_bottom_up.c below 3 FAIL125.614
edit_distance_top_down.c below 3 FAIL2.651
log_log_n_solution.c below 3 FAIL0.425
log_log_n_solution_unsafe.c below 3 OKAY0.434
log_n_solution.c below 2 FAIL0.437
log_n_solution_unsafe.c below 2 OKAY0.42
multivariate_1.c below TIMEOUT 300.006
multivariate_1_unsafe.c below TIMEOUT 300.004
multivariate_higher_order.c below 7 FAIL19.168
multivariate_higher_order_unsafe.c below 7 OKAY18.894
n_cubed_solution.c below EXCEPTION 45.75
n_cubed_solution_unsafe.c below EXCEPTION 0.024
n_log_n_solution.c below TIMEOUT 300.059
n_log_n_solution_unsafe.c below TIMEOUT 300.051
n_squared_two_base_case_even.c below 2 PASS0.476
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.495
n_squared_two_base_case_odd.c below 2 PASS0.468
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.497
pascals_dynamic.c below 3 FAIL2.432
pascals_dynamic_unsafe.c below 3 OKAY2.428
pascals_iterative.c below 1 FAIL3.507
pascals_iterative_unsafe.c below 1 OKAY3.497
pascals_recursive.c below 8 FAIL9.7
pascals_recursive_unsafe.c below 8 OKAY9.662
squared_solution.c below TIMEOUT 300.004
squared_solution_unsafe.c below TIMEOUT 300.007
two_n_even.c below 2 PASS0.388
two_n_even_unsafe.c below 2 OKAY0.407
two_n_odd.c below 2 PASS0.394
two_n_odd_unsafe.c below 2 OKAY0.412
two_to_n_over_two_even.c below TIMEOUT 300.004
two_to_n_over_two_even_unsafe.c below TIMEOUT 300.007
two_to_n_over_two_odd.c below TIMEOUT 300.006
two_to_n_over_two_odd_unsafe.c below TIMEOUT 300.004
two_to_n_squared.c below 8 FAIL20.823
two_to_n_squared_unsafe.c below 8 OKAY20.553
two_to_two_to_n.c below 7 FAIL0.819
two_to_two_to_n_unsafe.c below 7 OKAY0.841
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 13/19
ICRA Time = 3292.766
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.381
adding_and_mult_unsafe.c below 1 OKAY0.366
binary_search_array_tree.c below 1 FAIL0.593
exp_add_linear.c below 1 PASS0.429
exp_add_linear_unsafe.c below 1 OKAY0.426
exp_add_loop_rec.c below 1 FAIL0.359
exp_add_loop_rec_unsafe.c below 1 OKAY0.358
exp_add_loop_variable.c below 1 PASS0.405
exp_add_loop_variable_unsafe.c below 1 OKAY0.405
exp_with_linear_inner_loop.c below 1 FAIL0.473
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.475
halving_log1.c below 1 FAIL0.508
linear_two_to_n.c below 8 FAIL1.064
linear_two_to_n_unsafe.c below 8 OKAY1.056
loop_five_to_n.c below 1 PASS0.368
loop_five_to_n_unsafe.c below 1 OKAY0.392
non_loop_five_to_n.c below TIMEOUT 300.042
non_loop_five_to_n_unsafe.c below TIMEOUT 300.032
power_log.c below 1 PASS0.486
power_log_modified.c below 1 PASS0.5
simple_exponential.c below 1 PASS0.389
simple_exponential_for.c below 1 PASS0.385
simple_exponential_for_unsafe.c below 1 OKAY0.397
simple_exponential_unsafe.c below 1 OKAY0.384
two_to_n_minus_n.c below 7 FAIL1.185
two_to_n_minus_n_loop.c below 7 FAIL1.607
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.649
two_to_n_minus_n_unsafe.c below 7 OKAY1.161
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 616.275
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.511
02.c below 3 FAIL0.649
03.c below 1 PASS0.416
04.c below 1 PASS0.338
05.c below 3 PASS1.691
06.c below 3 PASS5.643
07.c below 3 PASS0.521
08.c below 3 PASS1.001
09.c below 3 PASS0.593
10.c below 3 FAIL0.793
11.c below 1 PASS0.344
12.c below 3 PASS1.533
13.c below 3 PASS0.473
14.c below 3 PASS0.425
15.c below 1 PASS0.331
16.c below 1 PASS0.408
17.c below EXCEPTION 0.37
18.c below 1 PASS0.397
19.c below 1 PASS0.435
20.c below 3 FAIL0.577
21.c below 3 PASS0.45
22.c below 3 FAIL0.619
23.c below 1 PASS0.35
24.c below 1 PASS0.376
25.c below 3 FAIL1.131
26.c below TIMEOUT 300.005
27.c below 1 PASS0.423
28.c below 3 PASS0.457
29.c below 3 PASS0.735
30.c below 1 PASS0.376
31.c below 3 PASS0.764
32.c below 1 FAIL0.372
33.c below 3 PASS1.203
34.c below 1 FAIL0.381
35.c below 1 PASS0.325
36.c below 3 PASS2.789
37.c below 3 FAIL0.465
38.c below 1 FAIL0.381
39.c below 3 PASS0.394
40.c below 3 PASS0.646
41.c below 1 PASS0.389
42.c below 3 PASS0.789
43.c below 3 PASS0.441
44.c below 1 PASS0.379
45.c below 3 FAIL3.449
46.c below 3 FAIL1.644
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 337.182
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.376
AGHKTW2017_foo.c below 1 PASS0.389
AGHKTW2017_loginSafe.c below 1 PASS0.774
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.427
BCK2011_gauss.c below 1 PASS0.434
BCK2011_strength_reduction.c below 1 PASS0.41
BCK2011_strength_reduction_linear.c below 1 PASS0.43
fibonacci_information_flow.c below 1 PASS0.571
TA2005_fib2.c below 1 PASS0.554
TA2005_fib.c below 1 PASS0.441
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.806