[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.368
kmp.c below 1 PASS1.594
qsort.c below 5 PASS0.864
speed_pldi09_fig1.c below 1 PASS0.519
speed_pldi09_fig4_2.c below 1 FAIL0.387
speed_pldi09_fig4_4.c below 1 PASS21.163
speed_pldi09_fig4_5.c below 1 PASS0.407
speed_pldi10_ex1.c below 1 PASS1.231
speed_pldi10_ex3.c below 1 PASS0.494
speed_pldi10_ex4.c below 1 PASS0.517
speed_popl10_fig2_1.c below 1 PASS0.454
speed_popl10_fig2_2.c below 1 FAIL0.355
speed_popl10_nested_multiple.c below 1 PASS0.448
speed_popl10_nested_single.c below 1 PASS0.433
speed_popl10_sequential_single.c below 1 PASS0.397
speed_popl10_simple_multiple.c below 1 PASS0.515
speed_popl10_simple_single_2.c below 1 PASS0.657
speed_popl10_simple_single.c below 1 PASS0.359
t07.c below 1 PASS0.424
t08.c below 1 PASS0.384
t09.c below 1 PASS0.386
t10.c below 1 PASS0.376
t11.c below 1 PASS0.461
t13.c below 1 FAIL0.414
t15.c below 1 PASS0.405
t16.c below 1 PASS0.393
t19.c below 1 PASS0.418
t20.c below 1 PASS0.373
t27.c below 1 PASS0.549
t28.c below 1 PASS0.475
t30.c below 1 FAIL0.411
t37.c below 2 PASS0.588
t39.c below 2 PASS0.548
t46.c below 1 PASS0.42
t47.c below 1 FAIL0.544
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 38.731
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.376
qsort_full.c below 4 PASS5.577
rec1-param_safe.c below 2 PASS0.387
rec1-param_unsafe.c below 2 OKAY0.38
rec1_safe.c below 2 PASS0.368
rec1_unsafe.c below 2 OKAY0.358
rec2-param_safe.c below 2 PASS0.378
rec2-param_unsafe.c below 2 OKAY0.429
rec2_safe.c below 2 PASS0.376
rec2_unsafe.c below 2 OKAY0.366
rec-test.c below 2 PASS0.369
sas03_bothbranches.c below 7 PASS0.694
sas03.c below 2 PASS0.789
simulated_lese_recursive.c below 2 PASS0.438
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.285
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.324
count_up_down_unsafe.c below 1 OKAY0.334
divide.c below 1 PASS0.342
factor_unsafe.c below 1 OKAY0.331
for_infinite_loop_1_safe.c below 1 PASS0.321
for_infinite_loop_2_safe.c below 1 PASS0.325
interproc.c below 1 PASS0.309
mult.c below 1 PASS0.332
pointer_arith.c below 1 PASS0.306
quotient.c below 3 PASS0.489
subtract.c below 1 PASS0.325
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.347
sum01_bug02_unsafe.c below 1 OKAY0.601
sum01_real_safe.c below 1 PASS0.313
sum01_safe.c below 1 PASS0.338
sum01_unsafe.c below 1 OKAY0.466
sum02_safe.c below 1 PASS0.368
sum03_safe.c below 1 PASS0.389
sum03_unsafe.c below 1 OKAY0.477
sum04_safe.c below 1 PASS0.351
sum04_unsafe.c below 1 OKAY0.493
terminator_02_safe.c below 1 PASS0.324
terminator_02_unsafe.c below 1 OKAY0.366
terminator_03_safe.c below 1 PASS0.326
terminator_03_unsafe.c below 1 OKAY0.325
token_ring01_safe.c below 4 FAIL68.07
token_ring01_unsafe.c below 4 OKAY113.33
toy_safe.c below EXCEPTION 174.5
trex01_safe.c below 1 PASS0.74
trex01_unsafe.c below 1 OKAY0.361
trex02_safe2.c below 3 PASS0.399
trex02_safe.c below 3 PASS0.398
trex02_unsafe.c below 3 OKAY0.394
trex03_safe.c below 1 PASS0.425
trex03_unsafe.c below 1 OKAY0.425
trex04_safe.c below 1 PASS0.353
while_infinite_loop_1_safe.c below 1 PASS0.311
while_infinite_loop_2_safe.c below 1 PASS0.301
while_infinite_loop_3_safe.c below 1 PASS0.317
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 369.546
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.378
blogger_simplified1.c below 3 PASS1.146
divided_difference2.c below TIMEOUT 300.008
mult-proc.c below 3 PASS0.373
mult-proc-params.c below 3 PASS0.39
popall.c below 1 PASS0.65
simulated_scc.c below 1 PASS0.634
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.579
/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 PASS0.717
degree2_monomial.c below 1 PASS0.393
degree3_binomial.c below 1 PASS1.336
degree3_monomial.c below 1 PASS0.443
degree4_binomial.c below 1 PASS2.627
degree4_monomial.c below 1 PASS0.49
degree5_binomial.c below 1 PASS7.352
degree5_monomial.c below 1 PASS0.58
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 14.306
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.453
cubic_with_square_interproc.c below 2 PASS0.562
cubic_with_square_nonlinear.c below 1 PASS0.357
cubic_with_square_nonlinear_interproc.c below 2 PASS0.399
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.391
cubic_with_square_unsafe.c below 1 OKAY0.456
multi-input.c below 1 PASS214.061
multi-input_unsafe.c below 1 OKAY0.492
nondet_loop_bound.c below 1 PASS0.365
nondet_loop_bound_quartic.c below 1 PASS0.387
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.37
nondet_loop_bound_unsafe.c below 1 OKAY0.372
nonlinear_stratified.c below 1 PASS79.965
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.006
quartic_with_cube.c below 1 PASS0.601
quartic_with_cube_nonlinear.c below 1 PASS0.389
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.376
quartic_with_cube_unsafe.c below 1 OKAY0.509
quintic_with_quartic.c below 1 PASS1.017
quintic_with_quartic_nonlinear.c below 1 PASS0.425
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.434
quintic_with_quartic_unsafe.c below 1 OKAY1.041
ICRA Assertions (True) = 12/12
ICRA Assertions (False) = 9/10
ICRA Time = 603.428
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.695
degree2_FD_AllAux_AllAssm.c below 1 PASS161.794
degree2_FD_AllAux_FewAssm.c below 1 PASS4.992
degree2_FD_FewAux_FewAssm.c below 1 PASS0.931
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.914
degree3.c below 1 PASS0.64
degree3_FD.c below 1 PASS0.818
degree4.c below 1 PASS0.43
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 171.214
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.431
loop_unsafe.c below 1 OKAY0.44
simulated_lese_parser.c below 1 PASS0.352
simulated_lese_sentinel.c below 1 PASS0.353
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.576
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.346
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.346
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.005
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.005
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.347
array_false-unreach-call2.c below 1 OKAY0.358
array_false-unreach-call3.c below 1 OKAY0.35
array_true-unreach-call1.c below 1 FAIL0.352
array_true-unreach-call2.c below 1 FAIL0.372
array_true-unreach-call3.c below 1 PASS0.346
array_true-unreach-call4.c below 1 FAIL0.343
const_false-unreach-call1.c below 1 OKAY0.349
const_true-unreach-call1.c below 1 PASS0.35
diamond_false-unreach-call1.c below 1 OKAY0.364
diamond_true-unreach-call1.c below 1 PASS0.369
diamond_true-unreach-call2.c below 1 PASS0.386
functions_false-unreach-call1.c below 3 OKAY0.387
functions_true-unreach-call1.c below 3 PASS0.377
multivar_false-unreach-call1.c below 1 OKAY0.36
multivar_true-unreach-call1.c below 1 PASS0.353
nested_false-unreach-call1.c below 1 OKAY0.368
nested_true-unreach-call1.c below 1 PASS0.369
overflow_true-unreach-call1.c below 1 PASS0.308
phases_false-unreach-call1.c below 1 OKAY0.408
phases_false-unreach-call2.c below 1 OKAY0.343
phases_true-unreach-call1.c below 1 PASS0.456
phases_true-unreach-call2.c below 1 PASS0.338
simple_false-unreach-call1.c below 1 OKAY0.329
simple_false-unreach-call2.c below 1 OKAY0.325
simple_false-unreach-call3.c below 1 OKAY0.323
simple_false-unreach-call4.c below 1 OKAY0.331
simple_true-unreach-call1.c below 1 PASS0.328
simple_true-unreach-call2.c below 1 PASS0.318
simple_true-unreach-call3.c below 1 PASS0.327
simple_true-unreach-call4.c below 1 PASS0.342
underapprox_false-unreach-call1.c below 1 OKAY0.344
underapprox_false-unreach-call2.c below 1 OKAY0.353
underapprox_true-unreach-call1.c below 1 FAIL0.34
underapprox_true-unreach-call2.c below 1 PASS0.35
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.363
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.841
apache-get-tag_true-unreach-call.c below 1 FAIL0.437
down_true-unreach-call.c below 1 PASS0.357
fragtest_simple_true-unreach-call.c below 1 PASS0.431
half_2_true-unreach-call.c below 1 PASS0.4
heapsort_true-unreach-call.c below 1 TIMEOUT300.204
id_build_true-unreach-call.c below 1 PASS0.525
id_trans_false-unreach-call.c below 1 OKAY0.344
large_const_true-unreach-call.c below 1 PASS0.419
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.369
nested6_true-unreach-call.c below 1 FAIL0.489
nested9_true-unreach-call.c below 1 PASS0.517
nest-if3_true-unreach-call.c below 1 PASS0.481
NetBSD_loop_true-unreach-call.c below 1 PASS0.335
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.407
seq_true-unreach-call.c below 1 PASS0.431
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.471
string_concat-noarr_true-unreach-call.c below 1 PASS0.388
up_true-unreach-call.c below 1 PASS0.358
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 309.204
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.369
bhmr2007_true-unreach-call.c below 1 PASS0.383
cggmp2005b_true-unreach-call.c below 1 PASS0.489
cggmp2005_true-unreach-call.c below 1 PASS0.361
cggmp2005_variant_true-unreach-call.c below 1 PASS0.363
css2003_true-unreach-call.c below 1 PASS0.757
ddlm2013_true-unreach-call.c below 1 PASS0.498
gcnr2008_false-unreach-call.c below 1 OKAY0.897
gj2007b_true-unreach-call.c below 1 FAIL0.38
gj2007_true-unreach-call.c below 1 PASS0.441
gr2006_true-unreach-call.c below 1 PASS0.43
gsv2008_true-unreach-call.c below 1 PASS0.354
hhk2008_true-unreach-call.c below 1 PASS0.328
jm2006_true-unreach-call.c below 1 PASS0.394
jm2006_variant_true-unreach-call.c below 1 PASS0.478
mcmillan2006_true-unreach-call.c below 1 FAIL0.382
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.304
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.323
count_by_1_variant_true-unreach-call.c below 1 PASS0.368
count_by_2_true-unreach-call.c below 1 PASS0.319
count_by_k_true-unreach-call.c below 1 PASS0.357
count_by_nondet_true-unreach-call.c below 1 FAIL0.352
gauss_sum_true-unreach-call.c below 1 PASS0.367
half_true-unreach-call.c below 1 FAIL0.371
nested_true-unreach-call.c below 1 PASS0.414
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.871
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.383
array_true-unreach-call.c below 1 FAIL0.374
bubble_sort_false-unreach-call.c below 4 OKAY49.27
bubble_sort_true-unreach-call.c below 1 PASS3.653
compact_false-unreach-call.c below 1 OKAY0.385
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.353
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.357
eureka_01_false-unreach-call.c below 1 OKAY2.041
eureka_01_true-unreach-call.c below 1 FAIL1.401
eureka_05_true-unreach-call.c below TIMEOUT 300.004
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.343
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.314
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.32
heavy_false-unreach-call.c below 1 OKAY0.459
heavy_true-unreach-call.c below 1 PASS0.454
insertion_sort_false-unreach-call.c below 1 OKAY1.531
insertion_sort_true-unreach-call.c below 1 FAIL0.516
invert_string_false-unreach-call.c below 1 OKAY0.499
invert_string_true-unreach-call.c below 1 FAIL0.535
linear_sea.ch_true-unreach-call.c below 1 FAIL0.385
linear_search_false-unreach-call.c below 1 OKAY0.398
lu.cmp_true-unreach-call.c below 3 PASS16.057
ludcmp_false-unreach-call.c below 3 OKAY16.53
matrix_false-unreach-call_true-termination.c below 1 OKAY1.037
matrix_true-unreach-call_true-termination.c below 1 FAIL0.418
n.c11_true-unreach-call.c below 3 FAIL0.419
n.c24_false-unreach-call.c below 3 OKAY2.679
n.c40_true-unreach-call.c below 1 FAIL0.373
nec11_false-unreach-call.c below 1 OKAY0.359
nec20_false-unreach-call.c below 1 OKAY0.403
nec40_true-unreach-call.c below 1 FAIL0.379
string_false-unreach-call.c below 1 OKAY0.606
string_true-unreach-call.c below 1 FAIL0.626
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.594
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.46
sum01_true-unreach-call_true-termination.c below 1 PASS0.364
sum03_false-unreach-call_true-termination.c below 1 OKAY0.49
sum03_true-unreach-call_false-termination.c below 1 PASS0.443
sum04_false-unreach-call_true-termination.c below 1 OKAY0.464
sum04_true-unreach-call_true-termination.c below 1 PASS0.347
sum_array_false-unreach-call.c below 1 OKAY0.573
sum_array_true-unreach-call.c below 1 FAIL0.642
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.332
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.455
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.35
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.351
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.345
trex01_false-unreach-call_true-termination.c below 3 OKAY0.435
trex01_true-unreach-call.c below 3 PASS0.679
trex02_false-unreach-call_true-termination.c below 3 OKAY0.393
trex02_true-unreach-call_true-termination.c below 3 PASS0.392
trex03_false-unreach-call_true-termination.c below 3 OKAY0.669
trex03_true-unreach-call.c below 3 PASS0.674
trex04_true-unreach-call_false-termination.c below 1 PASS0.4
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.338
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.394
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.373
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.354
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY3.827
vogal_false-unreach-call.c below 1 OKAY0.752
vogal_true-unreach-call.c below 1 FAIL0.732
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.304
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.313
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.318
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 = 427.076
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.945
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.912
Ackermann03_true-unreach-call.c below 7 FAIL0.97
Ackermann04_true-unreach-call.c below 7 FAIL0.971
Addition01_true-unreach-call_true-termination.c below 2 PASS0.558
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.527
Addition03_false-no-overflow.c below 2 PASS0.538
Addition03_true-unreach-call.c below 2 PASS0.542
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.462
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.418
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.423
Fibonacci01_true-unreach-call.c below 7 FAIL0.696
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.652
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.701
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.668
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.68
gcd01_true-unreach-call_true-termination.c below 2 PASS0.551
gcd02_true-unreach-call.c below 2 FAIL0.926
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY6.942
McCarthy91_true-unreach-call.c below 7 PASS6.961
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.556
Primes_true-unreach-call.c below 3 FAIL1.368
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.715
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.396
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.39
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 7/7
ICRA Time = 30.468
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.441
afterrec_2calls_true-unreach-call.c below 2 PASS0.401
afterrec_false-unreach-call.c below 2 OKAY0.373
afterrec_true-unreach-call.c below 2 PASS0.368
fibo_10_false-unreach-call.c below 7 OKAY0.657
fibo_10_true-unreach-call.c below 7 FAIL0.662
fibo_15_false-unreach-call.c below 7 OKAY0.685
fibo_15_true-unreach-call.c below 7 FAIL0.686
fibo_20_false-unreach-call.c below 7 OKAY0.68
fibo_20_true-unreach-call.c below 7 FAIL0.666
fibo_25_false-unreach-call.c below 7 OKAY0.666
fibo_25_true-unreach-call.c below 7 FAIL0.693
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.032
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.02
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.013
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.016
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.016
fibo_5_false-unreach-call.c below 7 OKAY0.67
fibo_5_true-unreach-call.c below 7 FAIL0.699
fibo_7_false-unreach-call.c below 7 OKAY0.656
fibo_7_true-unreach-call.c below 7 FAIL0.677
id2_b2_o3_true-unreach-call.c below 2 PASS0.617
id2_b3_o2_false-unreach-call.c below 2 OKAY0.66
id2_b3_o5_true-unreach-call.c below 2 PASS0.609
id2_b5_o10_true-unreach-call.c below 2 PASS0.647
id2_i5_o5_false-unreach-call.c below 2 OKAY0.415
id2_i5_o5_true-unreach-call.c below 2 PASS0.402
id_b2_o3_true-unreach-call.c below 2 PASS0.538
id_b3_o2_false-unreach-call.c below 2 OKAY0.532
id_b3_o5_true-unreach-call.c below 2 PASS0.539
id_b5_o10_true-unreach-call.c below 2 PASS0.539
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.374
id_i15_o15_true-unreach-call.c below 2 PASS0.37
id_i20_o20_false-unreach-call.c below 2 OKAY0.371
id_i20_o20_true-unreach-call.c below 2 PASS0.385
id_i25_o25_false-unreach-call.c below 2 OKAY0.381
id_i25_o25_true-unreach-call.c below 2 PASS0.38
id_i5_o5_false-unreach-call.c below 2 OKAY0.38
id_i5_o5_true-unreach-call.c below 2 PASS0.366
id_o1000_false-unreach-call.c below 2 OKAY0.381
id_o100_false-unreach-call.c below 2 OKAY0.387
id_o10_false-unreach-call.c below 2 OKAY0.383
id_o200_false-unreach-call.c below 2 OKAY0.368
id_o20_false-unreach-call.c below 2 OKAY0.373
id_o3_false-unreach-call.c below 2 OKAY0.379
sum_10x0_false-unreach-call.c below 2 OKAY0.424
sum_10x0_true-unreach-call.c below 2 PASS0.408
sum_15x0_false-unreach-call.c below 2 OKAY0.394
sum_15x0_true-unreach-call.c below 2 PASS0.406
sum_20x0_false-unreach-call.c below 2 OKAY0.403
sum_20x0_true-unreach-call.c below 2 PASS0.412
sum_25x0_false-unreach-call.c below 2 OKAY0.405
sum_25x0_true-unreach-call.c below 2 PASS0.413
sum_2x3_false-unreach-call.c below 2 OKAY0.412
sum_2x3_true-unreach-call.c below 2 PASS0.424
sum_non_eq_false-unreach-call.c below 2 OKAY0.405
sum_non_eq_true-unreach-call.c below 2 PASS0.4
sum_non_false-unreach-call.c below 2 OKAY0.424
sum_non_true-unreach-call.c below 2 PASS0.413
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5427.228
/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.413
rec-bhmr2007_true-unreach-call.c below 2 PASS0.408
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.636
rec-cggmp2005_true-unreach-call.c below 2 PASS0.389
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.399
rec-css2003_true-unreach-call.c below 2 PASS1.009
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.113
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.765
rec-gj2007b_true-unreach-call.c below 2 FAIL0.366
rec-gj2007_true-unreach-call.c below 2 FAIL0.46
rec-gr2006_true-unreach-call.c below 2 FAIL0.465
rec-gsv2008_true-unreach-call.c below 2 PASS0.424
rec-hhk2008_true-unreach-call.c below 2 PASS0.376
rec-jm2006_true-unreach-call.c below 2 PASS0.437
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.496
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.435
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.591
/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.366
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.402
rec-count_by_2_true-unreach-call.c below 2 PASS0.352
rec-count_by_k_true-unreach-call.c below 2 PASS0.38
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.398
rec-gauss_sum_true-unreach-call.c below 2 PASS0.398
rec-half_true-unreach-call.c below 2 FAIL0.394
rec-nested_true-unreach-call.c below 3 FAIL0.51
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.2
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.492
cubic_polynomial_unsafe.c below 2 OKAY0.497
edit_distance_bottom_up.c below 3 FAIL126.159
edit_distance_top_down.c below 3 FAIL2.587
log_log_n_solution.c below 3 FAIL0.403
log_log_n_solution_unsafe.c below 3 OKAY0.433
log_n_solution.c below 2 FAIL0.439
log_n_solution_unsafe.c below 2 OKAY0.464
multivariate_1.c below TIMEOUT 300.004
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL18.888
multivariate_higher_order_unsafe.c below 7 OKAY18.857
n_cubed_solution.c below EXCEPTION 45.511
n_cubed_solution_unsafe.c below EXCEPTION 0.024
n_log_n_solution.c below TIMEOUT 300.055
n_log_n_solution_unsafe.c below TIMEOUT 300.046
n_squared_two_base_case_even.c below 2 PASS0.483
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.532
n_squared_two_base_case_odd.c below 2 PASS0.475
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.473
pascals_dynamic.c below 3 FAIL2.38
pascals_dynamic_unsafe.c below 3 OKAY2.457
pascals_iterative.c below 1 FAIL3.493
pascals_iterative_unsafe.c below 1 OKAY3.613
pascals_recursive.c below 8 FAIL9.58
pascals_recursive_unsafe.c below 8 OKAY9.712
squared_solution.c below TIMEOUT 300.004
squared_solution_unsafe.c below TIMEOUT 300.006
two_n_even.c below 2 PASS0.412
two_n_even_unsafe.c below 2 OKAY0.403
two_n_odd.c below 2 PASS0.41
two_n_odd_unsafe.c below 2 OKAY0.415
two_to_n_over_two_even.c below TIMEOUT 300.004
two_to_n_over_two_even_unsafe.c below TIMEOUT 300.007
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.941
two_to_n_squared_unsafe.c below 8 OKAY20.564
two_to_two_to_n.c below 7 FAIL0.866
two_to_two_to_n_unsafe.c below 7 OKAY0.832
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 13/19
ICRA Time = 3292.934
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.364
adding_and_mult_unsafe.c below 1 OKAY0.372
binary_search_array_tree.c below 1 FAIL0.62
exp_add_linear.c below 1 PASS0.419
exp_add_linear_unsafe.c below 1 OKAY0.424
exp_add_loop_rec.c below 1 FAIL0.357
exp_add_loop_rec_unsafe.c below 1 OKAY0.366
exp_add_loop_variable.c below 1 PASS0.413
exp_add_loop_variable_unsafe.c below 1 OKAY0.404
exp_with_linear_inner_loop.c below 1 FAIL0.465
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.466
halving_log1.c below 1 FAIL0.507
linear_two_to_n.c below 8 FAIL1.084
linear_two_to_n_unsafe.c below 8 OKAY1.083
loop_five_to_n.c below 1 PASS0.393
loop_five_to_n_unsafe.c below 1 OKAY0.407
non_loop_five_to_n.c below TIMEOUT 300.041
non_loop_five_to_n_unsafe.c below TIMEOUT 300.031
power_log.c below 1 PASS0.465
power_log_modified.c below 1 PASS0.494
simple_exponential.c below 1 PASS0.386
simple_exponential_for.c below 1 PASS0.398
simple_exponential_for_unsafe.c below 1 OKAY0.383
simple_exponential_unsafe.c below 1 OKAY0.384
two_to_n_minus_n.c below 7 FAIL1.158
two_to_n_minus_n_loop.c below 7 FAIL1.658
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.647
two_to_n_minus_n_unsafe.c below 7 OKAY1.143
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 616.332
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.532
02.c below 3 FAIL0.668
03.c below 1 PASS0.407
04.c below 1 PASS0.352
05.c below 3 PASS1.682
06.c below 3 PASS5.614
07.c below 3 PASS0.503
08.c below 3 PASS1.051
09.c below 3 PASS0.619
10.c below 3 FAIL0.781
11.c below 1 PASS0.336
12.c below 3 PASS1.503
13.c below 3 PASS0.494
14.c below 3 PASS0.431
15.c below 1 PASS0.34
16.c below 1 PASS0.409
17.c below EXCEPTION 0.38
18.c below 1 PASS0.384
19.c below 1 PASS0.442
20.c below 3 FAIL0.583
21.c below 3 PASS0.454
22.c below 3 FAIL0.641
23.c below 1 PASS0.359
24.c below 1 PASS0.388
25.c below 3 FAIL1.14
26.c below TIMEOUT 300.006
27.c below 1 PASS0.413
28.c below 3 PASS0.474
29.c below 3 PASS0.837
30.c below 1 PASS0.402
31.c below 3 PASS0.761
32.c below 1 FAIL0.373
33.c below 3 PASS1.23
34.c below 1 FAIL0.385
35.c below 1 PASS0.333
36.c below 3 PASS2.822
37.c below 3 FAIL0.471
38.c below 1 FAIL0.371
39.c below 3 PASS0.405
40.c below 3 PASS0.614
41.c below 1 PASS0.411
42.c below 3 PASS0.741
43.c below 3 PASS0.434
44.c below 1 PASS0.377
45.c below 3 FAIL3.518
46.c below 3 FAIL1.656
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 337.527
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.393
AGHKTW2017_foo.c below 1 PASS0.387
AGHKTW2017_loginSafe.c below 1 PASS0.765
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.434
BCK2011_gauss.c below 1 PASS0.408
BCK2011_strength_reduction.c below 1 PASS0.389
BCK2011_strength_reduction_linear.c below 1 PASS0.442
fibonacci_information_flow.c below 1 PASS0.564
TA2005_fib2.c below 1 PASS0.552
TA2005_fib.c below 1 PASS0.453
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.787