[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.361
kmp.c below 1 PASS1.773
qsort.c below 5 PASS0.926
speed_pldi09_fig1.c below 1 PASS0.515
speed_pldi09_fig4_2.c below 1 FAIL0.399
speed_pldi09_fig4_4.c below 1 PASS4.775
speed_pldi09_fig4_5.c below 1 PASS0.419
speed_pldi10_ex1.c below 1 PASS1.397
speed_pldi10_ex3.c below 1 PASS0.498
speed_pldi10_ex4.c below 1 PASS0.538
speed_popl10_fig2_1.c below 1 PASS0.446
speed_popl10_fig2_2.c below 1 FAIL0.363
speed_popl10_nested_multiple.c below 1 PASS0.449
speed_popl10_nested_single.c below 1 PASS0.432
speed_popl10_sequential_single.c below 1 PASS0.387
speed_popl10_simple_multiple.c below 1 PASS0.516
speed_popl10_simple_single_2.c below 1 PASS0.637
speed_popl10_simple_single.c below 1 PASS0.359
t07.c below 1 PASS0.424
t08.c below 1 PASS0.378
t09.c below 1 PASS0.4
t10.c below 1 PASS0.359
t11.c below 1 PASS0.463
t13.c below 1 FAIL0.41
t15.c below 1 PASS0.403
t16.c below 1 PASS0.394
t19.c below 1 PASS0.39
t20.c below 1 PASS0.368
t27.c below 1 PASS0.556
t28.c below 1 PASS0.469
t30.c below 1 FAIL0.43
t37.c below 2 PASS0.603
t39.c below 2 PASS0.526
t46.c below 1 PASS0.421
t47.c below 1 FAIL0.565
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.749
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.366
qsort_full.c below 4 PASS6.125
rec1-param_safe.c below 2 PASS0.382
rec1-param_unsafe.c below 2 OKAY0.395
rec1_safe.c below 2 PASS0.38
rec1_unsafe.c below 2 OKAY0.361
rec2-param_safe.c below 2 PASS0.372
rec2-param_unsafe.c below 2 OKAY0.365
rec2_safe.c below 2 PASS0.366
rec2_unsafe.c below 2 OKAY0.368
rec-test.c below 2 PASS0.374
sas03_bothbranches.c below 7 PASS0.7
sas03.c below 2 PASS0.725
simulated_lese_recursive.c below 2 PASS0.457
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.736
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.337
count_up_down_unsafe.c below 1 OKAY0.333
divide.c below 1 PASS0.337
factor_unsafe.c below 1 OKAY0.328
for_infinite_loop_1_safe.c below 1 PASS0.322
for_infinite_loop_2_safe.c below 1 PASS0.312
interproc.c below 1 PASS0.297
mult.c below 1 PASS0.326
pointer_arith.c below 1 PASS0.306
quotient.c below 3 PASS0.481
subtract.c below 1 PASS0.331
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.343
sum01_bug02_unsafe.c below 1 OKAY0.617
sum01_real_safe.c below 1 PASS0.334
sum01_safe.c below 1 PASS0.362
sum01_unsafe.c below 1 OKAY0.468
sum02_safe.c below 1 PASS0.365
sum03_safe.c below 1 PASS0.406
sum03_unsafe.c below 1 OKAY0.48
sum04_safe.c below 1 PASS0.373
sum04_unsafe.c below 1 OKAY0.467
terminator_02_safe.c below 1 PASS0.343
terminator_02_unsafe.c below 1 OKAY0.358
terminator_03_safe.c below 1 PASS0.32
terminator_03_unsafe.c below 1 OKAY0.338
token_ring01_safe.c below 4 FAIL97.911
token_ring01_unsafe.c below 4 OKAY248.79
toy_safe.c below EXCEPTION 167.164
trex01_safe.c below 1 PASS0.531
trex01_unsafe.c below 1 OKAY0.374
trex02_safe2.c below 3 PASS0.397
trex02_safe.c below 3 PASS0.394
trex02_unsafe.c below 3 OKAY0.4
trex03_safe.c below 1 PASS0.437
trex03_unsafe.c below 1 OKAY0.435
trex04_safe.c below 1 PASS0.35
while_infinite_loop_1_safe.c below 1 PASS0.307
while_infinite_loop_2_safe.c below 1 PASS0.307
while_infinite_loop_3_safe.c below 1 PASS0.308
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 527.389
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.38
blogger_simplified1.c below 3 PASS1.088
divided_difference2.c below TIMEOUT 300.008
mult-proc.c below 3 PASS0.37
mult-proc-params.c below 3 PASS0.388
popall.c below 1 PASS0.682
simulated_scc.c below 1 PASS0.63
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.546
/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 FAIL0.844
degree2_monomial.c below 1 PASS0.391
degree3_binomial.c below 1 FAIL1.388
degree3_monomial.c below 1 PASS0.458
degree4_binomial.c below 1 FAIL3.087
degree4_monomial.c below 1 PASS0.522
degree5_binomial.c below 1 FAIL9.336
degree5_monomial.c below 1 PASS0.559
ICRA Assertions (True) = 5/9
ICRA Assertions (False) = 0/0
ICRA Time = 16.946
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.466
cubic_with_square_interproc.c below 2 FAIL0.571
cubic_with_square_nonlinear.c below 1 FAIL0.382
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.424
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.38
cubic_with_square_unsafe.c below 1 OKAY0.441
multi-input.c below 1 PASS214.47
multi-input_unsafe.c below 1 OKAY0.542
nondet_loop_bound.c below 1 FAIL0.367
nondet_loop_bound_quartic.c below 1 FAIL0.385
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.388
nondet_loop_bound_unsafe.c below 1 OKAY0.357
nonlinear_stratified.c below 1 PASS79.989
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.005
quartic_with_cube.c below 1 PASS0.627
quartic_with_cube_nonlinear.c below 1 FAIL0.398
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.4
quartic_with_cube_unsafe.c below 1 OKAY0.508
quintic_with_quartic.c below 1 PASS1.016
quintic_with_quartic_nonlinear.c below 1 PASS0.423
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.433
quintic_with_quartic_unsafe.c below 1 OKAY1.037
ICRA Assertions (True) = 6/12
ICRA Assertions (False) = 9/10
ICRA Time = 604.009
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.69
degree2_FD_AllAux_AllAssm.c below 1 PASS217.115
degree2_FD_AllAux_FewAssm.c below 1 PASS5.024
degree2_FD_FewAux_FewAssm.c below 1 PASS0.914
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.925
degree3.c below 1 PASS0.668
degree3_FD.c below 1 PASS0.802
degree4.c below 1 PASS0.429
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 226.567
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.437
loop_unsafe.c below 1 OKAY0.445
simulated_lese_parser.c below 1 PASS0.344
simulated_lese_sentinel.c below 1 PASS0.348
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.574
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.335
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.335
/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.354
array_false-unreach-call2.c below 1 OKAY0.366
array_false-unreach-call3.c below 1 OKAY0.346
array_true-unreach-call1.c below 1 FAIL0.349
array_true-unreach-call2.c below 1 FAIL0.365
array_true-unreach-call3.c below 1 PASS0.353
array_true-unreach-call4.c below 1 FAIL0.352
const_false-unreach-call1.c below 1 OKAY0.346
const_true-unreach-call1.c below 1 PASS0.345
diamond_false-unreach-call1.c below 1 OKAY0.373
diamond_true-unreach-call1.c below 1 PASS0.356
diamond_true-unreach-call2.c below 1 PASS0.379
functions_false-unreach-call1.c below 3 OKAY0.396
functions_true-unreach-call1.c below 3 PASS0.371
multivar_false-unreach-call1.c below 1 OKAY0.374
multivar_true-unreach-call1.c below 1 PASS0.365
nested_false-unreach-call1.c below 1 OKAY0.377
nested_true-unreach-call1.c below 1 PASS0.366
overflow_true-unreach-call1.c below 1 PASS0.325
phases_false-unreach-call1.c below 1 OKAY0.425
phases_false-unreach-call2.c below 1 OKAY0.339
phases_true-unreach-call1.c below 1 PASS0.397
phases_true-unreach-call2.c below 1 PASS0.346
simple_false-unreach-call1.c below 1 OKAY0.326
simple_false-unreach-call2.c below 1 OKAY0.325
simple_false-unreach-call3.c below 1 OKAY0.32
simple_false-unreach-call4.c below 1 OKAY0.324
simple_true-unreach-call1.c below 1 PASS0.327
simple_true-unreach-call2.c below 1 PASS0.322
simple_true-unreach-call3.c below 1 PASS0.325
simple_true-unreach-call4.c below 1 PASS0.327
underapprox_false-unreach-call1.c below 1 OKAY0.352
underapprox_false-unreach-call2.c below 1 OKAY0.344
underapprox_true-unreach-call1.c below 1 FAIL0.352
underapprox_true-unreach-call2.c below 1 PASS0.348
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.357
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.829
apache-get-tag_true-unreach-call.c below 1 FAIL0.424
down_true-unreach-call.c below 1 PASS0.361
fragtest_simple_true-unreach-call.c below 1 PASS0.441
half_2_true-unreach-call.c below 1 PASS0.387
heapsort_true-unreach-call.c below 1 PASS1.312
id_build_true-unreach-call.c below 1 PASS0.362
id_trans_false-unreach-call.c below 1 OKAY0.337
large_const_true-unreach-call.c below 1 PASS0.424
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.369
nested6_true-unreach-call.c below 1 FAIL0.508
nested9_true-unreach-call.c below 1 PASS0.49
nest-if3_true-unreach-call.c below 1 PASS0.474
NetBSD_loop_true-unreach-call.c below 1 PASS0.343
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.395
seq_true-unreach-call.c below 1 PASS0.43
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.352
string_concat-noarr_true-unreach-call.c below 1 PASS0.401
up_true-unreach-call.c below 1 PASS0.37
ICRA Assertions (True) = 15/18
ICRA Assertions (False) = 1/1
ICRA Time = 10.009
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.377
bhmr2007_true-unreach-call.c below 1 PASS0.389
cggmp2005b_true-unreach-call.c below 1 PASS0.501
cggmp2005_true-unreach-call.c below 1 PASS0.356
cggmp2005_variant_true-unreach-call.c below 1 PASS0.358
css2003_true-unreach-call.c below 1 PASS0.797
ddlm2013_true-unreach-call.c below 1 PASS0.523
gcnr2008_false-unreach-call.c below 1 OKAY0.936
gj2007b_true-unreach-call.c below 1 FAIL0.395
gj2007_true-unreach-call.c below 1 PASS0.438
gr2006_true-unreach-call.c below 1 PASS0.438
gsv2008_true-unreach-call.c below 1 PASS0.353
hhk2008_true-unreach-call.c below 1 PASS0.337
jm2006_true-unreach-call.c below 1 PASS0.415
jm2006_variant_true-unreach-call.c below 1 PASS0.482
mcmillan2006_true-unreach-call.c below 1 FAIL0.395
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.49
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.329
count_by_1_variant_true-unreach-call.c below 1 PASS0.379
count_by_2_true-unreach-call.c below 1 PASS0.325
count_by_k_true-unreach-call.c below 1 PASS0.333
count_by_nondet_true-unreach-call.c below 1 FAIL0.347
gauss_sum_true-unreach-call.c below 1 PASS0.374
half_true-unreach-call.c below 1 FAIL0.376
nested_true-unreach-call.c below 1 PASS0.405
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.868
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.393
array_true-unreach-call.c below 1 FAIL0.388
bubble_sort_false-unreach-call.c below 4 OKAY50.935
bubble_sort_true-unreach-call.c below 1 PASS3.715
compact_false-unreach-call.c below 1 OKAY0.383
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.349
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.339
eureka_01_false-unreach-call.c below 1 OKAY2.12
eureka_01_true-unreach-call.c below 1 FAIL1.513
eureka_05_true-unreach-call.c below 1 FAIL0.659
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.343
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.329
heavy_false-unreach-call.c below 1 OKAY0.46
heavy_true-unreach-call.c below 1 PASS0.439
insertion_sort_false-unreach-call.c below 1 OKAY1.726
insertion_sort_true-unreach-call.c below 1 FAIL0.578
invert_string_false-unreach-call.c below 1 OKAY0.512
invert_string_true-unreach-call.c below 1 FAIL0.548
linear_sea.ch_true-unreach-call.c below 1 FAIL0.389
linear_search_false-unreach-call.c below 1 OKAY0.417
lu.cmp_true-unreach-call.c below 3 PASS17.605
ludcmp_false-unreach-call.c below 3 OKAY17.836
matrix_false-unreach-call_true-termination.c below 1 OKAY1.093
matrix_true-unreach-call_true-termination.c below 1 FAIL0.425
n.c11_true-unreach-call.c below 3 FAIL0.437
n.c24_false-unreach-call.c below 3 OKAY2.81
n.c40_true-unreach-call.c below 1 FAIL0.361
nec11_false-unreach-call.c below 1 OKAY0.346
nec20_false-unreach-call.c below 1 OKAY0.4
nec40_true-unreach-call.c below 1 FAIL0.378
string_false-unreach-call.c below 1 OKAY0.634
string_true-unreach-call.c below 1 FAIL0.611
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.593
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.351
sum01_false-unreach-call_true-termination.c below 1 OKAY0.456
sum01_true-unreach-call_true-termination.c below 1 PASS0.351
sum03_false-unreach-call_true-termination.c below 1 OKAY0.498
sum03_true-unreach-call_false-termination.c below 1 PASS0.433
sum04_false-unreach-call_true-termination.c below 1 OKAY0.469
sum04_true-unreach-call_true-termination.c below 1 PASS0.336
sum_array_false-unreach-call.c below 1 OKAY0.604
sum_array_true-unreach-call.c below 1 FAIL0.664
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.331
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.465
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.345
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.338
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.332
trex01_false-unreach-call_true-termination.c below 3 OKAY0.439
trex01_true-unreach-call.c below 3 PASS0.701
trex02_false-unreach-call_true-termination.c below 3 OKAY0.396
trex02_true-unreach-call_true-termination.c below 3 PASS0.402
trex03_false-unreach-call_true-termination.c below 3 OKAY0.659
trex03_true-unreach-call.c below 3 PASS0.66
trex04_true-unreach-call_false-termination.c below 1 PASS0.39
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.356
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS6.107
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.364
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.354
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY4.604
vogal_false-unreach-call.c below 1 OKAY0.778
vogal_true-unreach-call.c below 1 FAIL0.775
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.295
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.31
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.31
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.323
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 134.608
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.948
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.909
Ackermann03_true-unreach-call.c below 7 FAIL0.948
Ackermann04_true-unreach-call.c below 7 FAIL0.952
Addition01_true-unreach-call_true-termination.c below 2 PASS0.545
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.539
Addition03_false-no-overflow.c below 2 PASS0.539
Addition03_true-unreach-call.c below 2 PASS0.537
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.478
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.428
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.414
Fibonacci01_true-unreach-call.c below 7 FAIL0.672
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.67
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.673
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.685
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.674
gcd01_true-unreach-call_true-termination.c below 2 PASS0.552
gcd02_true-unreach-call.c below 2 FAIL0.932
McCarthy91_false-unreach-call_false-termination.c below TIMEOUT 300.007
McCarthy91_true-unreach-call.c below TIMEOUT 300.005
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.546
Primes_true-unreach-call.c below 3 FAIL1.394
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.814
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.374
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.389
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 6/7
ICRA Time = 616.624
/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.395
afterrec_false-unreach-call.c below 2 OKAY0.383
afterrec_true-unreach-call.c below 2 PASS0.379
fibo_10_false-unreach-call.c below 7 OKAY0.66
fibo_10_true-unreach-call.c below 7 FAIL0.673
fibo_15_false-unreach-call.c below 7 OKAY0.681
fibo_15_true-unreach-call.c below 7 FAIL0.691
fibo_20_false-unreach-call.c below 7 OKAY0.667
fibo_20_true-unreach-call.c below 7 FAIL0.688
fibo_25_false-unreach-call.c below 7 OKAY0.703
fibo_25_true-unreach-call.c below 7 FAIL0.656
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.014
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.014
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.01
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.01
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.007
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.015
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.676
fibo_5_true-unreach-call.c below 7 FAIL0.673
fibo_7_false-unreach-call.c below 7 OKAY0.67
fibo_7_true-unreach-call.c below 7 FAIL0.687
id2_b2_o3_true-unreach-call.c below 2 PASS0.626
id2_b3_o2_false-unreach-call.c below 2 OKAY0.675
id2_b3_o5_true-unreach-call.c below 2 PASS0.598
id2_b5_o10_true-unreach-call.c below 2 PASS0.611
id2_i5_o5_false-unreach-call.c below 2 OKAY0.422
id2_i5_o5_true-unreach-call.c below 2 PASS0.443
id_b2_o3_true-unreach-call.c below 2 PASS0.544
id_b3_o2_false-unreach-call.c below 2 OKAY0.561
id_b3_o5_true-unreach-call.c below 2 PASS0.528
id_b5_o10_true-unreach-call.c below 2 PASS0.546
id_i10_o10_false-unreach-call.c below 2 OKAY0.383
id_i10_o10_true-unreach-call.c below 2 PASS0.37
id_i15_o15_false-unreach-call.c below 2 OKAY0.383
id_i15_o15_true-unreach-call.c below 2 PASS0.378
id_i20_o20_false-unreach-call.c below 2 OKAY0.37
id_i20_o20_true-unreach-call.c below 2 PASS0.378
id_i25_o25_false-unreach-call.c below 2 OKAY0.381
id_i25_o25_true-unreach-call.c below 2 PASS0.401
id_i5_o5_false-unreach-call.c below 2 OKAY0.372
id_i5_o5_true-unreach-call.c below 2 PASS0.379
id_o1000_false-unreach-call.c below 2 OKAY0.376
id_o100_false-unreach-call.c below 2 OKAY0.383
id_o10_false-unreach-call.c below 2 OKAY0.375
id_o200_false-unreach-call.c below 2 OKAY0.378
id_o20_false-unreach-call.c below 2 OKAY0.384
id_o3_false-unreach-call.c below 2 OKAY0.38
sum_10x0_false-unreach-call.c below 2 OKAY0.421
sum_10x0_true-unreach-call.c below 2 PASS0.42
sum_15x0_false-unreach-call.c below 2 OKAY0.407
sum_15x0_true-unreach-call.c below 2 PASS0.413
sum_20x0_false-unreach-call.c below 2 OKAY0.414
sum_20x0_true-unreach-call.c below 2 PASS0.409
sum_25x0_false-unreach-call.c below 2 OKAY0.416
sum_25x0_true-unreach-call.c below 2 PASS0.412
sum_2x3_false-unreach-call.c below 2 OKAY0.452
sum_2x3_true-unreach-call.c below 2 PASS0.438
sum_non_eq_false-unreach-call.c below 2 OKAY0.413
sum_non_eq_true-unreach-call.c below 2 PASS0.433
sum_non_false-unreach-call.c below 2 OKAY0.437
sum_non_true-unreach-call.c below 2 PASS0.406
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5427.419
/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.429
rec-bhmr2007_true-unreach-call.c below 2 PASS0.42
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.679
rec-cggmp2005_true-unreach-call.c below 2 PASS0.397
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.413
rec-css2003_true-unreach-call.c below 2 PASS0.937
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.089
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.769
rec-gj2007b_true-unreach-call.c below 2 FAIL0.385
rec-gj2007_true-unreach-call.c below 2 FAIL0.476
rec-gr2006_true-unreach-call.c below 2 FAIL0.471
rec-gsv2008_true-unreach-call.c below 2 PASS0.442
rec-hhk2008_true-unreach-call.c below 2 PASS0.388
rec-jm2006_true-unreach-call.c below 2 PASS0.454
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.495
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.422
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.666
/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.37
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.398
rec-count_by_2_true-unreach-call.c below 2 PASS0.368
rec-count_by_k_true-unreach-call.c below 2 PASS0.377
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.38
rec-gauss_sum_true-unreach-call.c below 2 PASS0.447
rec-half_true-unreach-call.c below 2 PASS0.392
rec-nested_true-unreach-call.c below 3 FAIL0.511
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.243
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.521
cubic_polynomial_unsafe.c below 2 OKAY0.528
edit_distance_bottom_up.c below 3 FAIL132.328
edit_distance_top_down.c below 3 FAIL2.828
log_log_n_solution.c below 3 FAIL0.427
log_log_n_solution_unsafe.c below 3 OKAY0.426
log_n_solution.c below 2 FAIL0.448
log_n_solution_unsafe.c below 2 OKAY0.454
multivariate_1.c below TIMEOUT 300.093
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL7.974
multivariate_higher_order_unsafe.c below 7 OKAY7.887
n_cubed_solution.c below EXCEPTION 46.878
n_cubed_solution_unsafe.c below EXCEPTION 0.023
n_log_n_solution.c below 10 FAIL4.658
n_log_n_solution_unsafe.c below 10 OKAY4.544
n_squared_two_base_case_even.c below 2 PASS0.486
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.486
n_squared_two_base_case_odd.c below 2 PASS0.487
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.496
pascals_dynamic.c below 3 FAIL2.616
pascals_dynamic_unsafe.c below 3 OKAY2.597
pascals_iterative.c below 1 FAIL3.595
pascals_iterative_unsafe.c below 1 OKAY3.652
pascals_recursive.c below 8 FAIL2.411
pascals_recursive_unsafe.c below 8 OKAY2.434
squared_solution.c below TIMEOUT 300.008
squared_solution_unsafe.c below TIMEOUT 300.004
two_n_even.c below 2 PASS0.4
two_n_even_unsafe.c below 2 OKAY0.402
two_n_odd.c below 2 PASS0.411
two_n_odd_unsafe.c below 2 OKAY0.407
two_to_n_over_two_even.c below TIMEOUT 300.006
two_to_n_over_two_even_unsafe.c below TIMEOUT 300.005
two_to_n_over_two_odd.c below TIMEOUT 300.005
two_to_n_over_two_odd_unsafe.c below TIMEOUT 300.007
two_to_n_squared.c below 8 EXCEPTION 17.07
two_to_n_squared_unsafe.c below 8 EXCEPTION 16.846
two_to_two_to_n.c below 7 FAIL0.858
two_to_two_to_n_unsafe.c below 7 OKAY0.867
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 13/19
ICRA Time = 2666.579
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.353
adding_and_mult_unsafe.c below 1 OKAY0.35
binary_search_array_tree.c below 1 FAIL0.671
exp_add_linear.c below 1 PASS0.423
exp_add_linear_unsafe.c below 1 OKAY0.447
exp_add_loop_rec.c below 1 FAIL0.35
exp_add_loop_rec_unsafe.c below 1 OKAY0.375
exp_add_loop_variable.c below 1 PASS0.399
exp_add_loop_variable_unsafe.c below 1 OKAY0.394
exp_with_linear_inner_loop.c below 1 FAIL0.476
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.472
halving_log1.c below 1 FAIL0.491
linear_two_to_n.c below 8 FAIL1.051
linear_two_to_n_unsafe.c below 8 OKAY1.044
loop_five_to_n.c below 1 PASS0.377
loop_five_to_n_unsafe.c below 1 OKAY0.405
non_loop_five_to_n.c below TIMEOUT 300.037
non_loop_five_to_n_unsafe.c below TIMEOUT 300.04
power_log.c below 1 PASS0.48
power_log_modified.c below 1 PASS0.484
simple_exponential.c below 1 PASS0.383
simple_exponential_for.c below 1 PASS0.39
simple_exponential_for_unsafe.c below 1 OKAY0.39
simple_exponential_unsafe.c below 1 OKAY0.388
two_to_n_minus_n.c below 7 FAIL1.195
two_to_n_minus_n_loop.c below 7 FAIL1.73
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.696
two_to_n_minus_n_unsafe.c below 7 OKAY1.188
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 616.479
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.527
02.c below 3 FAIL0.661
03.c below 1 PASS0.413
04.c below 1 PASS0.339
05.c below 3 PASS0.951
06.c below 3 PASS12.383
07.c below 3 PASS0.503
08.c below 3 PASS1.021
09.c below 3 PASS0.631
10.c below 3 FAIL0.789
11.c below 1 PASS0.345
12.c below 3 PASS1.112
13.c below 3 PASS0.493
14.c below 3 PASS0.419
15.c below 1 PASS0.348
16.c below 1 PASS0.404
17.c below EXCEPTION 0.383
18.c below 1 PASS0.389
19.c below 1 PASS0.443
20.c below 3 FAIL0.581
21.c below 3 PASS0.464
22.c below 3 FAIL0.964
23.c below 1 PASS0.354
24.c below 1 PASS0.375
25.c below 3 FAIL1.126
26.c below TIMEOUT 300.004
27.c below 1 PASS0.429
28.c below 3 PASS0.481
29.c below EXCEPTION 0.389
30.c below 1 PASS0.408
31.c below 3 PASS0.807
32.c below 1 FAIL0.393
33.c below 3 PASS1.183
34.c below 1 FAIL0.397
35.c below 1 PASS0.349
36.c below 3 PASS2.323
37.c below 3 FAIL0.471
38.c below 1 FAIL0.373
39.c below 3 PASS0.419
40.c below 3 PASS0.681
41.c below 1 PASS0.384
42.c below 3 PASS0.782
43.c below 3 PASS0.454
44.c below 1 PASS0.37
45.c below 3 FAIL2.435
46.c below 3 FAIL2.16
ICRA Assertions (True) = 32/46
ICRA Assertions (False) = 0/0
ICRA Time = 342.11
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.524
AGHKTW2017_foo.c below 1 PASS0.548
AGHKTW2017_loginSafe.c below 1 PASS0.956
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.467
BCK2011_gauss.c below 1 PASS0.439
BCK2011_strength_reduction.c below 1 PASS0.401
BCK2011_strength_reduction_linear.c below 1 PASS0.439
fibonacci_information_flow.c below 1 PASS0.58
TA2005_fib2.c below 1 PASS0.539
TA2005_fib.c below 1 PASS0.476
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 5.369