[Version Information]
WALi-OpenNWA version: 0f994ef6a5cbe02200899575605ae35f227d9ddb (2017-07-12 11:45:09 -0500) "Added programs and files used for POPL18"
duet version: 0bb65ddfee3d65b76cb927b278e492b410b1c720 (2017-08-06 18:12:28 -0400) "Merge remote-tracking branch 'origin/ark2' into Newton-ark2"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.5.3  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
camlp4               4.02+7  Camlp4 is a system for writing extensible parsers f
cil                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
conf-which                1  Virtual package relying on which
cppo                  1.4.1  Equivalent of the C preprocessor for OCaml programs
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170101  LR(1) parser generator
mlgmpidl              1.2.4  OCaml interface to the GMP library
num                       0  The Num library for arbitrary-precision integer and
oasis                 0.4.8  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.1  A library manager for OCaml
ocamlgraph            1.8.7  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.8  Generate OCaml modules from source files
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.374
kmp.c below 1 PASS1.133
qsort.c below 4 PASS0.993
speed_pldi09_fig1.c below 1 PASS0.489
speed_pldi09_fig4_2.c below 1 FAIL0.4
speed_pldi09_fig4_4.c below 1 PASS4.748
speed_pldi09_fig4_5.c below 1 PASS0.404
speed_pldi10_ex1.c below 1 PASS1.752
speed_pldi10_ex3.c below 1 PASS0.521
speed_pldi10_ex4.c below 1 PASS0.537
speed_popl10_fig2_1.c below 1 PASS0.483
speed_popl10_fig2_2.c below 1 FAIL0.383
speed_popl10_nested_multiple.c below 1 PASS0.461
speed_popl10_nested_single.c below 1 PASS0.435
speed_popl10_sequential_single.c below 1 PASS0.399
speed_popl10_simple_multiple.c below 1 PASS0.51
speed_popl10_simple_single_2.c below 1 PASS0.608
speed_popl10_simple_single.c below 1 PASS0.354
t07.c below 1 PASS0.414
t08.c below 1 PASS0.369
t09.c below 1 PASS0.411
t10.c below 1 PASS0.374
t11.c below 1 PASS0.481
t13.c below 1 FAIL0.445
t15.c below 1 PASS0.43
t16.c below 1 PASS0.371
t19.c below 1 PASS0.388
t20.c below 1 PASS0.379
t27.c below 1 PASS0.553
t28.c below 1 PASS0.467
t30.c below 1 FAIL0.404
t37.c below 2 PASS0.608
t39.c below 2 PASS0.531
t46.c below 1 PASS0.428
t47.c below 1 FAIL0.558
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.595
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.377
qsort_full.c below 4 PASS11.06
rec1-param_safe.c below 2 PASS0.379
rec1-param_unsafe.c below 2 OKAY0.388
rec1_safe.c below 2 PASS0.345
rec1_unsafe.c below 2 OKAY0.354
rec2-param_safe.c below 2 PASS0.37
rec2-param_unsafe.c below 2 OKAY0.354
rec2_safe.c below 2 PASS0.365
rec2_unsafe.c below 2 OKAY0.357
rec-test.c below 2 PASS0.368
sas03_bothbranches.c below 7 PASS0.875
sas03.c below 2 PASS0.739
simulated_lese_recursive.c below 2 PASS0.445
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 16.776
/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.333
divide.c below 1 PASS0.335
factor_unsafe.c below 1 OKAY0.322
for_infinite_loop_1_safe.c below 1 PASS0.316
for_infinite_loop_2_safe.c below 1 PASS0.309
interproc.c below 1 PASS0.31
mult.c below 1 PASS0.346
pointer_arith.c below 1 PASS0.303
quotient.c below 3 PASS0.489
subtract.c below 1 PASS0.327
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.334
sum01_bug02_unsafe.c below 1 OKAY0.611
sum01_real_safe.c below 1 PASS0.329
sum01_safe.c below 1 PASS0.341
sum01_unsafe.c below 1 OKAY0.463
sum02_safe.c below 1 PASS0.368
sum03_safe.c below 1 PASS0.403
sum03_unsafe.c below 1 OKAY0.506
sum04_safe.c below 1 PASS0.343
sum04_unsafe.c below 1 OKAY0.473
terminator_02_safe.c below 1 PASS0.343
terminator_02_unsafe.c below 1 OKAY0.361
terminator_03_safe.c below 1 PASS0.326
terminator_03_unsafe.c below 1 OKAY0.335
token_ring01_safe.c below 4 FAIL202.647
token_ring01_unsafe.c below 4 TIMEOUT 300.004
toy_safe.c below EXCEPTION 161.465
trex01_safe.c below 1 PASS0.739
trex01_unsafe.c below 1 OKAY0.373
trex02_safe2.c below 3 PASS0.419
trex02_safe.c below 3 PASS0.408
trex02_unsafe.c below 3 OKAY0.434
trex03_safe.c below 1 PASS0.459
trex03_unsafe.c below 1 OKAY0.445
trex04_safe.c below 1 PASS0.354
while_infinite_loop_1_safe.c below 1 PASS0.321
while_infinite_loop_2_safe.c below 1 PASS0.309
while_infinite_loop_3_safe.c below 1 PASS0.317
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 677.951
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.408
blogger_simplified1.c below 3 PASS1.196
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.388
mult-proc-params.c below 3 PASS0.41
popall.c below 1 PASS0.683
simulated_scc.c below 1 PASS0.653
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.742
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.368
degree2_binomial.c below 1 FAIL0.867
degree2_monomial.c below 1 PASS0.41
degree3_binomial.c below 1 FAIL1.985
degree3_monomial.c below 1 PASS0.466
degree4_binomial.c below 1 FAIL8.12
degree4_monomial.c below 1 PASS0.535
degree5_binomial.c below 1 FAIL188.824
degree5_monomial.c below 1 PASS0.654
ICRA Assertions (True) = 5/9
ICRA Assertions (False) = 0/0
ICRA Time = 202.229
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.473
cubic_with_square_interproc.c below 2 PASS0.618
cubic_with_square_nonlinear.c below 1 FAIL0.374
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.443
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.398
cubic_with_square_unsafe.c below 1 OKAY0.457
multi-input.c below 1 PASS0.48
multi-input_unsafe.c below 1 OKAY0.525
nondet_loop_bound.c below 1 FAIL0.367
nondet_loop_bound_quartic.c below 1 FAIL0.389
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.386
nondet_loop_bound_unsafe.c below 1 OKAY0.366
nonlinear_stratified.c below 1 TIMEOUT300.004
nonlinear_stratified_unsafe.c below 1 OKAY0.71
quartic_with_cube.c below 1 PASS0.607
quartic_with_cube_nonlinear.c below 1 FAIL0.391
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.389
quartic_with_cube_unsafe.c below 1 OKAY0.511
quintic_with_quartic.c below 1 PASS1.047
quintic_with_quartic_nonlinear.c below 1 PASS2.915
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.566
quintic_with_quartic_unsafe.c below 1 OKAY1.094
ICRA Assertions (True) = 6/12
ICRA Assertions (False) = 10/10
ICRA Time = 313.51
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.705
degree2_FD_AllAux_AllAssm.c below 1 PASS102.497
degree2_FD_AllAux_FewAssm.c below 1 PASS6.893
degree2_FD_FewAux_FewAssm.c below 1 PASS0.994
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.011
degree3.c below 1 PASS0.772
degree3_FD.c below 1 PASS0.949
degree4.c below 1 PASS0.461
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 114.282
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.437
loop_unsafe.c below 1 OKAY0.449
simulated_lese_parser.c below 1 PASS0.346
simulated_lese_sentinel.c below 1 PASS0.361
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.593
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.358
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.358
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below EXCEPTION 113.371
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 113.371
/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.37
array_false-unreach-call3.c below 1 OKAY0.349
array_true-unreach-call1.c below 1 FAIL0.342
array_true-unreach-call2.c below 1 FAIL0.373
array_true-unreach-call3.c below 1 PASS0.341
array_true-unreach-call4.c below 1 FAIL0.342
const_false-unreach-call1.c below 1 OKAY0.36
const_true-unreach-call1.c below 1 PASS0.347
diamond_false-unreach-call1.c below 1 OKAY0.348
diamond_true-unreach-call1.c below 1 PASS0.347
diamond_true-unreach-call2.c below 1 PASS0.37
functions_false-unreach-call1.c below 3 OKAY0.383
functions_true-unreach-call1.c below 3 PASS0.383
multivar_false-unreach-call1.c below 1 OKAY0.353
multivar_true-unreach-call1.c below 1 PASS0.361
nested_false-unreach-call1.c below 1 OKAY0.37
nested_true-unreach-call1.c below 1 PASS0.388
overflow_true-unreach-call1.c below 1 PASS0.32
phases_false-unreach-call1.c below 1 OKAY0.422
phases_false-unreach-call2.c below 1 OKAY0.365
phases_true-unreach-call1.c below 1 PASS0.403
phases_true-unreach-call2.c below 1 PASS0.35
simple_false-unreach-call1.c below 1 OKAY0.328
simple_false-unreach-call2.c below 1 OKAY0.32
simple_false-unreach-call3.c below 1 OKAY0.325
simple_false-unreach-call4.c below 1 OKAY0.33
simple_true-unreach-call1.c below 1 PASS0.315
simple_true-unreach-call2.c below 1 PASS0.327
simple_true-unreach-call3.c below 1 PASS0.335
simple_true-unreach-call4.c below 1 PASS0.323
underapprox_false-unreach-call1.c below 1 OKAY0.337
underapprox_false-unreach-call2.c below 1 OKAY0.342
underapprox_true-unreach-call1.c below 1 FAIL0.365
underapprox_true-unreach-call2.c below 1 PASS0.336
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.318
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.833
apache-get-tag_true-unreach-call.c below 1 FAIL0.436
down_true-unreach-call.c below 1 PASS0.354
fragtest_simple_true-unreach-call.c below 1 PASS0.444
half_2_true-unreach-call.c below 1 PASS0.388
heapsort_true-unreach-call.c below 1 PASS3.3
id_build_true-unreach-call.c below 1 PASS0.359
id_trans_false-unreach-call.c below 1 OKAY0.332
large_const_true-unreach-call.c below 1 PASS0.425
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.376
nested6_true-unreach-call.c below 1 FAIL0.525
nested9_true-unreach-call.c below 1 PASS0.555
nest-if3_true-unreach-call.c below 1 PASS0.489
NetBSD_loop_true-unreach-call.c below 1 PASS0.348
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.381
seq_true-unreach-call.c below 1 PASS0.418
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.436
string_concat-noarr_true-unreach-call.c below 1 PASS0.389
up_true-unreach-call.c below 1 PASS0.379
ICRA Assertions (True) = 15/18
ICRA Assertions (False) = 1/1
ICRA Time = 12.167
/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.4
cggmp2005b_true-unreach-call.c below 1 PASS0.483
cggmp2005_true-unreach-call.c below 1 PASS0.348
cggmp2005_variant_true-unreach-call.c below 1 PASS0.358
css2003_true-unreach-call.c below 1 PASS0.782
ddlm2013_true-unreach-call.c below 1 PASS0.529
gcnr2008_false-unreach-call.c below 1 OKAY0.985
gj2007b_true-unreach-call.c below 1 FAIL0.367
gj2007_true-unreach-call.c below 1 PASS0.424
gr2006_true-unreach-call.c below 1 PASS0.417
gsv2008_true-unreach-call.c below 1 PASS0.347
hhk2008_true-unreach-call.c below 1 PASS0.345
jm2006_true-unreach-call.c below 1 PASS0.424
jm2006_variant_true-unreach-call.c below 1 PASS0.473
mcmillan2006_true-unreach-call.c below 1 FAIL0.376
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.435
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.33
count_by_1_variant_true-unreach-call.c below 1 PASS0.403
count_by_2_true-unreach-call.c below 1 PASS0.335
count_by_k_true-unreach-call.c below 1 PASS0.344
count_by_nondet_true-unreach-call.c below 1 FAIL0.352
gauss_sum_true-unreach-call.c below 1 PASS0.393
half_true-unreach-call.c below 1 FAIL0.37
nested_true-unreach-call.c below 1 PASS0.437
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.964
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.404
array_true-unreach-call.c below 1 FAIL0.396
bubble_sort_false-unreach-call.c below 4 OKAY71.918
bubble_sort_true-unreach-call.c below 1 PASS5.186
compact_false-unreach-call.c below 1 OKAY0.391
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.348
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.343
eureka_01_false-unreach-call.c below 1 OKAY2.296
eureka_01_true-unreach-call.c below 1 FAIL1.628
eureka_05_true-unreach-call.c below 1 FAIL0.769
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.339
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.322
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.316
heavy_false-unreach-call.c below 1 OKAY0.512
heavy_true-unreach-call.c below 1 PASS0.473
insertion_sort_false-unreach-call.c below 1 OKAY2.401
insertion_sort_true-unreach-call.c below 1 FAIL0.566
invert_string_false-unreach-call.c below 1 OKAY0.516
invert_string_true-unreach-call.c below 1 FAIL0.53
linear_sea.ch_true-unreach-call.c below 1 FAIL0.389
linear_search_false-unreach-call.c below 1 OKAY0.392
lu.cmp_true-unreach-call.c below 3 PASS63.757
ludcmp_false-unreach-call.c below 3 OKAY64.818
matrix_false-unreach-call_true-termination.c below 1 OKAY1.101
matrix_true-unreach-call_true-termination.c below 1 FAIL0.446
n.c11_true-unreach-call.c below 3 FAIL0.459
n.c24_false-unreach-call.c below 3 OKAY5.52
n.c40_true-unreach-call.c below 1 FAIL0.372
nec11_false-unreach-call.c below 1 OKAY0.364
nec20_false-unreach-call.c below 1 OKAY0.41
nec40_true-unreach-call.c below 1 FAIL0.371
string_false-unreach-call.c below 1 OKAY0.639
string_true-unreach-call.c below 1 FAIL0.638
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.606
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.434
sum01_true-unreach-call_true-termination.c below 1 PASS0.349
sum03_false-unreach-call_true-termination.c below 1 OKAY0.49
sum03_true-unreach-call_false-termination.c below 1 PASS0.45
sum04_false-unreach-call_true-termination.c below 1 OKAY0.488
sum04_true-unreach-call_true-termination.c below 1 PASS0.342
sum_array_false-unreach-call.c below 1 OKAY0.601
sum_array_true-unreach-call.c below 1 FAIL0.684
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.329
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.474
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.359
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.329
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.343
trex01_false-unreach-call_true-termination.c below 3 OKAY0.446
trex01_true-unreach-call.c below 3 PASS0.708
trex02_false-unreach-call_true-termination.c below 3 OKAY0.422
trex02_true-unreach-call_true-termination.c below 3 PASS0.417
trex03_false-unreach-call_true-termination.c below 3 OKAY0.688
trex03_true-unreach-call.c below 3 PASS0.669
trex04_true-unreach-call_false-termination.c below 1 PASS0.375
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.363
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS11.891
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.371
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.357
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY7.59
vogal_false-unreach-call.c below 1 OKAY0.806
vogal_true-unreach-call.c below 1 FAIL0.783
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.3
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.311
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 = 263.057
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.336
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.217
Ackermann03_true-unreach-call.c below 7 FAIL1.319
Ackermann04_true-unreach-call.c below 7 FAIL1.328
Addition01_true-unreach-call_true-termination.c below 2 PASS0.588
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.575
Addition03_false-no-overflow.c below 2 PASS0.584
Addition03_true-unreach-call.c below 2 PASS0.611
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.502
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.441
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.436
Fibonacci01_true-unreach-call.c below 7 FAIL0.826
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.826
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.827
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.835
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.841
gcd01_true-unreach-call_true-termination.c below 2 PASS0.575
gcd02_true-unreach-call.c below 2 FAIL1.138
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.944
McCarthy91_true-unreach-call.c below 7 FAIL0.977
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.576
Primes_true-unreach-call.c below 3 FAIL1.628
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL46.361
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.402
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.393
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 7/7
ICRA Time = 66.086
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.432
afterrec_2calls_true-unreach-call.c below 2 PASS0.409
afterrec_false-unreach-call.c below 2 OKAY0.377
afterrec_true-unreach-call.c below 2 PASS0.374
fibo_10_false-unreach-call.c below 7 OKAY0.835
fibo_10_true-unreach-call.c below 7 FAIL0.821
fibo_15_false-unreach-call.c below 7 OKAY0.805
fibo_15_true-unreach-call.c below 7 FAIL0.825
fibo_20_false-unreach-call.c below 7 OKAY0.831
fibo_20_true-unreach-call.c below 7 FAIL0.818
fibo_25_false-unreach-call.c below 7 OKAY0.861
fibo_25_true-unreach-call.c below 7 FAIL0.84
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.017
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.022
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.024
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.019
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.026
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.022
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.026
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.024
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.022
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.024
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.023
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.021
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.022
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.025
fibo_5_false-unreach-call.c below 7 OKAY0.87
fibo_5_true-unreach-call.c below 7 FAIL0.813
fibo_7_false-unreach-call.c below 7 OKAY0.843
fibo_7_true-unreach-call.c below 7 FAIL0.845
id2_b2_o3_true-unreach-call.c below 2 PASS0.725
id2_b3_o2_false-unreach-call.c below 2 OKAY0.783
id2_b3_o5_true-unreach-call.c below 2 PASS0.741
id2_b5_o10_true-unreach-call.c below 2 PASS0.712
id2_i5_o5_false-unreach-call.c below 2 OKAY0.431
id2_i5_o5_true-unreach-call.c below 2 PASS0.432
id_b2_o3_true-unreach-call.c below 2 PASS0.605
id_b3_o2_false-unreach-call.c below 2 OKAY0.618
id_b3_o5_true-unreach-call.c below 2 PASS0.629
id_b5_o10_true-unreach-call.c below 2 PASS0.619
id_i10_o10_false-unreach-call.c below 2 OKAY0.4
id_i10_o10_true-unreach-call.c below 2 PASS0.4
id_i15_o15_false-unreach-call.c below 2 OKAY0.417
id_i15_o15_true-unreach-call.c below 2 PASS0.392
id_i20_o20_false-unreach-call.c below 2 OKAY0.395
id_i20_o20_true-unreach-call.c below 2 PASS0.392
id_i25_o25_false-unreach-call.c below 2 OKAY0.447
id_i25_o25_true-unreach-call.c below 2 PASS0.411
id_i5_o5_false-unreach-call.c below 2 OKAY0.389
id_i5_o5_true-unreach-call.c below 2 PASS0.416
id_o1000_false-unreach-call.c below 2 OKAY0.394
id_o100_false-unreach-call.c below 2 OKAY0.389
id_o10_false-unreach-call.c below 2 OKAY0.402
id_o200_false-unreach-call.c below 2 OKAY0.404
id_o20_false-unreach-call.c below 2 OKAY0.403
id_o3_false-unreach-call.c below 2 OKAY0.399
sum_10x0_false-unreach-call.c below 2 OKAY0.428
sum_10x0_true-unreach-call.c below 2 PASS0.44
sum_15x0_false-unreach-call.c below 2 OKAY0.45
sum_15x0_true-unreach-call.c below 2 PASS0.425
sum_20x0_false-unreach-call.c below 2 OKAY0.443
sum_20x0_true-unreach-call.c below 2 PASS0.426
sum_25x0_false-unreach-call.c below 2 OKAY0.436
sum_25x0_true-unreach-call.c below 2 PASS0.423
sum_2x3_false-unreach-call.c below 2 OKAY0.429
sum_2x3_true-unreach-call.c below 2 PASS0.437
sum_non_eq_false-unreach-call.c below 2 OKAY0.442
sum_non_eq_true-unreach-call.c below 2 PASS0.433
sum_non_false-unreach-call.c below 2 OKAY0.427
sum_non_true-unreach-call.c below 2 PASS0.431
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5430.826
/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.421
rec-bhmr2007_true-unreach-call.c below 2 PASS0.44
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.687
rec-cggmp2005_true-unreach-call.c below 2 PASS0.38
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.414
rec-css2003_true-unreach-call.c below 2 PASS0.98
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.897
rec-gj2007b_true-unreach-call.c below 2 FAIL0.386
rec-gj2007_true-unreach-call.c below 2 FAIL0.489
rec-gr2006_true-unreach-call.c below 2 FAIL0.495
rec-gsv2008_true-unreach-call.c below 2 PASS0.422
rec-hhk2008_true-unreach-call.c below 2 PASS0.393
rec-jm2006_true-unreach-call.c below 2 PASS0.451
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.516
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.443
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 307.818
/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.377
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.393
rec-count_by_2_true-unreach-call.c below 2 PASS0.362
rec-count_by_k_true-unreach-call.c below 2 PASS0.38
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.408
rec-gauss_sum_true-unreach-call.c below 2 PASS0.432
rec-half_true-unreach-call.c below 2 FAIL0.416
rec-nested_true-unreach-call.c below 3 FAIL0.554
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.322
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.56
cubic_polynomial_unsafe.c below 2 OKAY0.588
edit_distance_bottom_up.c below 3 FAIL192.414
edit_distance_top_down.c below 3 FAIL4.483
log_log_n_solution.c below 3 FAIL0.477
log_log_n_solution_unsafe.c below 3 OKAY0.45
log_n_solution.c below 2 FAIL0.464
log_n_solution_unsafe.c below 2 OKAY0.473
multivariate_1.c below TIMEOUT 300.005
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below TIMEOUT 300.005
multivariate_higher_order_unsafe.c below TIMEOUT 300.005
n_cubed_solution.c below EXCEPTION 107.11
n_cubed_solution_unsafe.c below EXCEPTION 0.023
n_log_n_solution.c below 9 FAIL1.414
n_log_n_solution_unsafe.c below 9 OKAY1.422
n_squared_two_base_case_even.c below 2 PASS0.568
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.594
n_squared_two_base_case_odd.c below 2 PASS0.614
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.596
pascals_dynamic.c below 3 FAIL2.971
pascals_dynamic_unsafe.c below 3 OKAY2.997
pascals_iterative.c below 1 FAIL5.009
pascals_iterative_unsafe.c below 1 OKAY4.96
pascals_recursive.c below 8 FAIL5.242
pascals_recursive_unsafe.c below 8 OKAY5.379
squared_solution.c below 8 FAIL11.199
squared_solution_unsafe.c below 8 OKAY11.193
two_n_even.c below 2 PASS0.417
two_n_even_unsafe.c below 2 OKAY0.43
two_n_odd.c below 2 PASS0.428
two_n_odd_unsafe.c below 2 OKAY0.43
two_to_n_over_two_even.c below 7 FAIL1.059
two_to_n_over_two_even_unsafe.c below 7 OKAY1.054
two_to_n_over_two_odd.c below 7 FAIL1.061
two_to_n_over_two_odd_unsafe.c below 7 OKAY1.075
two_to_n_squared.c below 5 FAIL24.673
two_to_n_squared_unsafe.c below 5 OKAY25.349
two_to_two_to_n.c below 7 FAIL1.061
two_to_two_to_n_unsafe.c below 7 OKAY1.032
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 16/19
ICRA Time = 1619.29
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.361
adding_and_mult_unsafe.c below 1 OKAY0.363
binary_search_array_tree.c below 1 FAIL0.717
exp_add_linear.c below 1 PASS0.423
exp_add_linear_unsafe.c below 1 OKAY0.431
exp_add_loop_rec.c below 1 FAIL0.357
exp_add_loop_rec_unsafe.c below 1 OKAY0.374
exp_add_loop_variable.c below 1 PASS0.405
exp_add_loop_variable_unsafe.c below 1 OKAY0.417
exp_with_linear_inner_loop.c below 1 FAIL0.475
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.476
halving_log1.c below 1 FAIL0.509
linear_two_to_n.c below TIMEOUT 300.012
linear_two_to_n_unsafe.c below TIMEOUT 300.006
loop_five_to_n.c below 1 PASS0.381
loop_five_to_n_unsafe.c below 1 OKAY0.398
non_loop_five_to_n.c below TIMEOUT 300.032
non_loop_five_to_n_unsafe.c below TIMEOUT 300.031
power_log.c below 1 PASS0.49
power_log_modified.c below 1 PASS0.521
simple_exponential.c below 1 PASS0.402
simple_exponential_for.c below 1 PASS0.398
simple_exponential_for_unsafe.c below 1 OKAY0.385
simple_exponential_unsafe.c below 1 OKAY0.396
two_to_n_minus_n.c below 8 FAIL3.005
two_to_n_minus_n_loop.c below 8 FAIL4.764
two_to_n_minus_n_loop_unsafe.c below 8 OKAY4.745
two_to_n_minus_n_unsafe.c below 8 OKAY3.004
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 10/12
ICRA Time = 1224.278
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.534
02.c below 3 FAIL0.695
03.c below 1 PASS0.422
04.c below 1 PASS0.35
05.c below 3 PASS0.997
06.c below 3 PASS7.633
07.c below 3 PASS0.507
08.c below 3 PASS1.145
09.c below 3 PASS0.646
10.c below 3 FAIL0.882
11.c below 1 PASS0.35
12.c below 3 PASS1.172
13.c below 3 PASS0.518
14.c below 3 PASS0.423
15.c below 1 PASS0.339
16.c below 1 PASS0.407
17.c below 1 PASS0.469
18.c below 1 PASS0.396
19.c below 1 PASS0.442
20.c below 3 FAIL0.606
21.c below 3 PASS0.494
22.c below 3 FAIL0.684
23.c below 1 PASS0.363
24.c below 1 PASS0.379
25.c below 3 FAIL1.362
26.c below 3 PASS113.734
27.c below 1 PASS0.446
28.c below 3 PASS0.475
29.c below EXCEPTION 0.395
30.c below 1 PASS0.364
31.c below 3 PASS0.764
32.c below 1 FAIL0.365
33.c below 3 PASS1.294
34.c below 1 FAIL0.39
35.c below 1 PASS0.336
36.c below 3 PASS2.23
37.c below 3 FAIL0.473
38.c below 1 FAIL0.37
39.c below 3 PASS0.407
40.c below 3 PASS0.648
41.c below 1 PASS0.38
42.c below EXCEPTION 0.366
43.c below 3 PASS0.468
44.c below 1 PASS0.355
45.c below 3 FAIL3.093
46.c below 3 FAIL1.753
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 151.321
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.398
AGHKTW2017_foo.c below 1 PASS0.402
AGHKTW2017_loginSafe.c below 1 PASS0.787
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.456
BCK2011_gauss.c below 1 PASS0.419
BCK2011_strength_reduction.c below 1 PASS0.417
BCK2011_strength_reduction_linear.c below 1 PASS0.421
fibonacci_information_flow.c below 1 PASS0.544
TA2005_fib2.c below 1 PASS0.552
TA2005_fib.c below 1 PASS0.474
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.87