[Version Information]
WALi-OpenNWA version: 75fdb983ac71dbbdeebcb250836a1edd25f0b874 (2018-03-01 12:06:33 -0600) "Adding first version of java_icra.sh"
duet version: e0a1b1e22f1b8f755b70e388abf4b098326cd3c9 (2017-12-11 14:36:14 -0500) "Symbolic bounds always include constant bounds if they exist"
# 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-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.7.0  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
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170712  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.10  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.3  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               20170905  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            3.2  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
Z3                 20161217  Z3 SMT solver

Test Name Output No. of Rounds Result Run Time
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below 1 FAIL0.402
kmp.c below 1 PASS1.346
qsort.c below 4 PASS1.262
speed_pldi09_fig1.c below 1 PASS0.671
speed_pldi09_fig4_2.c below 1 FAIL0.454
speed_pldi09_fig4_4.c below 1 PASS0.616
speed_pldi09_fig4_5.c below 1 PASS0.477
speed_pldi10_ex1.c below 1 PASS1.689
speed_pldi10_ex3.c below 1 PASS0.675
speed_pldi10_ex4.c below 1 PASS0.737
speed_popl10_fig2_1.c below 1 PASS0.626
speed_popl10_fig2_2.c below 1 FAIL0.43
speed_popl10_nested_multiple.c below 1 PASS0.576
speed_popl10_nested_single.c below 1 PASS0.528
speed_popl10_sequential_single.c below 1 PASS0.513
speed_popl10_simple_multiple.c below 1 PASS0.75
speed_popl10_simple_single_2.c below 1 PASS0.896
speed_popl10_simple_single.c below 1 PASS0.421
t07.c below 1 PASS0.59
t08.c below 1 PASS0.496
t09.c below 1 PASS0.44
t10.c below 1 PASS0.435
t11.c below 1 PASS0.646
t13.c below 1 FAIL0.523
t15.c below 1 PASS0.533
t16.c below 1 PASS0.498
t19.c below 1 PASS0.499
t20.c below 1 PASS0.446
t27.c below 1 PASS0.786
t28.c below 1 PASS0.712
t30.c below 1 FAIL0.49
t37.c below 2 PASS0.908
t39.c below 2 PASS0.751
t46.c below 1 PASS0.52
t47.c below 1 PASS0.692
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.034
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.504
qsort_full.c below 4 PASS11.585
rec1-param_safe.c below 2 PASS0.527
rec1-param_unsafe.c below 2 OKAY0.525
rec1_safe.c below 2 PASS0.473
rec1_unsafe.c below 2 OKAY0.487
rec2-param_safe.c below 2 PASS0.5
rec2-param_unsafe.c below 2 OKAY0.47
rec2_safe.c below 2 PASS0.463
rec2_unsafe.c below 2 OKAY0.465
rec-test.c below 2 PASS0.465
sas03_bothbranches.c below 7 PASS1.219
sas03.c below 2 PASS0.927
simulated_lese_recursive.c below 2 PASS0.619
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.229
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.387
count_up_down_unsafe.c below 1 OKAY0.395
divide.c below 1 PASS0.395
factor_unsafe.c below 1 OKAY0.367
for_infinite_loop_1_safe.c below 1 PASS0.371
for_infinite_loop_2_safe.c below 1 PASS0.351
interproc.c below 1 PASS0.319
mult.c below 1 PASS0.372
pointer_arith.c below 1 PASS0.333
quotient.c below 3 PASS0.718
subtract.c below 1 PASS0.374
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.372
sum01_bug02_unsafe.c below 1 OKAY0.744
sum01_real_safe.c below 1 PASS0.401
sum01_safe.c below 1 PASS0.413
sum01_unsafe.c below 1 OKAY0.585
sum02_safe.c below 1 PASS0.413
sum03_safe.c below 1 PASS0.479
sum03_unsafe.c below 1 OKAY0.587
sum04_safe.c below 1 PASS0.402
sum04_unsafe.c below 1 OKAY0.583
terminator_02_safe.c below 1 PASS0.346
terminator_02_unsafe.c below 1 OKAY0.41
terminator_03_safe.c below 1 PASS0.365
terminator_03_unsafe.c below 1 OKAY0.368
token_ring01_safe.c below 4 FAIL124.035
token_ring01_unsafe.c below 4 OKAY197.109
toy_safe.c below EXCEPTION 129.575
trex01_safe.c below 1 PASS0.801
trex01_unsafe.c below 1 OKAY0.462
trex02_safe2.c below 3 PASS0.549
trex02_safe.c below 3 PASS0.549
trex02_unsafe.c below 3 OKAY0.534
trex03_safe.c below 1 PASS0.493
trex03_unsafe.c below 1 OKAY0.524
trex04_safe.c below 1 PASS0.383
while_infinite_loop_1_safe.c below 1 PASS0.337
while_infinite_loop_2_safe.c below 1 PASS0.339
while_infinite_loop_3_safe.c below 1 PASS0.342
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 466.882
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.546
blogger_simplified1.c below 3 PASS1.63
divided_difference2.c below TIMEOUT 300.009
mult-proc.c below 3 PASS0.523
mult-proc-params.c below 3 PASS0.53
popall.c below 1 PASS0.958
simulated_scc.c below 1 PASS0.846
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.042
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.41
degree2_binomial.c below 1 PASS0.928
degree2_monomial.c below 1 PASS0.506
degree3_binomial.c below 1 FAIL4.703
degree3_monomial.c below 1 PASS1.007
degree4_binomial.c below 1 FAIL5.082
degree4_monomial.c below 1 PASS1.658
degree5_binomial.c below 1 FAIL16.36
degree5_monomial.c below 1 PASS3.042
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 33.696
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.507
cubic_with_square_interproc.c below 2 FAIL0.727
cubic_with_square_nonlinear.c below 1 FAIL0.651
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.698
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.649
cubic_with_square_unsafe.c below 1 OKAY0.518
multi-input.c below 1 FAIL10.383
multi-input_unsafe.c below 1 OKAY10.302
nondet_loop_bound.c below 1 FAIL0.558
nondet_loop_bound_quartic.c below 1 FAIL0.764
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.798
nondet_loop_bound_unsafe.c below 1 OKAY0.555
nonlinear_stratified.c below 1 PASS124.814
nonlinear_stratified_unsafe.c below 1 OKAY68.104
quartic_with_cube.c below 1 FAIL0.686
quartic_with_cube_nonlinear.c below 1 FAIL0.979
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.957
quartic_with_cube_unsafe.c below 1 OKAY0.546
quintic_with_quartic.c below 1 PASS1.073
quintic_with_quartic_nonlinear.c below 1 PASS1.166
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.2
quintic_with_quartic_unsafe.c below 1 OKAY1.109
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 227.744
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.983
degree2_FD_AllAux_AllAssm.c below 1 PASS103.706
degree2_FD_AllAux_FewAssm.c below 1 PASS7.001
degree2_FD_FewAux_FewAssm.c below 1 PASS1.344
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.431
degree3.c below 1 PASS1.15
degree3_FD.c below 1 PASS1.266
degree4.c below 1 PASS1.903
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 118.784
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.532
loop_unsafe.c below 1 OKAY0.527
simulated_lese_parser.c below 1 PASS0.394
simulated_lese_sentinel.c below 1 PASS0.395
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.848
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.424
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.424
/bat0/stac/Code/WALi-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/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.391
array_false-unreach-call2.c below 1 OKAY0.415
array_false-unreach-call3.c below 1 OKAY0.387
array_true-unreach-call1.c below 1 FAIL0.393
array_true-unreach-call2.c below 1 FAIL0.417
array_true-unreach-call3.c below 1 PASS0.38
array_true-unreach-call4.c below 1 FAIL0.381
const_false-unreach-call1.c below 1 OKAY0.406
const_true-unreach-call1.c below 1 PASS0.413
diamond_false-unreach-call1.c below 1 OKAY0.393
diamond_true-unreach-call1.c below 1 PASS0.408
diamond_true-unreach-call2.c below 1 PASS0.414
functions_false-unreach-call1.c below 3 OKAY0.52
functions_true-unreach-call1.c below 3 PASS0.522
multivar_false-unreach-call1.c below 1 OKAY0.415
multivar_true-unreach-call1.c below 1 PASS0.402
nested_false-unreach-call1.c below 1 OKAY0.468
nested_true-unreach-call1.c below 1 PASS0.456
overflow_true-unreach-call1.c below 1 PASS0.364
phases_false-unreach-call1.c below 1 OKAY0.496
phases_false-unreach-call2.c below 1 OKAY0.375
phases_true-unreach-call1.c below 1 PASS0.511
phases_true-unreach-call2.c below 1 PASS0.39
simple_false-unreach-call1.c below 1 OKAY0.373
simple_false-unreach-call2.c below 1 OKAY0.35
simple_false-unreach-call3.c below 1 OKAY0.349
simple_false-unreach-call4.c below 1 OKAY0.372
simple_true-unreach-call1.c below 1 PASS0.362
simple_true-unreach-call2.c below 1 PASS0.356
simple_true-unreach-call3.c below 1 PASS0.35
simple_true-unreach-call4.c below 1 PASS0.373
underapprox_false-unreach-call1.c below 1 OKAY0.408
underapprox_false-unreach-call2.c below 1 OKAY0.399
underapprox_true-unreach-call1.c below 1 FAIL0.401
underapprox_true-unreach-call2.c below 1 PASS0.41
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.22
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.538
apache-get-tag_true-unreach-call.c below 1 FAIL0.607
down_true-unreach-call.c below 1 PASS0.465
fragtest_simple_true-unreach-call.c below 1 PASS0.603
half_2_true-unreach-call.c below 1 PASS0.485
heapsort_true-unreach-call.c below 1 PASS2.219
id_build_true-unreach-call.c below 1 PASS0.449
id_trans_false-unreach-call.c below 1 OKAY0.382
id_trans_true-unreach-call.c below 1 PASS0.406
large_const_true-unreach-call.c below 1 PASS0.515
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.45
nested6_true-unreach-call.c below 1 FAIL0.639
nested9_true-unreach-call.c below 1 PASS0.746
nest-if3_true-unreach-call.c below 1 PASS0.558
NetBSD_loop_true-unreach-call.c below 1 PASS0.393
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.468
seq_true-unreach-call.c below 1 PASS0.559
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.602
string_concat-noarr_true-unreach-call.c below 1 PASS0.501
up_true-unreach-call.c below 1 PASS0.472
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.057
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.443
bhmr2007_true-unreach-call.c below 1 PASS0.447
cggmp2005b_true-unreach-call.c below 1 PASS0.64
cggmp2005_true-unreach-call.c below 1 PASS0.427
cggmp2005_variant_true-unreach-call.c below 1 PASS0.419
css2003_true-unreach-call.c below 1 PASS1.1
ddlm2013_true-unreach-call.c below 1 PASS0.603
gcnr2008_false-unreach-call.c below 1 OKAY1.104
gj2007b_true-unreach-call.c below 1 FAIL0.449
gj2007_true-unreach-call.c below 1 PASS0.607
gr2006_true-unreach-call.c below 1 PASS0.564
gsv2008_true-unreach-call.c below 1 PASS0.389
hhk2008_true-unreach-call.c below 1 PASS0.388
jm2006_true-unreach-call.c below 1 PASS0.525
jm2006_variant_true-unreach-call.c below 1 PASS0.614
mcmillan2006_true-unreach-call.c below 1 FAIL0.456
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.175
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.361
count_by_1_variant_true-unreach-call.c below 1 PASS0.478
count_by_2_true-unreach-call.c below 1 PASS0.369
count_by_k_true-unreach-call.c below 1 PASS0.378
count_by_nondet_true-unreach-call.c below 1 PASS0.392
gauss_sum_true-unreach-call.c below 1 PASS0.442
half_true-unreach-call.c below 1 FAIL0.408
nested_true-unreach-call.c below 1 PASS0.522
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.35
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.439
array_true-unreach-call.c below 1 FAIL0.443
bubble_sort_false-unreach-call.c below 4 OKAY77.726
bubble_sort_true-unreach-call.c below 1 PASS5.249
compact_false-unreach-call.c below 1 OKAY0.491
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.406
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.413
eureka_01_false-unreach-call.c below 1 OKAY2.659
eureka_01_true-unreach-call.c below 1 FAIL1.58
eureka_05_true-unreach-call.c below 1 FAIL0.872
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.398
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.395
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.369
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.363
heavy_false-unreach-call.c below 1 OKAY0.588
heavy_true-unreach-call.c below 1 PASS0.588
insertion_sort_false-unreach-call.c below 1 OKAY1.528
insertion_sort_true-unreach-call.c below 1 FAIL0.639
invert_string_false-unreach-call.c below 1 OKAY0.595
invert_string_true-unreach-call.c below 1 FAIL0.626
linear_sea.ch_true-unreach-call.c below 1 FAIL0.416
linear_search_false-unreach-call.c below 1 OKAY0.429
lu.cmp_true-unreach-call.c below 3 PASS27.969
ludcmp_false-unreach-call.c below 3 OKAY27.428
matrix_false-unreach-call_true-termination.c below 1 OKAY1.409
matrix_true-unreach-call_true-termination.c below 1 FAIL0.517
n.c11_true-unreach-call.c below 3 FAIL0.575
n.c24_false-unreach-call.c below 3 OKAY5.146
n.c40_true-unreach-call.c below 1 FAIL0.399
nec11_false-unreach-call.c below 1 OKAY0.403
nec20_false-unreach-call.c below 1 OKAY0.446
nec40_true-unreach-call.c below 1 FAIL0.417
string_false-unreach-call.c below 1 OKAY0.76
string_true-unreach-call.c below 1 FAIL0.763
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.72
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.388
sum01_false-unreach-call_true-termination.c below 1 OKAY0.58
sum01_true-unreach-call_true-termination.c below 1 PASS0.414
sum03_false-unreach-call_true-termination.c below 1 OKAY0.642
sum03_true-unreach-call_false-termination.c below 1 PASS0.515
sum04_false-unreach-call_true-termination.c below 1 OKAY0.604
sum04_true-unreach-call_true-termination.c below 1 PASS0.408
sum_array_false-unreach-call.c below 1 OKAY0.655
sum_array_true-unreach-call.c below 1 FAIL0.747
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.357
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.614
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.441
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.373
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.365
trex01_false-unreach-call_true-termination.c below 3 OKAY0.609
trex01_true-unreach-call.c below 3 PASS0.905
trex02_false-unreach-call_true-termination.c below 3 OKAY0.54
trex02_true-unreach-call_true-termination.c below 3 PASS0.54
trex03_false-unreach-call_true-termination.c below 3 OKAY0.835
trex03_true-unreach-call.c below 3 PASS0.877
trex04_true-unreach-call_false-termination.c below 1 PASS0.424
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.404
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.14
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.416
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.432
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.157
vogal_false-unreach-call.c below 1 OKAY0.916
vogal_true-unreach-call.c below 1 FAIL0.94
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.343
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.333
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.342
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.341
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 195.761
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.58
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.508
Ackermann03_true-unreach-call.c below 7 FAIL1.563
Ackermann04_true-unreach-call.c below 7 FAIL1.608
Addition01_true-unreach-call_true-termination.c below 2 PASS0.804
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.787
Addition03_false-no-overflow.c below 2 PASS0.793
Addition03_true-unreach-call.c below 2 PASS0.794
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.642
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.567
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.581
Fibonacci01_true-unreach-call.c below TIMEOUT 300.005
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.005
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.005
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.004
gcd01_true-unreach-call_true-termination.c below 2 PASS0.723
gcd02_true-unreach-call.c below 2 FAIL1.385
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.268
McCarthy91_true-unreach-call.c below 7 FAIL1.266
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.727
Primes_true-unreach-call.c below 3 FAIL2.304
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.44
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.514
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.507
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.386
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.567
afterrec_2calls_true-unreach-call.c below 2 PASS0.55
afterrec_false-unreach-call.c below 2 OKAY0.471
afterrec_true-unreach-call.c below 2 PASS0.459
fibo_10_false-unreach-call.c below TIMEOUT 300.005
fibo_10_true-unreach-call.c below TIMEOUT 300.004
fibo_15_false-unreach-call.c below TIMEOUT 300.004
fibo_15_true-unreach-call.c below TIMEOUT 300.006
fibo_20_false-unreach-call.c below TIMEOUT 300.004
fibo_20_true-unreach-call.c below TIMEOUT 300.004
fibo_25_false-unreach-call.c below TIMEOUT 300.005
fibo_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.007
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.006
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.005
fibo_5_false-unreach-call.c below TIMEOUT 300.005
fibo_5_true-unreach-call.c below TIMEOUT 300.006
fibo_7_false-unreach-call.c below TIMEOUT 300.005
fibo_7_true-unreach-call.c below TIMEOUT 300.004
id2_b2_o3_true-unreach-call.c below 2 PASS0.949
id2_b3_o2_false-unreach-call.c below 2 OKAY0.99
id2_b3_o5_true-unreach-call.c below 2 PASS0.975
id2_b5_o10_true-unreach-call.c below 2 PASS0.965
id2_i5_o5_false-unreach-call.c below 2 OKAY0.559
id2_i5_o5_true-unreach-call.c below 2 PASS0.576
id_b2_o3_true-unreach-call.c below 2 PASS0.821
id_b3_o2_false-unreach-call.c below 2 OKAY0.831
id_b3_o5_true-unreach-call.c below 2 PASS0.832
id_b5_o10_true-unreach-call.c below 2 PASS0.831
id_i10_o10_false-unreach-call.c below 2 OKAY0.51
id_i10_o10_true-unreach-call.c below 2 PASS0.521
id_i15_o15_false-unreach-call.c below 2 OKAY0.5
id_i15_o15_true-unreach-call.c below 2 PASS0.517
id_i20_o20_false-unreach-call.c below 2 OKAY0.511
id_i20_o20_true-unreach-call.c below 2 PASS0.493
id_i25_o25_false-unreach-call.c below 2 OKAY0.514
id_i25_o25_true-unreach-call.c below 2 PASS0.493
id_i5_o5_false-unreach-call.c below 2 OKAY0.518
id_i5_o5_true-unreach-call.c below 2 PASS0.519
id_o1000_false-unreach-call.c below 2 OKAY0.51
id_o100_false-unreach-call.c below 2 OKAY0.51
id_o10_false-unreach-call.c below 2 OKAY0.527
id_o200_false-unreach-call.c below 2 OKAY0.51
id_o20_false-unreach-call.c below 2 OKAY0.495
id_o3_false-unreach-call.c below 2 OKAY0.501
sum_10x0_false-unreach-call.c below 2 OKAY0.572
sum_10x0_true-unreach-call.c below 2 PASS0.56
sum_15x0_false-unreach-call.c below 2 OKAY0.585
sum_15x0_true-unreach-call.c below 2 PASS0.58
sum_20x0_false-unreach-call.c below 2 OKAY0.544
sum_20x0_true-unreach-call.c below 2 PASS0.541
sum_25x0_false-unreach-call.c below 2 OKAY0.59
sum_25x0_true-unreach-call.c below 2 PASS0.573
sum_2x3_false-unreach-call.c below 2 OKAY0.554
sum_2x3_true-unreach-call.c below 2 PASS0.547
sum_non_eq_false-unreach-call.c below 2 OKAY0.563
sum_non_eq_true-unreach-call.c below 2 PASS0.573
sum_non_false-unreach-call.c below 2 OKAY0.581
sum_non_true-unreach-call.c below 2 PASS0.565
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.608
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-lit
rec-afnp2014_true-unreach-call.c below 2 PASS0.577
rec-bhmr2007_true-unreach-call.c below 2 PASS0.557
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.07
rec-cggmp2005_true-unreach-call.c below 2 PASS0.504
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.534
rec-css2003_true-unreach-call.c below 2 PASS1.481
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.14
rec-gj2007b_true-unreach-call.c below 2 FAIL0.517
rec-gj2007_true-unreach-call.c below 2 FAIL0.673
rec-gr2006_true-unreach-call.c below 2 FAIL0.668
rec-gsv2008_true-unreach-call.c below 2 PASS0.538
rec-hhk2008_true-unreach-call.c below 2 PASS0.524
rec-jm2006_true-unreach-call.c below 2 PASS0.669
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.718
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.627
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.801
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c below 2 PASS0.465
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.554
rec-count_by_2_true-unreach-call.c below 2 PASS0.465
rec-count_by_k_true-unreach-call.c below 2 PASS0.48
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.514
rec-gauss_sum_true-unreach-call.c below 2 PASS0.549
rec-half_true-unreach-call.c below 2 FAIL0.536
rec-nested_true-unreach-call.c below 3 FAIL0.86
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.423
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.649
cubic_polynomial_unsafe.c below 2 OKAY0.634
edit_distance_bottom_up.c below 3 FAIL189.36
edit_distance_top_down.c below 3 FAIL5.13
log_log_n_solution.c below 3 FAIL0.599
log_log_n_solution_unsafe.c below 3 OKAY0.591
log_n_solution.c below 2 FAIL0.606
log_n_solution_unsafe.c below 2 OKAY0.617
multivariate_1.c below TIMEOUT 300.1
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL3.498
multivariate_higher_order_unsafe.c below 7 OKAY3.584
n_cubed_solution.c below EXCEPTION 100.931
n_cubed_solution_unsafe.c below EXCEPTION 0.025
n_log_n_solution.c below 8 FAIL1.6
n_log_n_solution_unsafe.c below 8 OKAY1.579
n_squared_two_base_case_even.c below 2 PASS0.702
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.688
n_squared_two_base_case_odd.c below 2 PASS0.694
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.721
pascals_dynamic.c below 3 FAIL2.679
pascals_dynamic_unsafe.c below 3 OKAY2.717
pascals_iterative.c below 1 FAIL5.005
pascals_iterative_unsafe.c below 1 OKAY4.856
pascals_recursive.c below 8 FAIL3.633
pascals_recursive_unsafe.c below 8 OKAY3.641
squared_solution.c below 8 FAIL3.161
squared_solution_unsafe.c below 8 OKAY3.158
two_n_even.c below 2 PASS0.524
two_n_even_unsafe.c below 2 OKAY0.528
two_n_odd.c below 2 PASS0.515
two_n_odd_unsafe.c below 2 OKAY0.528
two_to_n_over_two_even.c below 7 FAIL293.915
two_to_n_over_two_even_unsafe.c below 7 OKAY136.639
two_to_n_over_two_odd.c below 7 FAIL245.976
two_to_n_over_two_odd_unsafe.c below 7 OKAY150.144
two_to_n_squared.c below 5 FAIL20.13
two_to_n_squared_unsafe.c below 5 OKAY21.802
two_to_two_to_n.c below 7 FAIL1.487
two_to_two_to_n_unsafe.c below 7 OKAY1.546
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1814.898
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.461
adding_and_mult_unsafe.c below 1 OKAY0.466
binary_search_array_tree.c below 1 FAIL0.816
exp_add_linear.c below 1 PASS0.567
exp_add_linear_unsafe.c below 1 OKAY0.575
exp_add_loop_rec.c below 1 FAIL0.402
exp_add_loop_rec_unsafe.c below 1 OKAY0.422
exp_add_loop_variable.c below 1 PASS0.529
exp_add_loop_variable_unsafe.c below 1 OKAY0.521
exp_with_linear_inner_loop.c below 1 FAIL0.632
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.647
halving_log1.c below 1 FAIL0.693
linear_two_to_n.c below 7 FAIL1.754
linear_two_to_n_unsafe.c below 7 OKAY1.728
loop_five_to_n.c below 1 PASS0.493
loop_five_to_n_unsafe.c below 1 OKAY0.483
non_loop_five_to_n.c below 7 FAIL55.328
non_loop_five_to_n_unsafe.c below 7 OKAY56.511
power_log_modified.c below 1 PASS0.729
simple_exponential.c below 1 PASS0.482
simple_exponential_for.c below 1 PASS0.503
simple_exponential_for_unsafe.c below 1 OKAY0.499
simple_exponential_unsafe.c below 1 OKAY0.48
two_to_n_minus_n.c below 7 FAIL2.585
two_to_n_minus_n_loop.c below TIMEOUT 300.005
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.007
two_to_n_minus_n_unsafe.c below 7 OKAY2.393
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 730.711
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.706
02.c below 3 FAIL0.898
03.c below 1 PASS0.551
04.c below 1 PASS0.397
05.c below 3 PASS1.291
06.c below 3 FAIL10.2
07.c below 3 PASS0.758
08.c below 3 PASS1.649
09.c below 3 PASS1.153
10.c below 3 FAIL1.319
11.c below 1 PASS0.424
12.c below 3 PASS1.668
13.c below 3 PASS0.727
14.c below 3 PASS0.639
15.c below 1 PASS0.391
16.c below 1 PASS0.542
17.c below 1 PASS3.629
18.c below 1 PASS0.49
19.c below 1 PASS0.577
20.c below 3 FAIL0.838
21.c below 3 PASS0.689
22.c below 3 FAIL0.917
23.c below 1 PASS0.422
24.c below 1 PASS0.504
25.c below 3 FAIL1.699
26.c below TIMEOUT 300.005
27.c below 1 PASS0.568
28.c below 3 PASS0.696
29.c below 3 PASS1.257
30.c below 1 PASS0.425
31.c below 3 PASS1.374
32.c below 1 FAIL0.444
33.c below 3 PASS1.411
34.c below 1 FAIL0.464
35.c below 1 PASS0.37
36.c below 3 PASS3.082
37.c below 3 FAIL0.714
38.c below 1 FAIL0.463
39.c below 3 PASS0.579
40.c below 3 PASS1.002
41.c below 1 PASS0.464
42.c below 3 PASS1.04
43.c below 3 PASS0.66
44.c below 1 PASS0.437
45.c below 3 FAIL2.996
46.c below 3 FAIL2.044
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 353.573
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.553
AGHKTW2017_foo.c below 1 PASS0.521
AGHKTW2017_loginSafe.c below 1 PASS1.05
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.559
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.596
BCK2011_gauss.c below 1 PASS0.542
BCK2011_strength_reduction.c below 1 PASS0.854
BCK2011_strength_reduction_linear.c below 1 PASS0.573
CFD17-add-const_product.c below 1 PASS0.39
CFD17-add-const_product-syntax.c below 1 PASS0.528
CFD17-add-const_self-comp.c below 1 FAIL0.468
collatz_product-syntax.c below 1 FAIL18.278
collatz_self-comp.c below 1 FAIL2.005
fibonacci_information_flow.c below 1 PASS0.664
halving_log1_product.c below 1 PASS0.768
halving_log1_product-syntax.c below 1 PASS0.866
halving_log1_self-comp.c below 1 FAIL0.61
loop_splitting_test_safe.c below 1 PASS0.695
TA2005_fib2.c below 1 PASS0.681
TA2005_fib.c below 1 PASS0.563
top-level-if-add-const_product.c below 1 PASS1.051
top-level-if-add-const_self-comp.c below 1 FAIL0.563
ICRA Assertions (True) = 16/21
ICRA Assertions (False) = 1/1
ICRA Time = 33.378
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.849
c3_cleanup_better.c below 3 PASS1.686
c3_cleanup.c below 3 PASS1.714
c3_intermediate.c below 3 PASS1.678
c3_noinv.c below 3 FAIL1.416
doublers.c below 1 FAIL0.685
doublers_easier.c below 3 FAIL1.336
doublers_easy.c below 1 FAIL0.733
exp_mult.c below 1 FAIL0.427
fig1_rotation_unsafe.c below 1 OKAY0.482
guessing_game.c below 3 FAIL0.618
not_P_solvable.c below 1 PASS0.384
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 12.008
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.431
maxequals_linear_1.c below 1 PASS0.636
maxequals_linear_2.c below 1 PASS0.667
maxequals_linear_3.c below 1 FAIL0.427
maxequals_linear_4.c below 1 PASS0.412
maxequals_linear_5.c below 1 PASS0.416
maxequals_linear_6.c below 1 FAIL0.432
maxequals_matrix1.c below 3 FAIL1.595
maxequals_matrix2.c below 3 FAIL1.579
maxequals_quadratic1.c below 1 FAIL0.441
maxequals_quadratic2.c below 1 PASS0.449
maxequals_stratified1.c below 3 PASS4.893
maxequals_stratified2.c below 3 PASS5.184
maxequals_stratified3.c below 3 FAIL5.283
nine.c below 1 FAIL0.437
nine_nondecreasing.c below 1 PASS0.691
sum_interval_1.c below 1 FAIL0.518
sum_interval_2.c below 1 FAIL0.488
sum_interval_3.c below 1 FAIL0.49
TrackingObjectFields.c below 3 PASS11.045
TrackingObjectFields_inlined.c below 1 PASS3.214
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 39.728
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.501
bobble2_varloop.c below 1 PASS0.485
bobble3.c below TIMEOUT 300.005
bobble4.c below 1 FAIL0.467
bobble5.c below 1 FAIL0.46
bobble.c below 1 PASS0.465
inchworm2.c below 1 TIMEOUT300.006
inchworm3.c below 1 PASS0.489
inchworm4.c below 1 PASS0.498
inchworm5.c below 1 PASS0.487
inchworm6_unsafe.c below 1 OKAY0.467
inchworm.c below 1 FAIL0.444
leapdiff2.c below 1 TIMEOUT300.005
leapfrog_annotated.c below 1 FAIL0.483
leapfrog_annotated_disjunction.c below 1 PASS0.476
leapfrog_asymmetric2.c below 1 FAIL0.532
leapfrog_asymmetric3.c below 1 FAIL0.552
leapfrog_asymmetric.c below 1 FAIL0.482
leapfrog.c below 1 FAIL0.44
leapfrog_materialized.c below 1 FAIL0.505
leapfrog_verbose.c below 1 FAIL0.489
leapspin.c below 1 FAIL0.395
leapsum2.c below 1 TIMEOUT300.006
leapthree.c below 1 FAIL0.477
microbobble2.c below 1 PASS0.453
microbobble3.c below 1 PASS0.442
microbobble_asymmetric.c below 1 PASS0.444
microbobble.c below 1 FAIL0.437
simple_bl2.c below 1 FAIL0.487
simple_bl3.c below 1 FAIL0.397
simple_bl.c below 1 FAIL0.471
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1212.747
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.345
binval_example_2_unsafe.c below 1 OKAY0.359
binval_example_3_unsafe.c below 1 OKAY0.35
binval_example_4.c below 1 PASS0.42
binval_example_4_unsafe.c below 1 OKAY0.408
binval_example_5.c below 1 FAIL1.589
binval_example_5_unsafe.c below 1 OKAY3.736
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.207