[Version Information]
WALi-OpenNWA version: 0f994ef6a5cbe02200899575605ae35f227d9ddb (2017-07-12 11:45:09 -0500) "Added programs and files used for POPL18"
duet version: 81b6696f6f312fabfa1611e9943c2a6ea2f1ed79 (2017-07-20 23:59:08 +0200) "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-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.363
kmp.c below 1 PASS1.758
qsort.c below 5 PASS0.948
speed_pldi09_fig1.c below 1 PASS0.516
speed_pldi09_fig4_2.c below 1 FAIL0.402
speed_pldi09_fig4_4.c below 1 PASS4.788
speed_pldi09_fig4_5.c below 1 PASS0.416
speed_pldi10_ex1.c below 1 PASS1.236
speed_pldi10_ex3.c below 1 PASS0.509
speed_pldi10_ex4.c below 1 PASS0.524
speed_popl10_fig2_1.c below 1 PASS0.457
speed_popl10_fig2_2.c below 1 FAIL0.372
speed_popl10_nested_multiple.c below 1 PASS0.476
speed_popl10_nested_single.c below 1 PASS0.455
speed_popl10_sequential_single.c below 1 PASS0.398
speed_popl10_simple_multiple.c below 1 PASS0.503
speed_popl10_simple_single_2.c below 1 PASS0.642
speed_popl10_simple_single.c below 1 PASS0.338
t07.c below 1 PASS0.418
t08.c below 1 PASS0.392
t09.c below 1 PASS0.393
t10.c below 1 PASS0.371
t11.c below 1 PASS0.469
t13.c below 1 FAIL0.411
t15.c below 1 PASS0.425
t16.c below 1 PASS0.417
t19.c below 1 PASS0.396
t20.c below 1 PASS0.368
t27.c below 1 PASS0.567
t28.c below 1 PASS0.472
t30.c below 1 FAIL0.444
t37.c below 2 PASS0.629
t39.c below 2 PASS0.521
t46.c below 1 PASS0.419
t47.c below 1 FAIL0.565
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.778
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.377
qsort_full.c below 4 PASS6.149
rec1-param_safe.c below 2 PASS0.38
rec1-param_unsafe.c below 2 OKAY0.389
rec1_safe.c below 2 PASS0.372
rec1_unsafe.c below 2 OKAY0.365
rec2-param_safe.c below 2 PASS0.376
rec2-param_unsafe.c below 2 OKAY0.38
rec2_safe.c below 2 PASS0.365
rec2_unsafe.c below 2 OKAY0.357
rec-test.c below 2 PASS0.374
sas03_bothbranches.c below 7 PASS0.702
sas03.c below 2 PASS0.719
simulated_lese_recursive.c below 2 PASS0.447
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.752
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.33
count_up_down_unsafe.c below 1 OKAY0.349
divide.c below 1 PASS0.351
factor_unsafe.c below 1 OKAY0.33
for_infinite_loop_1_safe.c below 1 PASS0.318
for_infinite_loop_2_safe.c below 1 PASS0.322
interproc.c below 1 PASS0.306
mult.c below 1 PASS0.334
pointer_arith.c below 1 PASS0.305
quotient.c below 3 PASS0.492
subtract.c below 1 PASS0.333
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.353
sum01_bug02_unsafe.c below 1 OKAY0.6
sum01_real_safe.c below 1 PASS0.328
sum01_safe.c below 1 PASS0.354
sum01_unsafe.c below 1 OKAY0.466
sum02_safe.c below 1 PASS0.36
sum03_safe.c below 1 PASS0.389
sum03_unsafe.c below 1 OKAY0.483
sum04_safe.c below 1 PASS0.346
sum04_unsafe.c below 1 OKAY0.485
terminator_02_safe.c below 1 PASS0.316
terminator_02_unsafe.c below 1 OKAY0.369
terminator_03_safe.c below 1 PASS0.332
terminator_03_unsafe.c below 1 OKAY0.337
token_ring01_safe.c below 4 FAIL97.41
token_ring01_unsafe.c below 4 TIMEOUT 300.02
toy_safe.c below EXCEPTION 170.25
trex01_safe.c below 1 PASS0.534
trex01_unsafe.c below 1 OKAY0.38
trex02_safe2.c below 3 PASS0.405
trex02_safe.c below 3 PASS0.385
trex02_unsafe.c below 3 OKAY0.396
trex03_safe.c below 1 PASS0.429
trex03_unsafe.c below 1 OKAY0.425
trex04_safe.c below 1 PASS0.344
while_infinite_loop_1_safe.c below 1 PASS0.31
while_infinite_loop_2_safe.c below 1 PASS0.305
while_infinite_loop_3_safe.c below 1 PASS0.316
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 581.197
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.385
blogger_simplified1.c below 3 PASS1.102
divided_difference2.c below TIMEOUT 300.007
mult-proc.c below 3 PASS0.372
mult-proc-params.c below 3 PASS0.386
popall.c below 1 PASS0.68
simulated_scc.c below 1 PASS0.649
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.581
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.346
degree2_binomial.c below 1 FAIL0.853
degree2_monomial.c below 1 PASS0.407
degree3_binomial.c below 1 FAIL1.345
degree3_monomial.c below 1 PASS0.438
degree4_binomial.c below 1 FAIL3.084
degree4_monomial.c below 1 PASS0.501
degree5_binomial.c below 1 FAIL9.283
degree5_monomial.c below 1 PASS0.606
ICRA Assertions (True) = 5/9
ICRA Assertions (False) = 0/0
ICRA Time = 16.863
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.453
cubic_with_square_interproc.c below 2 FAIL0.569
cubic_with_square_nonlinear.c below 1 FAIL0.371
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.425
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.377
cubic_with_square_unsafe.c below 1 OKAY0.439
multi-input.c below 1 PASS214.195
multi-input_unsafe.c below 1 OKAY0.504
nondet_loop_bound.c below 1 FAIL0.367
nondet_loop_bound_quartic.c below 1 FAIL0.392
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.394
nondet_loop_bound_unsafe.c below 1 OKAY0.359
nonlinear_stratified.c below 1 PASS79.867
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.005
quartic_with_cube.c below 1 PASS0.599
quartic_with_cube_nonlinear.c below 1 FAIL0.382
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.396
quartic_with_cube_unsafe.c below 1 OKAY0.491
quintic_with_quartic.c below 1 PASS0.996
quintic_with_quartic_nonlinear.c below 1 PASS0.419
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.428
quintic_with_quartic_unsafe.c below 1 OKAY1.024
ICRA Assertions (True) = 6/12
ICRA Assertions (False) = 9/10
ICRA Time = 603.452
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.683
degree2_FD_AllAux_AllAssm.c below 1 PASS218.737
degree2_FD_AllAux_FewAssm.c below 1 PASS5.032
degree2_FD_FewAux_FewAssm.c below 1 PASS0.881
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.888
degree3.c below 1 PASS0.645
degree3_FD.c below 1 PASS0.823
degree4.c below 1 PASS0.437
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 228.126
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.437
loop_unsafe.c below 1 OKAY0.453
simulated_lese_parser.c below 1 PASS0.347
simulated_lese_sentinel.c below 1 PASS0.351
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.588
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.347
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.347
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.007
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.007
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.349
array_false-unreach-call2.c below 1 OKAY0.352
array_false-unreach-call3.c below 1 OKAY0.351
array_true-unreach-call1.c below 1 FAIL0.351
array_true-unreach-call2.c below 1 FAIL0.376
array_true-unreach-call3.c below 1 PASS0.34
array_true-unreach-call4.c below 1 FAIL0.341
const_false-unreach-call1.c below 1 OKAY0.335
const_true-unreach-call1.c below 1 PASS0.336
diamond_false-unreach-call1.c below 1 OKAY0.356
diamond_true-unreach-call1.c below 1 PASS0.355
diamond_true-unreach-call2.c below 1 PASS0.373
functions_false-unreach-call1.c below 3 OKAY0.376
functions_true-unreach-call1.c below 3 PASS0.37
multivar_false-unreach-call1.c below 1 OKAY0.355
multivar_true-unreach-call1.c below 1 PASS0.343
nested_false-unreach-call1.c below 1 OKAY0.376
nested_true-unreach-call1.c below 1 PASS0.349
overflow_true-unreach-call1.c below 1 PASS0.327
phases_false-unreach-call1.c below 1 OKAY0.418
phases_false-unreach-call2.c below 1 OKAY0.342
phases_true-unreach-call1.c below 1 PASS0.409
phases_true-unreach-call2.c below 1 PASS0.344
simple_false-unreach-call1.c below 1 OKAY0.323
simple_false-unreach-call2.c below 1 OKAY0.315
simple_false-unreach-call3.c below 1 OKAY0.306
simple_false-unreach-call4.c below 1 OKAY0.336
simple_true-unreach-call1.c below 1 PASS0.318
simple_true-unreach-call2.c below 1 PASS0.316
simple_true-unreach-call3.c below 1 PASS0.321
simple_true-unreach-call4.c below 1 PASS0.326
underapprox_false-unreach-call1.c below 1 OKAY0.338
underapprox_false-unreach-call2.c below 1 OKAY0.347
underapprox_true-unreach-call1.c below 1 FAIL0.359
underapprox_true-unreach-call2.c below 1 PASS0.327
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.156
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.864
apache-get-tag_true-unreach-call.c below 1 FAIL0.421
down_true-unreach-call.c below 1 PASS0.388
fragtest_simple_true-unreach-call.c below 1 PASS0.442
half_2_true-unreach-call.c below 1 PASS0.397
heapsort_true-unreach-call.c below 1 PASS1.363
id_build_true-unreach-call.c below 1 PASS0.349
id_trans_false-unreach-call.c below 1 OKAY0.351
large_const_true-unreach-call.c below 1 PASS0.418
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.375
nested6_true-unreach-call.c below 1 FAIL0.494
nested9_true-unreach-call.c below 1 PASS0.504
nest-if3_true-unreach-call.c below 1 PASS0.485
NetBSD_loop_true-unreach-call.c below 1 PASS0.362
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.389
seq_true-unreach-call.c below 1 PASS0.418
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.341
string_concat-noarr_true-unreach-call.c below 1 PASS0.399
up_true-unreach-call.c below 1 PASS0.366
ICRA Assertions (True) = 15/18
ICRA Assertions (False) = 1/1
ICRA Time = 10.126
/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.372
cggmp2005b_true-unreach-call.c below 1 PASS0.52
cggmp2005_true-unreach-call.c below 1 PASS0.351
cggmp2005_variant_true-unreach-call.c below 1 PASS0.348
css2003_true-unreach-call.c below 1 PASS0.767
ddlm2013_true-unreach-call.c below 1 PASS0.511
gcnr2008_false-unreach-call.c below 1 OKAY0.92
gj2007b_true-unreach-call.c below 1 FAIL0.381
gj2007_true-unreach-call.c below 1 PASS0.459
gr2006_true-unreach-call.c below 1 PASS0.432
gsv2008_true-unreach-call.c below 1 PASS0.354
hhk2008_true-unreach-call.c below 1 PASS0.346
jm2006_true-unreach-call.c below 1 PASS0.425
jm2006_variant_true-unreach-call.c below 1 PASS0.459
mcmillan2006_true-unreach-call.c below 1 FAIL0.385
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.397
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.326
count_by_1_variant_true-unreach-call.c below 1 PASS0.379
count_by_2_true-unreach-call.c below 1 PASS0.324
count_by_k_true-unreach-call.c below 1 PASS0.336
count_by_nondet_true-unreach-call.c below 1 FAIL0.343
gauss_sum_true-unreach-call.c below 1 PASS0.388
half_true-unreach-call.c below 1 FAIL0.362
nested_true-unreach-call.c below 1 PASS0.419
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.877
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.388
array_true-unreach-call.c below 1 FAIL0.38
bubble_sort_false-unreach-call.c below 4 OKAY48.784
bubble_sort_true-unreach-call.c below 1 PASS3.716
compact_false-unreach-call.c below 1 OKAY0.406
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.351
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.346
eureka_01_false-unreach-call.c below 1 OKAY2.142
eureka_01_true-unreach-call.c below 1 FAIL1.483
eureka_05_true-unreach-call.c below 1 FAIL0.661
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.341
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.33
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.324
heavy_false-unreach-call.c below 1 OKAY0.471
heavy_true-unreach-call.c below 1 PASS0.463
insertion_sort_false-unreach-call.c below 1 OKAY1.724
insertion_sort_true-unreach-call.c below 1 FAIL0.601
invert_string_false-unreach-call.c below 1 OKAY0.513
invert_string_true-unreach-call.c below 1 FAIL0.525
linear_sea.ch_true-unreach-call.c below 1 FAIL0.375
linear_search_false-unreach-call.c below 1 OKAY0.385
lu.cmp_true-unreach-call.c below 3 PASS17.73
ludcmp_false-unreach-call.c below 3 OKAY17.971
matrix_false-unreach-call_true-termination.c below 1 OKAY1.071
matrix_true-unreach-call_true-termination.c below 1 FAIL0.422
n.c11_true-unreach-call.c below 3 FAIL0.445
n.c24_false-unreach-call.c below 3 OKAY2.851
n.c40_true-unreach-call.c below 1 FAIL0.37
nec11_false-unreach-call.c below 1 OKAY0.355
nec20_false-unreach-call.c below 1 OKAY0.389
nec40_true-unreach-call.c below 1 FAIL0.358
string_false-unreach-call.c below 1 OKAY0.596
string_true-unreach-call.c below 1 FAIL0.616
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.605
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.334
sum01_false-unreach-call_true-termination.c below 1 OKAY0.457
sum01_true-unreach-call_true-termination.c below 1 PASS0.362
sum03_false-unreach-call_true-termination.c below 1 OKAY0.494
sum03_true-unreach-call_false-termination.c below 1 PASS0.423
sum04_false-unreach-call_true-termination.c below 1 OKAY0.472
sum04_true-unreach-call_true-termination.c below 1 PASS0.357
sum_array_false-unreach-call.c below 1 OKAY0.59
sum_array_true-unreach-call.c below 1 FAIL0.679
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.32
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.46
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.36
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.338
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.388
trex01_false-unreach-call_true-termination.c below 3 OKAY0.455
trex01_true-unreach-call.c below 3 PASS0.73
trex02_false-unreach-call_true-termination.c below 3 OKAY0.418
trex02_true-unreach-call_true-termination.c below 3 PASS0.417
trex03_false-unreach-call_true-termination.c below 3 OKAY0.676
trex03_true-unreach-call.c below 3 PASS0.675
trex04_true-unreach-call_false-termination.c below 1 PASS0.378
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.343
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.969
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.372
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.359
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY4.566
vogal_false-unreach-call.c below 1 OKAY0.775
vogal_true-unreach-call.c below 1 FAIL0.741
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.313
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.319
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.305
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 132.64
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.938
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.929
Ackermann03_true-unreach-call.c below 7 FAIL0.967
Ackermann04_true-unreach-call.c below 7 FAIL0.958
Addition01_true-unreach-call_true-termination.c below 2 PASS0.551
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.521
Addition03_false-no-overflow.c below 2 PASS0.536
Addition03_true-unreach-call.c below 2 PASS0.547
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.468
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.42
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.397
Fibonacci01_true-unreach-call.c below 7 FAIL0.675
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.745
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.696
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.678
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.719
gcd01_true-unreach-call_true-termination.c below 2 PASS0.533
gcd02_true-unreach-call.c below 2 FAIL0.927
McCarthy91_false-unreach-call_false-termination.c below TIMEOUT 300.005
McCarthy91_true-unreach-call.c below TIMEOUT 300.006
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.54
Primes_true-unreach-call.c below 3 FAIL1.383
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.732
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.384
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.374
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 6/7
ICRA Time = 616.629
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.42
afterrec_2calls_true-unreach-call.c below 2 PASS0.397
afterrec_false-unreach-call.c below 2 OKAY0.373
afterrec_true-unreach-call.c below 2 PASS0.366
fibo_10_false-unreach-call.c below 7 OKAY0.686
fibo_10_true-unreach-call.c below 7 FAIL0.688
fibo_15_false-unreach-call.c below 7 OKAY0.672
fibo_15_true-unreach-call.c below 7 FAIL0.65
fibo_20_false-unreach-call.c below 7 OKAY0.664
fibo_20_true-unreach-call.c below 7 FAIL0.658
fibo_25_false-unreach-call.c below 7 OKAY0.67
fibo_25_true-unreach-call.c below 7 FAIL0.676
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.004
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.015
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.013
fibo_5_false-unreach-call.c below 7 OKAY0.699
fibo_5_true-unreach-call.c below 7 FAIL0.669
fibo_7_false-unreach-call.c below 7 OKAY0.671
fibo_7_true-unreach-call.c below 7 FAIL0.688
id2_b2_o3_true-unreach-call.c below 2 PASS0.624
id2_b3_o2_false-unreach-call.c below 2 OKAY0.655
id2_b3_o5_true-unreach-call.c below 2 PASS0.633
id2_b5_o10_true-unreach-call.c below 2 PASS0.605
id2_i5_o5_false-unreach-call.c below 2 OKAY0.414
id2_i5_o5_true-unreach-call.c below 2 PASS0.41
id_b2_o3_true-unreach-call.c below 2 PASS0.509
id_b3_o2_false-unreach-call.c below 2 OKAY0.55
id_b3_o5_true-unreach-call.c below 2 PASS0.552
id_b5_o10_true-unreach-call.c below 2 PASS0.55
id_i10_o10_false-unreach-call.c below 2 OKAY0.38
id_i10_o10_true-unreach-call.c below 2 PASS0.375
id_i15_o15_false-unreach-call.c below 2 OKAY0.379
id_i15_o15_true-unreach-call.c below 2 PASS0.386
id_i20_o20_false-unreach-call.c below 2 OKAY0.38
id_i20_o20_true-unreach-call.c below 2 PASS0.392
id_i25_o25_false-unreach-call.c below 2 OKAY0.363
id_i25_o25_true-unreach-call.c below 2 PASS0.379
id_i5_o5_false-unreach-call.c below 2 OKAY0.377
id_i5_o5_true-unreach-call.c below 2 PASS0.374
id_o1000_false-unreach-call.c below 2 OKAY0.38
id_o100_false-unreach-call.c below 2 OKAY0.386
id_o10_false-unreach-call.c below 2 OKAY0.393
id_o200_false-unreach-call.c below 2 OKAY0.366
id_o20_false-unreach-call.c below 2 OKAY0.385
id_o3_false-unreach-call.c below 2 OKAY0.389
sum_10x0_false-unreach-call.c below 2 OKAY0.411
sum_10x0_true-unreach-call.c below 2 PASS0.428
sum_15x0_false-unreach-call.c below 2 OKAY0.425
sum_15x0_true-unreach-call.c below 2 PASS0.42
sum_20x0_false-unreach-call.c below 2 OKAY0.422
sum_20x0_true-unreach-call.c below 2 PASS0.418
sum_25x0_false-unreach-call.c below 2 OKAY0.425
sum_25x0_true-unreach-call.c below 2 PASS0.404
sum_2x3_false-unreach-call.c below 2 OKAY0.416
sum_2x3_true-unreach-call.c below 2 PASS0.438
sum_non_eq_false-unreach-call.c below 2 OKAY0.428
sum_non_eq_true-unreach-call.c below 2 PASS0.41
sum_non_false-unreach-call.c below 2 OKAY0.425
sum_non_true-unreach-call.c below 2 PASS0.411
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5427.321
/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.434
rec-bhmr2007_true-unreach-call.c below 2 PASS0.419
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.636
rec-cggmp2005_true-unreach-call.c below 2 PASS0.397
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.399
rec-css2003_true-unreach-call.c below 2 PASS0.951
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.081
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.786
rec-gj2007b_true-unreach-call.c below 2 FAIL0.378
rec-gj2007_true-unreach-call.c below 2 FAIL0.476
rec-gr2006_true-unreach-call.c below 2 FAIL0.484
rec-gsv2008_true-unreach-call.c below 2 PASS0.454
rec-hhk2008_true-unreach-call.c below 2 PASS0.392
rec-jm2006_true-unreach-call.c below 2 PASS0.46
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.48
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.408
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.635
/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.348
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.38
rec-count_by_2_true-unreach-call.c below 2 PASS0.379
rec-count_by_k_true-unreach-call.c below 2 PASS0.404
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.383
rec-gauss_sum_true-unreach-call.c below 2 PASS0.436
rec-half_true-unreach-call.c below 2 PASS0.397
rec-nested_true-unreach-call.c below 3 FAIL0.525
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.252
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.486
cubic_polynomial_unsafe.c below 2 OKAY0.537
edit_distance_bottom_up.c below 3 FAIL134.159
edit_distance_top_down.c below 3 FAIL2.843
log_log_n_solution.c below 3 FAIL0.431
log_log_n_solution_unsafe.c below 3 OKAY0.433
log_n_solution.c below 2 FAIL0.476
log_n_solution_unsafe.c below 2 OKAY0.444
multivariate_1.c below TIMEOUT 300.098
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL7.888
multivariate_higher_order_unsafe.c below 7 OKAY7.904
n_cubed_solution.c below EXCEPTION 45.75
n_cubed_solution_unsafe.c below EXCEPTION 0.023
n_log_n_solution.c below 10 FAIL4.477
n_log_n_solution_unsafe.c below 10 OKAY4.517
n_squared_two_base_case_even.c below 2 PASS0.479
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.483
n_squared_two_base_case_odd.c below 2 PASS0.473
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.494
pascals_dynamic.c below 3 FAIL2.661
pascals_dynamic_unsafe.c below 3 OKAY2.648
pascals_iterative.c below 1 FAIL3.634
pascals_iterative_unsafe.c below 1 OKAY3.759
pascals_recursive.c below 8 FAIL2.435
pascals_recursive_unsafe.c below 8 OKAY2.418
squared_solution.c below TIMEOUT 300.008
squared_solution_unsafe.c below TIMEOUT 300.004
two_n_even.c below 2 PASS0.391
two_n_even_unsafe.c below 2 OKAY0.413
two_n_odd.c below 2 PASS0.404
two_n_odd_unsafe.c below 2 OKAY0.4
two_to_n_over_two_even.c below TIMEOUT 300.005
two_to_n_over_two_even_unsafe.c below 8 OKAY296.943
two_to_n_over_two_odd.c below TIMEOUT 300.005
two_to_n_over_two_odd_unsafe.c below TIMEOUT 300.005
two_to_n_squared.c below 8 EXCEPTION 17.941
two_to_n_squared_unsafe.c below 8 EXCEPTION 17.87
two_to_two_to_n.c below 7 FAIL0.877
two_to_two_to_n_unsafe.c below 7 OKAY0.879
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 14/19
ICRA Time = 2666.1
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.35
adding_and_mult_unsafe.c below 1 OKAY0.379
binary_search_array_tree.c below 1 FAIL0.694
exp_add_linear.c below 1 PASS0.44
exp_add_linear_unsafe.c below 1 OKAY0.437
exp_add_loop_rec.c below 1 FAIL0.374
exp_add_loop_rec_unsafe.c below 1 OKAY0.368
exp_add_loop_variable.c below 1 PASS0.428
exp_add_loop_variable_unsafe.c below 1 OKAY0.425
exp_with_linear_inner_loop.c below 1 FAIL0.485
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.487
halving_log1.c below 1 FAIL0.532
linear_two_to_n.c below 8 FAIL1.138
linear_two_to_n_unsafe.c below 8 OKAY1.148
loop_five_to_n.c below 1 PASS0.407
loop_five_to_n_unsafe.c below 1 OKAY0.438
non_loop_five_to_n.c below TIMEOUT 300.037
non_loop_five_to_n_unsafe.c below TIMEOUT 300.038
power_log.c below 1 PASS0.569
power_log_modified.c below 1 PASS0.601
simple_exponential.c below 1 PASS0.448
simple_exponential_for.c below 1 PASS0.49
simple_exponential_for_unsafe.c below 1 OKAY0.496
simple_exponential_unsafe.c below 1 OKAY0.47
two_to_n_minus_n.c below 7 FAIL1.426
two_to_n_minus_n_loop.c below 7 FAIL1.67
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.71
two_to_n_minus_n_unsafe.c below 7 OKAY1.224
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 617.709
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.558
02.c below 3 FAIL0.685
03.c below 1 PASS0.428
04.c below 1 PASS0.355
05.c below 3 PASS0.999
06.c below 3 PASS12.744
07.c below 3 PASS0.538
08.c below 3 PASS1.037
09.c below 3 PASS0.639
10.c below 3 FAIL0.849
11.c below 1 PASS0.347
12.c below 3 PASS1.154
13.c below 3 PASS0.502
14.c below 3 PASS0.428
15.c below 1 PASS0.362
16.c below 1 PASS0.421
17.c below EXCEPTION 0.382
18.c below 1 PASS0.409
19.c below 1 PASS0.433
20.c below 3 FAIL0.569
21.c below 3 PASS0.479
22.c below 3 FAIL0.955
23.c below 1 PASS0.374
24.c below 1 PASS0.382
25.c below 3 FAIL1.167
26.c below TIMEOUT 300.008
27.c below 1 PASS0.415
28.c below 3 PASS0.478
29.c below EXCEPTION 0.405
30.c below 1 PASS0.368
31.c below 3 PASS0.767
32.c below 1 FAIL0.374
33.c below 3 PASS1.075
34.c below 1 FAIL0.387
35.c below 1 PASS0.33
36.c below 3 PASS2.335
37.c below 3 FAIL0.47
38.c below 1 FAIL0.404
39.c below 3 PASS0.438
40.c below 3 PASS0.66
41.c below 1 PASS0.397
42.c below 3 PASS0.799
43.c below 3 PASS0.416
44.c below 1 PASS0.351
45.c below 3 FAIL2.427
46.c below 3 FAIL1.967
ICRA Assertions (True) = 32/46
ICRA Assertions (False) = 0/0
ICRA Time = 342.467
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.403
AGHKTW2017_foo.c below 1 PASS0.388
AGHKTW2017_loginSafe.c below 1 PASS0.783
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.448
BCK2011_gauss.c below 1 PASS0.435
BCK2011_strength_reduction.c below 1 PASS0.416
BCK2011_strength_reduction_linear.c below 1 PASS0.435
fibonacci_information_flow.c below 1 PASS0.552
TA2005_fib2.c below 1 PASS0.543
TA2005_fib.c below 1 PASS0.459
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.862