[Version Information]
WALi-OpenNWA version: 0f994ef6a5cbe02200899575605ae35f227d9ddb (2017-07-12 11:45:09 -0500) "Added programs and files used for POPL18"
duet version: 37312f93042d9322883c425e7b53f0a32ea6ba3b (2017-07-05 19:03:26 -0400) "Big O bounds in print_hull"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.5.3  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
camlp4               4.02+7  Camlp4 is a system for writing extensible parsers f
cil                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
conf-which                1  Virtual package relying on which
cppo                  1.4.1  Equivalent of the C preprocessor for OCaml programs
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170101  LR(1) parser generator
mlgmpidl              1.2.4  OCaml interface to the GMP library
num                       0  The Num library for arbitrary-precision integer and
oasis                 0.4.8  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.1  A library manager for OCaml
ocamlgraph            1.8.7  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.8  Generate OCaml modules from source files
OCRS             20170627v3  Recurrence solver based on operational calculus
optcomp                 1.6  Optional compilation with cpp-like directives
ounit                 2.0.0  Unit testing framework loosely based on HUnit. It i
ppx_deriving            4.1  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
result                  1.2  Compatibility Result module
Z3                 20161217  Z3 SMT solver

Test Name Output No. of Rounds Result Run Time
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below 1 FAIL0.358
kmp.c below 1 PASS1.683
qsort.c below 5 PASS0.885
speed_pldi09_fig1.c below 1 PASS0.502
speed_pldi09_fig4_2.c below 1 FAIL0.378
speed_pldi09_fig4_4.c below 1 PASS21.347
speed_pldi09_fig4_5.c below 1 PASS0.404
speed_pldi10_ex1.c below 1 PASS1.176
speed_pldi10_ex3.c below 1 PASS0.491
speed_pldi10_ex4.c below 1 PASS0.517
speed_popl10_fig2_1.c below 1 PASS0.47
speed_popl10_fig2_2.c below 1 FAIL0.374
speed_popl10_nested_multiple.c below 1 PASS0.463
speed_popl10_nested_single.c below 1 PASS0.429
speed_popl10_sequential_single.c below 1 PASS0.414
speed_popl10_simple_multiple.c below 1 PASS0.513
speed_popl10_simple_single_2.c below 1 PASS0.67
speed_popl10_simple_single.c below 1 PASS0.369
t07.c below 1 PASS0.431
t08.c below 1 PASS0.391
t09.c below 1 PASS0.386
t10.c below 1 PASS0.36
t11.c below 1 PASS0.475
t13.c below 1 FAIL0.435
t15.c below 1 PASS0.419
t16.c below 1 PASS0.385
t19.c below 1 PASS0.39
t20.c below 1 PASS0.379
t27.c below 1 PASS0.527
t28.c below 1 PASS0.465
t30.c below 1 FAIL0.421
t37.c below 2 PASS0.59
t39.c below 2 PASS0.562
t46.c below 1 PASS0.389
t47.c below 1 FAIL0.533
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 38.981
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.385
qsort_full.c below 4 PASS5.523
rec1-param_safe.c below 2 PASS0.382
rec1-param_unsafe.c below 2 OKAY0.392
rec1_safe.c below 2 PASS0.364
rec1_unsafe.c below 2 OKAY0.36
rec2-param_safe.c below 2 PASS0.371
rec2-param_unsafe.c below 2 OKAY0.373
rec2_safe.c below 2 PASS0.366
rec2_unsafe.c below 2 OKAY0.355
rec-test.c below 2 PASS0.357
sas03_bothbranches.c below 7 PASS0.696
sas03.c below 2 PASS0.777
simulated_lese_recursive.c below 2 PASS0.418
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.119
/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.363
divide.c below 1 PASS0.35
factor_unsafe.c below 1 OKAY0.327
for_infinite_loop_1_safe.c below 1 PASS0.322
for_infinite_loop_2_safe.c below 1 PASS0.316
interproc.c below 1 PASS0.321
mult.c below 1 PASS0.339
pointer_arith.c below 1 PASS0.3
quotient.c below 3 PASS0.477
subtract.c below 1 PASS0.337
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.353
sum01_bug02_unsafe.c below 1 OKAY0.605
sum01_real_safe.c below 1 PASS0.339
sum01_safe.c below 1 PASS0.339
sum01_unsafe.c below 1 OKAY0.462
sum02_safe.c below 1 PASS0.372
sum03_safe.c below 1 PASS0.402
sum03_unsafe.c below 1 OKAY0.485
sum04_safe.c below 1 PASS0.355
sum04_unsafe.c below 1 OKAY0.473
terminator_02_safe.c below 1 PASS0.338
terminator_02_unsafe.c below 1 OKAY0.354
terminator_03_safe.c below 1 PASS0.335
terminator_03_unsafe.c below 1 OKAY0.339
token_ring01_safe.c below 4 FAIL68.303
token_ring01_unsafe.c below 4 OKAY114.168
toy_safe.c below EXCEPTION 169.485
trex01_safe.c below 1 PASS0.716
trex01_unsafe.c below 1 OKAY0.379
trex02_safe2.c below 3 PASS0.381
trex02_safe.c below 3 PASS0.401
trex02_unsafe.c below 3 OKAY0.387
trex03_safe.c below 1 PASS0.421
trex03_unsafe.c below 1 OKAY0.431
trex04_safe.c below 1 PASS0.359
while_infinite_loop_1_safe.c below 1 PASS0.321
while_infinite_loop_2_safe.c below 1 PASS0.307
while_infinite_loop_3_safe.c below 1 PASS0.309
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 365.701
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.387
blogger_simplified1.c below 3 PASS1.045
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.374
mult-proc-params.c below 3 PASS0.383
popall.c below 1 PASS0.687
simulated_scc.c below 1 PASS0.636
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.517
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.371
degree2_binomial.c below 1 PASS0.72
degree2_monomial.c below 1 PASS0.388
degree3_binomial.c below 1 PASS1.349
degree3_monomial.c below 1 PASS0.431
degree4_binomial.c below 1 PASS2.708
degree4_monomial.c below 1 PASS0.508
degree5_binomial.c below 1 PASS7.127
degree5_monomial.c below 1 PASS0.546
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 14.148
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.444
cubic_with_square_interproc.c below 2 PASS0.548
cubic_with_square_nonlinear.c below 1 PASS0.355
cubic_with_square_nonlinear_interproc.c below 2 PASS0.413
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.365
cubic_with_square_unsafe.c below 1 OKAY0.451
multi-input.c below 1 PASS213.153
multi-input_unsafe.c below 1 OKAY0.478
nondet_loop_bound.c below 1 PASS0.359
nondet_loop_bound_quartic.c below 1 PASS0.381
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.388
nondet_loop_bound_unsafe.c below 1 OKAY0.376
nonlinear_stratified.c below 1 PASS79.259
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.005
quartic_with_cube.c below 1 PASS0.599
quartic_with_cube_nonlinear.c below 1 PASS0.353
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.378
quartic_with_cube_unsafe.c below 1 OKAY0.485
quintic_with_quartic.c below 1 PASS0.998
quintic_with_quartic_nonlinear.c below 1 PASS0.436
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.457
quintic_with_quartic_unsafe.c below 1 OKAY1.003
ICRA Assertions (True) = 12/12
ICRA Assertions (False) = 9/10
ICRA Time = 601.684
/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 PASS161.542
degree2_FD_AllAux_FewAssm.c below 1 PASS4.989
degree2_FD_FewAux_FewAssm.c below 1 PASS0.904
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.938
degree3.c below 1 PASS0.635
degree3_FD.c below 1 PASS0.784
degree4.c below 1 PASS0.434
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 170.909
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.425
loop_unsafe.c below 1 OKAY0.463
simulated_lese_parser.c below 1 PASS0.353
simulated_lese_sentinel.c below 1 PASS0.351
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.592
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.344
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.344
/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.346
array_false-unreach-call2.c below 1 OKAY0.358
array_false-unreach-call3.c below 1 OKAY0.356
array_true-unreach-call1.c below 1 FAIL0.351
array_true-unreach-call2.c below 1 FAIL0.35
array_true-unreach-call3.c below 1 PASS0.35
array_true-unreach-call4.c below 1 FAIL0.35
const_false-unreach-call1.c below 1 OKAY0.352
const_true-unreach-call1.c below 1 PASS0.349
diamond_false-unreach-call1.c below 1 OKAY0.367
diamond_true-unreach-call1.c below 1 PASS0.37
diamond_true-unreach-call2.c below 1 PASS0.372
functions_false-unreach-call1.c below 3 OKAY0.372
functions_true-unreach-call1.c below 3 PASS0.382
multivar_false-unreach-call1.c below 1 OKAY0.35
multivar_true-unreach-call1.c below 1 PASS0.362
nested_false-unreach-call1.c below 1 OKAY0.38
nested_true-unreach-call1.c below 1 PASS0.354
overflow_true-unreach-call1.c below 1 PASS0.31
phases_false-unreach-call1.c below 1 OKAY0.408
phases_false-unreach-call2.c below 1 OKAY0.339
phases_true-unreach-call1.c below 1 PASS0.392
phases_true-unreach-call2.c below 1 PASS0.343
simple_false-unreach-call1.c below 1 OKAY0.332
simple_false-unreach-call2.c below 1 OKAY0.321
simple_false-unreach-call3.c below 1 OKAY0.324
simple_false-unreach-call4.c below 1 OKAY0.336
simple_true-unreach-call1.c below 1 PASS0.32
simple_true-unreach-call2.c below 1 PASS0.311
simple_true-unreach-call3.c below 1 PASS0.338
simple_true-unreach-call4.c below 1 PASS0.313
underapprox_false-unreach-call1.c below 1 OKAY0.329
underapprox_false-unreach-call2.c below 1 OKAY0.34
underapprox_true-unreach-call1.c below 1 FAIL0.334
underapprox_true-unreach-call2.c below 1 PASS0.345
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.206
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.826
apache-get-tag_true-unreach-call.c below 1 FAIL0.428
down_true-unreach-call.c below 1 PASS0.359
fragtest_simple_true-unreach-call.c below 1 PASS0.447
half_2_true-unreach-call.c below 1 PASS0.392
heapsort_true-unreach-call.c below 1 TIMEOUT300.206
id_build_true-unreach-call.c below 1 PASS0.509
id_trans_false-unreach-call.c below 1 OKAY0.334
large_const_true-unreach-call.c below 1 PASS0.416
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.371
nested6_true-unreach-call.c below 1 FAIL0.483
nested9_true-unreach-call.c below 1 PASS0.499
nest-if3_true-unreach-call.c below 1 PASS0.468
NetBSD_loop_true-unreach-call.c below 1 PASS0.336
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.381
seq_true-unreach-call.c below 1 PASS0.428
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.455
string_concat-noarr_true-unreach-call.c below 1 PASS0.384
up_true-unreach-call.c below 1 PASS0.369
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 309.091
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.385
bhmr2007_true-unreach-call.c below 1 PASS0.38
cggmp2005b_true-unreach-call.c below 1 PASS0.485
cggmp2005_true-unreach-call.c below 1 PASS0.353
cggmp2005_variant_true-unreach-call.c below 1 PASS0.351
css2003_true-unreach-call.c below 1 PASS0.771
ddlm2013_true-unreach-call.c below 1 PASS0.526
gcnr2008_false-unreach-call.c below 1 OKAY0.913
gj2007b_true-unreach-call.c below 1 FAIL0.388
gj2007_true-unreach-call.c below 1 PASS0.442
gr2006_true-unreach-call.c below 1 PASS0.437
gsv2008_true-unreach-call.c below 1 PASS0.349
hhk2008_true-unreach-call.c below 1 PASS0.332
jm2006_true-unreach-call.c below 1 PASS0.407
jm2006_variant_true-unreach-call.c below 1 PASS0.479
mcmillan2006_true-unreach-call.c below 1 FAIL0.39
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.388
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.313
count_by_1_variant_true-unreach-call.c below 1 PASS0.372
count_by_2_true-unreach-call.c below 1 PASS0.32
count_by_k_true-unreach-call.c below 1 PASS0.344
count_by_nondet_true-unreach-call.c below 1 FAIL0.355
gauss_sum_true-unreach-call.c below 1 PASS0.37
half_true-unreach-call.c below 1 FAIL0.358
nested_true-unreach-call.c below 1 PASS0.423
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.855
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.375
array_true-unreach-call.c below 1 FAIL0.378
bubble_sort_false-unreach-call.c below 4 OKAY49.283
bubble_sort_true-unreach-call.c below 1 PASS3.593
compact_false-unreach-call.c below 1 OKAY0.379
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.332
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.337
eureka_01_false-unreach-call.c below 1 OKAY2.039
eureka_01_true-unreach-call.c below 1 FAIL1.426
eureka_05_true-unreach-call.c below TIMEOUT 300.004
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.342
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.321
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.32
heavy_false-unreach-call.c below 1 OKAY0.461
heavy_true-unreach-call.c below 1 PASS0.442
insertion_sort_false-unreach-call.c below 1 OKAY1.519
insertion_sort_true-unreach-call.c below 1 FAIL0.546
invert_string_false-unreach-call.c below 1 OKAY0.502
invert_string_true-unreach-call.c below 1 FAIL0.511
linear_sea.ch_true-unreach-call.c below 1 FAIL0.388
linear_search_false-unreach-call.c below 1 OKAY0.395
lu.cmp_true-unreach-call.c below 3 PASS16.144
ludcmp_false-unreach-call.c below 3 OKAY16.3
matrix_false-unreach-call_true-termination.c below 1 OKAY1.03
matrix_true-unreach-call_true-termination.c below 1 FAIL0.397
n.c11_true-unreach-call.c below 3 FAIL0.411
n.c24_false-unreach-call.c below 3 OKAY2.624
n.c40_true-unreach-call.c below 1 FAIL0.355
nec11_false-unreach-call.c below 1 OKAY0.356
nec20_false-unreach-call.c below 1 OKAY0.381
nec40_true-unreach-call.c below 1 FAIL0.388
string_false-unreach-call.c below 1 OKAY0.611
string_true-unreach-call.c below 1 FAIL0.627
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.608
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.331
sum01_false-unreach-call_true-termination.c below 1 OKAY0.461
sum01_true-unreach-call_true-termination.c below 1 PASS0.367
sum03_false-unreach-call_true-termination.c below 1 OKAY0.494
sum03_true-unreach-call_false-termination.c below 1 PASS0.43
sum04_false-unreach-call_true-termination.c below 1 OKAY0.475
sum04_true-unreach-call_true-termination.c below 1 PASS0.357
sum_array_false-unreach-call.c below 1 OKAY0.567
sum_array_true-unreach-call.c below 1 FAIL0.605
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.322
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.456
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.35
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.326
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.336
trex01_false-unreach-call_true-termination.c below 3 OKAY0.445
trex01_true-unreach-call.c below 3 PASS0.672
trex02_false-unreach-call_true-termination.c below 3 OKAY0.404
trex02_true-unreach-call_true-termination.c below 3 PASS0.39
trex03_false-unreach-call_true-termination.c below 3 OKAY0.652
trex03_true-unreach-call.c below 3 PASS0.646
trex04_true-unreach-call_false-termination.c below 1 PASS0.383
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.358
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.398
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.362
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.352
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY3.876
vogal_false-unreach-call.c below 1 OKAY0.746
vogal_true-unreach-call.c below 1 FAIL0.733
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.309
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.294
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.312
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 = 426.639
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.96
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.95
Ackermann03_true-unreach-call.c below 7 FAIL0.994
Ackermann04_true-unreach-call.c below 7 FAIL0.921
Addition01_true-unreach-call_true-termination.c below 2 PASS0.505
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.573
Addition03_false-no-overflow.c below 2 PASS0.546
Addition03_true-unreach-call.c below 2 PASS0.56
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.468
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.405
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.406
Fibonacci01_true-unreach-call.c below 7 FAIL0.682
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.681
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.69
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.67
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.701
gcd01_true-unreach-call_true-termination.c below 2 PASS0.546
gcd02_true-unreach-call.c below 2 FAIL0.914
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY6.89
McCarthy91_true-unreach-call.c below 7 PASS6.944
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.547
Primes_true-unreach-call.c below 3 FAIL1.356
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.648
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.369
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.374
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 7/7
ICRA Time = 30.3
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.418
afterrec_2calls_true-unreach-call.c below 2 PASS0.408
afterrec_false-unreach-call.c below 2 OKAY0.386
afterrec_true-unreach-call.c below 2 PASS0.358
fibo_10_false-unreach-call.c below 7 OKAY0.649
fibo_10_true-unreach-call.c below 7 FAIL0.673
fibo_15_false-unreach-call.c below 7 OKAY0.67
fibo_15_true-unreach-call.c below 7 FAIL0.682
fibo_20_false-unreach-call.c below 7 OKAY0.687
fibo_20_true-unreach-call.c below 7 FAIL0.676
fibo_25_false-unreach-call.c below 7 OKAY0.694
fibo_25_true-unreach-call.c below 7 FAIL0.68
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.027
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.01
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.016
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.017
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.016
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.01
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.016
fibo_5_false-unreach-call.c below 7 OKAY0.675
fibo_5_true-unreach-call.c below 7 FAIL0.675
fibo_7_false-unreach-call.c below 7 OKAY0.655
fibo_7_true-unreach-call.c below 7 FAIL0.663
id2_b2_o3_true-unreach-call.c below 2 PASS0.593
id2_b3_o2_false-unreach-call.c below 2 OKAY0.654
id2_b3_o5_true-unreach-call.c below 2 PASS0.611
id2_b5_o10_true-unreach-call.c below 2 PASS0.604
id2_i5_o5_false-unreach-call.c below 2 OKAY0.423
id2_i5_o5_true-unreach-call.c below 2 PASS0.387
id_b2_o3_true-unreach-call.c below 2 PASS0.55
id_b3_o2_false-unreach-call.c below 2 OKAY0.529
id_b3_o5_true-unreach-call.c below 2 PASS0.531
id_b5_o10_true-unreach-call.c below 2 PASS0.519
id_i10_o10_false-unreach-call.c below 2 OKAY0.377
id_i10_o10_true-unreach-call.c below 2 PASS0.377
id_i15_o15_false-unreach-call.c below 2 OKAY0.394
id_i15_o15_true-unreach-call.c below 2 PASS0.387
id_i20_o20_false-unreach-call.c below 2 OKAY0.368
id_i20_o20_true-unreach-call.c below 2 PASS0.378
id_i25_o25_false-unreach-call.c below 2 OKAY0.377
id_i25_o25_true-unreach-call.c below 2 PASS0.366
id_i5_o5_false-unreach-call.c below 2 OKAY0.385
id_i5_o5_true-unreach-call.c below 2 PASS0.366
id_o1000_false-unreach-call.c below 2 OKAY0.366
id_o100_false-unreach-call.c below 2 OKAY0.383
id_o10_false-unreach-call.c below 2 OKAY0.382
id_o200_false-unreach-call.c below 2 OKAY0.378
id_o20_false-unreach-call.c below 2 OKAY0.382
id_o3_false-unreach-call.c below 2 OKAY0.374
sum_10x0_false-unreach-call.c below 2 OKAY0.42
sum_10x0_true-unreach-call.c below 2 PASS0.409
sum_15x0_false-unreach-call.c below 2 OKAY0.411
sum_15x0_true-unreach-call.c below 2 PASS0.396
sum_20x0_false-unreach-call.c below 2 OKAY0.405
sum_20x0_true-unreach-call.c below 2 PASS0.408
sum_25x0_false-unreach-call.c below 2 OKAY0.408
sum_25x0_true-unreach-call.c below 2 PASS0.45
sum_2x3_false-unreach-call.c below 2 OKAY0.411
sum_2x3_true-unreach-call.c below 2 PASS0.414
sum_non_eq_false-unreach-call.c below 2 OKAY0.398
sum_non_eq_true-unreach-call.c below 2 PASS0.403
sum_non_false-unreach-call.c below 2 OKAY0.418
sum_non_true-unreach-call.c below 2 PASS0.406
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5427.092
/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.433
rec-bhmr2007_true-unreach-call.c below 2 PASS0.414
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.61
rec-cggmp2005_true-unreach-call.c below 2 PASS0.373
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.403
rec-css2003_true-unreach-call.c below 2 PASS0.952
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.077
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.784
rec-gj2007b_true-unreach-call.c below 2 FAIL0.369
rec-gj2007_true-unreach-call.c below 2 FAIL0.458
rec-gr2006_true-unreach-call.c below 2 FAIL0.474
rec-gsv2008_true-unreach-call.c below 2 PASS0.426
rec-hhk2008_true-unreach-call.c below 2 PASS0.394
rec-jm2006_true-unreach-call.c below 2 PASS0.457
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.473
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.407
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.504
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c below 2 PASS0.352
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.398
rec-count_by_2_true-unreach-call.c below 2 PASS0.355
rec-count_by_k_true-unreach-call.c below 2 PASS0.4
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.388
rec-gauss_sum_true-unreach-call.c below 2 PASS0.405
rec-half_true-unreach-call.c below 2 FAIL0.401
rec-nested_true-unreach-call.c below 3 FAIL0.502
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.201
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.488
cubic_polynomial_unsafe.c below 2 OKAY0.52
edit_distance_bottom_up.c below 3 FAIL124.095
edit_distance_top_down.c below 3 FAIL2.658
log_log_n_solution.c below 3 FAIL0.425
log_log_n_solution_unsafe.c below 3 OKAY0.441
log_n_solution.c below 2 FAIL0.459
log_n_solution_unsafe.c below 2 OKAY0.452
multivariate_1.c below TIMEOUT 300.006
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL18.815
multivariate_higher_order_unsafe.c below 7 OKAY18.856
n_cubed_solution.c below EXCEPTION 47.125
n_cubed_solution_unsafe.c below EXCEPTION 0.023
n_log_n_solution.c below TIMEOUT 300.048
n_log_n_solution_unsafe.c below TIMEOUT 300.046
n_squared_two_base_case_even.c below 2 PASS0.471
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.51
n_squared_two_base_case_odd.c below 2 PASS0.493
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.467
pascals_dynamic.c below 3 FAIL2.37
pascals_dynamic_unsafe.c below 3 OKAY2.45
pascals_iterative.c below 1 FAIL3.484
pascals_iterative_unsafe.c below 1 OKAY3.579
pascals_recursive.c below 8 FAIL9.741
pascals_recursive_unsafe.c below 8 OKAY9.916
squared_solution.c below TIMEOUT 300.005
squared_solution_unsafe.c below TIMEOUT 300.006
two_n_even.c below 2 PASS0.393
two_n_even_unsafe.c below 2 OKAY0.402
two_n_odd.c below 2 PASS0.4
two_n_odd_unsafe.c below 2 OKAY0.391
two_to_n_over_two_even.c below TIMEOUT 300.004
two_to_n_over_two_even_unsafe.c below TIMEOUT 300.006
two_to_n_over_two_odd.c below TIMEOUT 300.004
two_to_n_over_two_odd_unsafe.c below TIMEOUT 300.004
two_to_n_squared.c below 8 FAIL20.724
two_to_n_squared_unsafe.c below 8 OKAY20.31
two_to_two_to_n.c below 7 FAIL0.805
two_to_two_to_n_unsafe.c below 7 OKAY0.808
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 13/19
ICRA Time = 3292.205
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.366
adding_and_mult_unsafe.c below 1 OKAY0.372
binary_search_array_tree.c below 1 FAIL0.622
exp_add_linear.c below 1 PASS0.428
exp_add_linear_unsafe.c below 1 OKAY0.423
exp_add_loop_rec.c below 1 FAIL0.362
exp_add_loop_rec_unsafe.c below 1 OKAY0.371
exp_add_loop_variable.c below 1 PASS0.412
exp_add_loop_variable_unsafe.c below 1 OKAY0.399
exp_with_linear_inner_loop.c below 1 FAIL0.459
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.476
halving_log1.c below 1 FAIL0.501
linear_two_to_n.c below 8 FAIL1.071
linear_two_to_n_unsafe.c below 8 OKAY1.074
loop_five_to_n.c below 1 PASS0.392
loop_five_to_n_unsafe.c below 1 OKAY0.382
non_loop_five_to_n.c below TIMEOUT 300.04
non_loop_five_to_n_unsafe.c below TIMEOUT 300.032
power_log.c below 1 PASS0.5
power_log_modified.c below 1 PASS0.498
simple_exponential.c below 1 PASS0.376
simple_exponential_for.c below 1 PASS0.385
simple_exponential_for_unsafe.c below 1 OKAY0.406
simple_exponential_unsafe.c below 1 OKAY0.39
two_to_n_minus_n.c below 7 FAIL1.165
two_to_n_minus_n_loop.c below 7 FAIL1.611
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.638
two_to_n_minus_n_unsafe.c below 7 OKAY1.182
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 616.333
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.535
02.c below 3 FAIL0.658
03.c below 1 PASS0.417
04.c below 1 PASS0.341
05.c below 3 PASS1.74
06.c below 3 PASS5.55
07.c below 3 PASS0.507
08.c below 3 PASS1.054
09.c below 3 PASS0.622
10.c below 3 FAIL0.758
11.c below 1 PASS0.363
12.c below 3 PASS1.566
13.c below 3 PASS0.474
14.c below 3 PASS0.432
15.c below 1 PASS0.343
16.c below 1 PASS0.406
17.c below EXCEPTION 0.35
18.c below 1 PASS0.424
19.c below 1 PASS0.437
20.c below 3 FAIL0.578
21.c below 3 PASS0.453
22.c below 3 FAIL0.655
23.c below 1 PASS0.342
24.c below 1 PASS0.383
25.c below 3 FAIL1.105
26.c below TIMEOUT 300.005
27.c below 1 PASS0.4
28.c below 3 PASS0.474
29.c below 3 PASS0.744
30.c below 1 PASS0.369
31.c below 3 PASS0.757
32.c below 1 FAIL0.357
33.c below 3 PASS1.217
34.c below 1 FAIL0.368
35.c below 1 PASS0.329
36.c below 3 PASS2.878
37.c below 3 FAIL0.458
38.c below 1 FAIL0.391
39.c below 3 PASS0.409
40.c below 3 PASS0.634
41.c below 1 PASS0.381
42.c below 3 PASS0.729
43.c below 3 PASS0.443
44.c below 1 PASS0.362
45.c below 3 FAIL3.531
46.c below 3 FAIL1.619
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 337.348
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.395
AGHKTW2017_foo.c below 1 PASS0.389
AGHKTW2017_loginSafe.c below 1 PASS0.754
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.438
BCK2011_gauss.c below 1 PASS0.425
BCK2011_strength_reduction.c below 1 PASS0.384
BCK2011_strength_reduction_linear.c below 1 PASS0.418
fibonacci_information_flow.c below 1 PASS0.577
TA2005_fib2.c below 1 PASS0.542
TA2005_fib.c below 1 PASS0.481
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.803