[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.389
kmp.c below 1 PASS1.134
qsort.c below 4 PASS0.993
speed_pldi09_fig1.c below 1 PASS0.483
speed_pldi09_fig4_2.c below 1 FAIL0.397
speed_pldi09_fig4_4.c below 1 PASS4.77
speed_pldi09_fig4_5.c below 1 PASS0.387
speed_pldi10_ex1.c below 1 PASS1.739
speed_pldi10_ex3.c below 1 PASS0.551
speed_pldi10_ex4.c below 1 PASS0.515
speed_popl10_fig2_1.c below 1 PASS0.454
speed_popl10_fig2_2.c below 1 FAIL0.362
speed_popl10_nested_multiple.c below 1 PASS0.47
speed_popl10_nested_single.c below 1 PASS0.44
speed_popl10_sequential_single.c below 1 PASS0.387
speed_popl10_simple_multiple.c below 1 PASS0.513
speed_popl10_simple_single_2.c below 1 PASS0.635
speed_popl10_simple_single.c below 1 PASS0.363
t07.c below 1 PASS0.432
t08.c below 1 PASS0.387
t09.c below 1 PASS0.394
t10.c below 1 PASS0.358
t11.c below 1 PASS0.453
t13.c below 1 FAIL0.426
t15.c below 1 PASS0.418
t16.c below 1 PASS0.38
t19.c below 1 PASS0.402
t20.c below 1 PASS0.377
t27.c below 1 PASS0.574
t28.c below 1 PASS0.47
t30.c below 1 FAIL0.445
t37.c below 2 PASS0.618
t39.c below 2 PASS0.543
t46.c below 1 PASS0.408
t47.c below 1 FAIL0.566
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.633
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.398
qsort_full.c below 4 PASS11.114
rec1-param_safe.c below 2 PASS0.379
rec1-param_unsafe.c below 2 OKAY0.382
rec1_safe.c below 2 PASS0.357
rec1_unsafe.c below 2 OKAY0.375
rec2-param_safe.c below 2 PASS0.361
rec2-param_unsafe.c below 2 OKAY0.37
rec2_safe.c below 2 PASS0.356
rec2_unsafe.c below 2 OKAY0.364
rec-test.c below 2 PASS0.372
sas03_bothbranches.c below 7 PASS0.872
sas03.c below 2 PASS0.732
simulated_lese_recursive.c below 2 PASS0.458
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 16.89
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.327
count_up_down_unsafe.c below 1 OKAY0.337
divide.c below 1 PASS0.346
factor_unsafe.c below 1 OKAY0.33
for_infinite_loop_1_safe.c below 1 PASS0.325
for_infinite_loop_2_safe.c below 1 PASS0.31
interproc.c below 1 PASS0.305
mult.c below 1 PASS0.334
pointer_arith.c below 1 PASS0.296
quotient.c below 3 PASS0.512
subtract.c below 1 PASS0.331
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.337
sum01_bug02_unsafe.c below 1 OKAY0.641
sum01_real_safe.c below 1 PASS0.323
sum01_safe.c below 1 PASS0.356
sum01_unsafe.c below 1 OKAY0.458
sum02_safe.c below 1 PASS0.363
sum03_safe.c below 1 PASS0.395
sum03_unsafe.c below 1 OKAY0.488
sum04_safe.c below 1 PASS0.358
sum04_unsafe.c below 1 OKAY0.472
terminator_02_safe.c below 1 PASS0.322
terminator_02_unsafe.c below 1 OKAY0.376
terminator_03_safe.c below 1 PASS0.328
terminator_03_unsafe.c below 1 OKAY0.332
token_ring01_safe.c below 4 FAIL194.772
token_ring01_unsafe.c below 4 TIMEOUT 300.008
toy_safe.c below EXCEPTION 174.784
trex01_safe.c below 1 PASS0.745
trex01_unsafe.c below 1 OKAY0.378
trex02_safe2.c below 3 PASS0.416
trex02_safe.c below 3 PASS0.404
trex02_unsafe.c below 3 OKAY0.406
trex03_safe.c below 1 PASS0.448
trex03_unsafe.c below 1 OKAY0.434
trex04_safe.c below 1 PASS0.357
while_infinite_loop_1_safe.c below 1 PASS0.315
while_infinite_loop_2_safe.c below 1 PASS0.306
while_infinite_loop_3_safe.c below 1 PASS0.311
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 683.386
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.408
blogger_simplified1.c below 3 PASS1.166
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.377
mult-proc-params.c below 3 PASS0.402
popall.c below 1 PASS0.671
simulated_scc.c below 1 PASS0.639
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.668
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.355
degree2_binomial.c below 1 FAIL0.88
degree2_monomial.c below 1 PASS0.396
degree3_binomial.c below 1 FAIL2.008
degree3_monomial.c below 1 PASS0.467
degree4_binomial.c below 1 FAIL8.072
degree4_monomial.c below 1 PASS0.532
degree5_binomial.c below 1 FAIL188.961
degree5_monomial.c below 1 PASS0.674
ICRA Assertions (True) = 5/9
ICRA Assertions (False) = 0/0
ICRA Time = 202.345
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.465
cubic_with_square_interproc.c below 2 PASS0.611
cubic_with_square_nonlinear.c below 1 FAIL0.369
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.444
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.389
cubic_with_square_unsafe.c below 1 OKAY0.47
multi-input.c below 1 PASS0.493
multi-input_unsafe.c below 1 OKAY0.563
nondet_loop_bound.c below 1 FAIL0.352
nondet_loop_bound_quartic.c below 1 FAIL0.398
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.396
nondet_loop_bound_unsafe.c below 1 OKAY0.362
nonlinear_stratified.c below 1 TIMEOUT300.004
nonlinear_stratified_unsafe.c below 1 OKAY0.714
quartic_with_cube.c below 1 PASS0.599
quartic_with_cube_nonlinear.c below 1 FAIL0.377
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.406
quartic_with_cube_unsafe.c below 1 OKAY0.519
quintic_with_quartic.c below 1 PASS1.028
quintic_with_quartic_nonlinear.c below 1 PASS2.915
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.547
quintic_with_quartic_unsafe.c below 1 OKAY1.016
ICRA Assertions (True) = 6/12
ICRA Assertions (False) = 10/10
ICRA Time = 313.437
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.693
degree2_FD_AllAux_AllAssm.c below 1 PASS103.678
degree2_FD_AllAux_FewAssm.c below 1 PASS6.941
degree2_FD_FewAux_FewAssm.c below 1 PASS1.017
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.019
degree3.c below 1 PASS0.729
degree3_FD.c below 1 PASS0.913
degree4.c below 1 PASS0.465
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 115.455
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.427
loop_unsafe.c below 1 OKAY0.457
simulated_lese_parser.c below 1 PASS0.356
simulated_lese_sentinel.c below 1 PASS0.361
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.601
/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 107.285
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 107.285
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.364
array_false-unreach-call2.c below 1 OKAY0.376
array_false-unreach-call3.c below 1 OKAY0.352
array_true-unreach-call1.c below 1 FAIL0.356
array_true-unreach-call2.c below 1 FAIL0.372
array_true-unreach-call3.c below 1 PASS0.352
array_true-unreach-call4.c below 1 FAIL0.354
const_false-unreach-call1.c below 1 OKAY0.348
const_true-unreach-call1.c below 1 PASS0.34
diamond_false-unreach-call1.c below 1 OKAY0.343
diamond_true-unreach-call1.c below 1 PASS0.344
diamond_true-unreach-call2.c below 1 PASS0.373
functions_false-unreach-call1.c below 3 OKAY0.383
functions_true-unreach-call1.c below 3 PASS0.386
multivar_false-unreach-call1.c below 1 OKAY0.375
multivar_true-unreach-call1.c below 1 PASS0.347
nested_false-unreach-call1.c below 1 OKAY0.377
nested_true-unreach-call1.c below 1 PASS0.371
overflow_true-unreach-call1.c below 1 PASS0.316
phases_false-unreach-call1.c below 1 OKAY0.413
phases_false-unreach-call2.c below 1 OKAY0.352
phases_true-unreach-call1.c below 1 PASS0.398
phases_true-unreach-call2.c below 1 PASS0.343
simple_false-unreach-call1.c below 1 OKAY0.328
simple_false-unreach-call2.c below 1 OKAY0.319
simple_false-unreach-call3.c below 1 OKAY0.321
simple_false-unreach-call4.c below 1 OKAY0.323
simple_true-unreach-call1.c below 1 PASS0.324
simple_true-unreach-call2.c below 1 PASS0.323
simple_true-unreach-call3.c below 1 PASS0.331
simple_true-unreach-call4.c below 1 PASS0.336
underapprox_false-unreach-call1.c below 1 OKAY0.354
underapprox_false-unreach-call2.c below 1 OKAY0.35
underapprox_true-unreach-call1.c below 1 FAIL0.358
underapprox_true-unreach-call2.c below 1 PASS0.328
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.33
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.852
apache-get-tag_true-unreach-call.c below 1 FAIL0.45
down_true-unreach-call.c below 1 PASS0.368
fragtest_simple_true-unreach-call.c below 1 PASS0.448
half_2_true-unreach-call.c below 1 PASS0.387
heapsort_true-unreach-call.c below 1 PASS3.238
id_build_true-unreach-call.c below 1 PASS0.356
id_trans_false-unreach-call.c below 1 OKAY0.332
large_const_true-unreach-call.c below 1 PASS0.433
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.384
nested6_true-unreach-call.c below 1 FAIL0.536
nested9_true-unreach-call.c below 1 PASS0.543
nest-if3_true-unreach-call.c below 1 PASS0.496
NetBSD_loop_true-unreach-call.c below 1 PASS0.334
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.401
seq_true-unreach-call.c below 1 PASS0.449
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.487
string_concat-noarr_true-unreach-call.c below 1 PASS0.387
up_true-unreach-call.c below 1 PASS0.371
ICRA Assertions (True) = 15/18
ICRA Assertions (False) = 1/1
ICRA Time = 12.252
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.37
bhmr2007_true-unreach-call.c below 1 PASS0.37
cggmp2005b_true-unreach-call.c below 1 PASS0.481
cggmp2005_true-unreach-call.c below 1 PASS0.354
cggmp2005_variant_true-unreach-call.c below 1 PASS0.346
css2003_true-unreach-call.c below 1 PASS0.807
ddlm2013_true-unreach-call.c below 1 PASS0.516
gcnr2008_false-unreach-call.c below 1 OKAY0.991
gj2007b_true-unreach-call.c below 1 FAIL0.379
gj2007_true-unreach-call.c below 1 PASS0.452
gr2006_true-unreach-call.c below 1 PASS0.44
gsv2008_true-unreach-call.c below 1 PASS0.346
hhk2008_true-unreach-call.c below 1 PASS0.378
jm2006_true-unreach-call.c below 1 PASS0.414
jm2006_variant_true-unreach-call.c below 1 PASS0.477
mcmillan2006_true-unreach-call.c below 1 FAIL0.385
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.506
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.333
count_by_1_variant_true-unreach-call.c below 1 PASS0.412
count_by_2_true-unreach-call.c below 1 PASS0.324
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.384
half_true-unreach-call.c below 1 FAIL0.38
nested_true-unreach-call.c below 1 PASS0.42
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.929
/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.417
bubble_sort_false-unreach-call.c below 4 OKAY72.332
bubble_sort_true-unreach-call.c below 1 PASS5.405
compact_false-unreach-call.c below 1 OKAY0.389
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.342
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.345
eureka_01_false-unreach-call.c below 1 OKAY2.26
eureka_01_true-unreach-call.c below 1 FAIL1.6
eureka_05_true-unreach-call.c below 1 FAIL0.771
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.355
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.326
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.317
heavy_false-unreach-call.c below 1 OKAY0.496
heavy_true-unreach-call.c below 1 PASS0.49
insertion_sort_false-unreach-call.c below 1 OKAY2.434
insertion_sort_true-unreach-call.c below 1 FAIL0.588
invert_string_false-unreach-call.c below 1 OKAY0.518
invert_string_true-unreach-call.c below 1 FAIL0.543
linear_sea.ch_true-unreach-call.c below 1 FAIL0.38
linear_search_false-unreach-call.c below 1 OKAY0.39
lu.cmp_true-unreach-call.c below 3 PASS64.906
ludcmp_false-unreach-call.c below 3 OKAY66.263
matrix_false-unreach-call_true-termination.c below 1 OKAY1.123
matrix_true-unreach-call_true-termination.c below 1 FAIL0.448
n.c11_true-unreach-call.c below 3 FAIL0.462
n.c24_false-unreach-call.c below 3 OKAY5.433
n.c40_true-unreach-call.c below 1 FAIL0.366
nec11_false-unreach-call.c below 1 OKAY0.352
nec20_false-unreach-call.c below 1 OKAY0.379
nec40_true-unreach-call.c below 1 FAIL0.364
string_false-unreach-call.c below 1 OKAY0.649
string_true-unreach-call.c below 1 FAIL0.627
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.598
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.462
sum01_true-unreach-call_true-termination.c below 1 PASS0.352
sum03_false-unreach-call_true-termination.c below 1 OKAY0.505
sum03_true-unreach-call_false-termination.c below 1 PASS0.444
sum04_false-unreach-call_true-termination.c below 1 OKAY0.479
sum04_true-unreach-call_true-termination.c below 1 PASS0.346
sum_array_false-unreach-call.c below 1 OKAY0.591
sum_array_true-unreach-call.c below 1 FAIL0.701
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.335
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.459
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.351
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.342
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.329
trex01_false-unreach-call_true-termination.c below 3 OKAY0.46
trex01_true-unreach-call.c below 3 PASS0.72
trex02_false-unreach-call_true-termination.c below 3 OKAY0.412
trex02_true-unreach-call_true-termination.c below 3 PASS0.407
trex03_false-unreach-call_true-termination.c below 3 OKAY0.687
trex03_true-unreach-call.c below 3 PASS0.656
trex04_true-unreach-call_false-termination.c below 1 PASS0.401
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.357
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS11.756
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.382
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY7.639
vogal_false-unreach-call.c below 1 OKAY0.767
vogal_true-unreach-call.c below 1 FAIL0.791
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.328
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.314
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.327
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 266.206
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.295
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.254
Ackermann03_true-unreach-call.c below 7 FAIL1.311
Ackermann04_true-unreach-call.c below 7 FAIL1.284
Addition01_true-unreach-call_true-termination.c below 2 PASS0.585
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.592
Addition03_false-no-overflow.c below 2 PASS0.588
Addition03_true-unreach-call.c below 2 PASS0.575
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.509
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.45
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.442
Fibonacci01_true-unreach-call.c below 7 FAIL0.828
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.837
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.851
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.852
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.836
gcd01_true-unreach-call_true-termination.c below 2 PASS0.563
gcd02_true-unreach-call.c below 2 FAIL1.117
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.965
McCarthy91_true-unreach-call.c below 7 FAIL0.927
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.583
Primes_true-unreach-call.c below 3 FAIL1.598
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL46.272
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.402
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.409
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 7/7
ICRA Time = 65.925
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.416
afterrec_2calls_true-unreach-call.c below 2 PASS0.413
afterrec_false-unreach-call.c below 2 OKAY0.379
afterrec_true-unreach-call.c below 2 PASS0.359
fibo_10_false-unreach-call.c below 7 OKAY0.825
fibo_10_true-unreach-call.c below 7 FAIL0.834
fibo_15_false-unreach-call.c below 7 OKAY0.813
fibo_15_true-unreach-call.c below 7 FAIL0.856
fibo_20_false-unreach-call.c below 7 OKAY0.817
fibo_20_true-unreach-call.c below 7 FAIL0.825
fibo_25_false-unreach-call.c below 7 OKAY0.833
fibo_25_true-unreach-call.c below 7 FAIL0.837
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.022
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.018
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.022
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.022
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.023
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.023
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.025
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.025
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.022
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.023
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.023
fibo_5_false-unreach-call.c below 7 OKAY0.86
fibo_5_true-unreach-call.c below 7 FAIL0.827
fibo_7_false-unreach-call.c below 7 OKAY0.84
fibo_7_true-unreach-call.c below 7 FAIL0.837
id2_b2_o3_true-unreach-call.c below 2 PASS0.71
id2_b3_o2_false-unreach-call.c below 2 OKAY0.747
id2_b3_o5_true-unreach-call.c below 2 PASS0.712
id2_b5_o10_true-unreach-call.c below 2 PASS0.733
id2_i5_o5_false-unreach-call.c below 2 OKAY0.427
id2_i5_o5_true-unreach-call.c below 2 PASS0.422
id_b2_o3_true-unreach-call.c below 2 PASS0.603
id_b3_o2_false-unreach-call.c below 2 OKAY0.631
id_b3_o5_true-unreach-call.c below 2 PASS0.576
id_b5_o10_true-unreach-call.c below 2 PASS0.587
id_i10_o10_false-unreach-call.c below 2 OKAY0.403
id_i10_o10_true-unreach-call.c below 2 PASS0.38
id_i15_o15_false-unreach-call.c below 2 OKAY0.392
id_i15_o15_true-unreach-call.c below 2 PASS0.394
id_i20_o20_false-unreach-call.c below 2 OKAY0.41
id_i20_o20_true-unreach-call.c below 2 PASS0.39
id_i25_o25_false-unreach-call.c below 2 OKAY0.388
id_i25_o25_true-unreach-call.c below 2 PASS0.379
id_i5_o5_false-unreach-call.c below 2 OKAY0.4
id_i5_o5_true-unreach-call.c below 2 PASS0.384
id_o1000_false-unreach-call.c below 2 OKAY0.385
id_o100_false-unreach-call.c below 2 OKAY0.402
id_o10_false-unreach-call.c below 2 OKAY0.391
id_o200_false-unreach-call.c below 2 OKAY0.387
id_o20_false-unreach-call.c below 2 OKAY0.378
id_o3_false-unreach-call.c below 2 OKAY0.39
sum_10x0_false-unreach-call.c below 2 OKAY0.443
sum_10x0_true-unreach-call.c below 2 PASS0.409
sum_15x0_false-unreach-call.c below 2 OKAY0.44
sum_15x0_true-unreach-call.c below 2 PASS0.423
sum_20x0_false-unreach-call.c below 2 OKAY0.429
sum_20x0_true-unreach-call.c below 2 PASS0.425
sum_25x0_false-unreach-call.c below 2 OKAY0.437
sum_25x0_true-unreach-call.c below 2 PASS0.416
sum_2x3_false-unreach-call.c below 2 OKAY0.423
sum_2x3_true-unreach-call.c below 2 PASS0.419
sum_non_eq_false-unreach-call.c below 2 OKAY0.451
sum_non_eq_true-unreach-call.c below 2 PASS0.442
sum_non_false-unreach-call.c below 2 OKAY0.42
sum_non_true-unreach-call.c below 2 PASS0.424
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5430.381
/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.437
rec-bhmr2007_true-unreach-call.c below 2 PASS0.441
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.68
rec-cggmp2005_true-unreach-call.c below 2 PASS0.381
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.406
rec-css2003_true-unreach-call.c below 2 PASS1.028
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.005
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.847
rec-gj2007b_true-unreach-call.c below 2 FAIL0.407
rec-gj2007_true-unreach-call.c below 2 FAIL0.49
rec-gr2006_true-unreach-call.c below 2 FAIL0.456
rec-gsv2008_true-unreach-call.c below 2 PASS0.408
rec-hhk2008_true-unreach-call.c below 2 PASS0.397
rec-jm2006_true-unreach-call.c below 2 PASS0.469
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.503
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.426
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 307.781
/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.364
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.402
rec-count_by_2_true-unreach-call.c below 2 PASS0.354
rec-count_by_k_true-unreach-call.c below 2 PASS0.404
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.394
rec-gauss_sum_true-unreach-call.c below 2 PASS0.434
rec-half_true-unreach-call.c below 2 FAIL0.423
rec-nested_true-unreach-call.c below 3 FAIL0.6
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.375
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.55
cubic_polynomial_unsafe.c below 2 OKAY0.613
edit_distance_bottom_up.c below 3 FAIL198.498
edit_distance_top_down.c below 3 FAIL4.351
log_log_n_solution.c below 3 FAIL0.439
log_log_n_solution_unsafe.c below 3 OKAY0.44
log_n_solution.c below 2 FAIL0.474
log_n_solution_unsafe.c below 2 OKAY0.48
multivariate_1.c below TIMEOUT 300.143
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below TIMEOUT 300.014
multivariate_higher_order_unsafe.c below TIMEOUT 300.016
n_cubed_solution.c below EXCEPTION 105.381
n_cubed_solution_unsafe.c below EXCEPTION 0.024
n_log_n_solution.c below 9 FAIL1.384
n_log_n_solution_unsafe.c below 9 OKAY1.43
n_squared_two_base_case_even.c below 2 PASS0.606
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.593
n_squared_two_base_case_odd.c below 2 PASS0.566
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.629
pascals_dynamic.c below 3 FAIL3.007
pascals_dynamic_unsafe.c below 3 OKAY3.085
pascals_iterative.c below 1 FAIL4.911
pascals_iterative_unsafe.c below 1 OKAY5.024
pascals_recursive.c below 8 FAIL5.384
pascals_recursive_unsafe.c below 8 OKAY5.35
squared_solution.c below 8 FAIL11.115
squared_solution_unsafe.c below 8 OKAY11.187
two_n_even.c below 2 PASS0.399
two_n_even_unsafe.c below 2 OKAY0.424
two_n_odd.c below 2 PASS0.405
two_n_odd_unsafe.c below 2 OKAY0.418
two_to_n_over_two_even.c below 7 FAIL1.021
two_to_n_over_two_even_unsafe.c below 7 OKAY1.007
two_to_n_over_two_odd.c below 7 FAIL1.031
two_to_n_over_two_odd_unsafe.c below 7 OKAY1.046
two_to_n_squared.c below 5 FAIL24.037
two_to_n_squared_unsafe.c below 5 OKAY23.533
two_to_two_to_n.c below 7 FAIL1.077
two_to_two_to_n_unsafe.c below 7 OKAY1.088
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 16/19
ICRA Time = 1621.185
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.372
adding_and_mult_unsafe.c below 1 OKAY0.372
binary_search_array_tree.c below 1 FAIL0.712
exp_add_linear.c below 1 PASS0.399
exp_add_linear_unsafe.c below 1 OKAY0.445
exp_add_loop_rec.c below 1 FAIL0.367
exp_add_loop_rec_unsafe.c below 1 OKAY0.383
exp_add_loop_variable.c below 1 PASS0.407
exp_add_loop_variable_unsafe.c below 1 OKAY0.396
exp_with_linear_inner_loop.c below 1 FAIL0.491
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.477
halving_log1.c below 1 FAIL0.508
linear_two_to_n.c below TIMEOUT 300.008
linear_two_to_n_unsafe.c below TIMEOUT 300.012
loop_five_to_n.c below 1 PASS0.371
loop_five_to_n_unsafe.c below 1 OKAY0.381
non_loop_five_to_n.c below TIMEOUT 300.044
non_loop_five_to_n_unsafe.c below TIMEOUT 300.032
power_log.c below 1 PASS0.481
power_log_modified.c below 1 PASS0.496
simple_exponential.c below 1 PASS0.377
simple_exponential_for.c below 1 PASS0.372
simple_exponential_for_unsafe.c below 1 OKAY0.396
simple_exponential_unsafe.c below 1 OKAY0.409
two_to_n_minus_n.c below 8 FAIL3.067
two_to_n_minus_n_loop.c below 8 FAIL4.761
two_to_n_minus_n_loop_unsafe.c below 8 OKAY4.793
two_to_n_minus_n_unsafe.c below 8 OKAY3.012
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 10/12
ICRA Time = 1224.341
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.536
02.c below 3 FAIL0.696
03.c below 1 PASS0.397
04.c below 1 PASS0.346
05.c below 3 PASS1.0
06.c below 3 PASS7.553
07.c below 3 PASS0.513
08.c below 3 PASS1.124
09.c below 3 PASS0.664
10.c below 3 FAIL0.848
11.c below 1 PASS0.339
12.c below 3 PASS1.178
13.c below 3 PASS0.506
14.c below 3 PASS0.441
15.c below 1 PASS0.351
16.c below 1 PASS0.425
17.c below 1 PASS0.47
18.c below 1 PASS0.399
19.c below 1 PASS0.445
20.c below 3 FAIL0.604
21.c below 3 PASS0.494
22.c below 3 FAIL0.676
23.c below 1 PASS0.363
24.c below 1 PASS0.391
25.c below 3 FAIL1.373
26.c below 3 PASS113.814
27.c below 1 PASS0.409
28.c below 3 PASS0.474
29.c below EXCEPTION 0.415
30.c below 1 PASS0.366
31.c below 3 PASS0.784
32.c below 1 FAIL0.367
33.c below 3 PASS1.326
34.c below 1 FAIL0.383
35.c below 1 PASS0.336
36.c below 3 PASS2.296
37.c below 3 FAIL0.481
38.c below 1 FAIL0.369
39.c below 3 PASS0.421
40.c below 3 PASS0.631
41.c below 1 PASS0.376
42.c below EXCEPTION 0.353
43.c below 3 PASS0.454
44.c below 1 PASS0.364
45.c below 3 FAIL3.154
46.c below 3 FAIL1.757
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 151.462
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.404
AGHKTW2017_foo.c below 1 PASS0.398
AGHKTW2017_loginSafe.c below 1 PASS0.787
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.501
BCK2011_gauss.c below 1 PASS0.476
BCK2011_strength_reduction.c below 1 PASS0.412
BCK2011_strength_reduction_linear.c below 1 PASS0.453
fibonacci_information_flow.c below 1 PASS0.608
TA2005_fib2.c below 1 PASS0.543
TA2005_fib.c below 1 PASS0.452
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 5.034