[Version Information]
WALi-OpenNWA version: 3673b90a57074c9f370793780d59fdd8e92f61a6 (2018-02-20 22:40:05 -0600) "Merge branch 'NewtonDuetGaussian' of https://github.com/WaliDev/WALi-OpenNWA into NewtonDuetGaussian"
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.419
kmp.c below 1 PASS1.353
qsort.c below 4 PASS1.296
speed_pldi09_fig1.c below 1 PASS0.678
speed_pldi09_fig4_2.c below 1 FAIL0.454
speed_pldi09_fig4_4.c below 1 PASS0.63
speed_pldi09_fig4_5.c below 1 PASS0.489
speed_pldi10_ex1.c below 1 PASS1.722
speed_pldi10_ex3.c below 1 PASS0.702
speed_pldi10_ex4.c below 1 PASS0.756
speed_popl10_fig2_1.c below 1 PASS0.632
speed_popl10_fig2_2.c below 1 FAIL0.443
speed_popl10_nested_multiple.c below 1 PASS0.58
speed_popl10_nested_single.c below 1 PASS0.538
speed_popl10_sequential_single.c below 1 PASS0.517
speed_popl10_simple_multiple.c below 1 PASS0.739
speed_popl10_simple_single_2.c below 1 PASS0.928
speed_popl10_simple_single.c below 1 PASS0.421
t07.c below 1 PASS0.577
t08.c below 1 PASS0.483
t09.c below 1 PASS0.447
t10.c below 1 PASS0.435
t11.c below 1 PASS0.629
t13.c below 1 FAIL0.558
t15.c below 1 PASS0.549
t16.c below 1 PASS0.499
t19.c below 1 PASS0.508
t20.c below 1 PASS0.469
t27.c below 1 PASS0.76
t28.c below 1 PASS0.722
t30.c below 1 FAIL0.494
t37.c below 2 PASS0.897
t39.c below 2 PASS0.794
t46.c below 1 PASS0.527
t47.c below 1 PASS0.668
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.313
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.506
qsort_full.c below 4 PASS11.765
rec1-param_safe.c below 2 PASS0.522
rec1-param_unsafe.c below 2 OKAY0.514
rec1_safe.c below 2 PASS0.5
rec1_unsafe.c below 2 OKAY0.478
rec2-param_safe.c below 2 PASS0.496
rec2-param_unsafe.c below 2 OKAY0.477
rec2_safe.c below 2 PASS0.488
rec2_unsafe.c below 2 OKAY0.473
rec-test.c below 2 PASS0.47
sas03_bothbranches.c below 7 PASS1.252
sas03.c below 2 PASS0.902
simulated_lese_recursive.c below 2 PASS0.646
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.489
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.388
count_up_down_unsafe.c below 1 OKAY0.398
divide.c below 1 PASS0.408
factor_unsafe.c below 1 OKAY0.369
for_infinite_loop_1_safe.c below 1 PASS0.362
for_infinite_loop_2_safe.c below 1 PASS0.37
interproc.c below 1 PASS0.326
mult.c below 1 PASS0.384
pointer_arith.c below 1 PASS0.338
quotient.c below 3 PASS0.705
subtract.c below 1 PASS0.367
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.38
sum01_bug02_unsafe.c below 1 OKAY0.729
sum01_real_safe.c below 1 PASS0.386
sum01_safe.c below 1 PASS0.406
sum01_unsafe.c below 1 OKAY0.578
sum02_safe.c below 1 PASS0.412
sum03_safe.c below 1 PASS0.492
sum03_unsafe.c below 1 OKAY0.59
sum04_safe.c below 1 PASS0.41
sum04_unsafe.c below 1 OKAY0.613
terminator_02_safe.c below 1 PASS0.338
terminator_02_unsafe.c below 1 OKAY0.411
terminator_03_safe.c below 1 PASS0.372
terminator_03_unsafe.c below 1 OKAY0.38
token_ring01_safe.c below 4 FAIL124.376
token_ring01_unsafe.c below 4 OKAY194.12
toy_safe.c below EXCEPTION 126.663
trex01_safe.c below 1 PASS0.811
trex01_unsafe.c below 1 OKAY0.454
trex02_safe2.c below 3 PASS0.593
trex02_safe.c below 3 PASS0.535
trex02_unsafe.c below 3 OKAY0.533
trex03_safe.c below 1 PASS0.51
trex03_unsafe.c below 1 OKAY0.522
trex04_safe.c below 1 PASS0.375
while_infinite_loop_1_safe.c below 1 PASS0.328
while_infinite_loop_2_safe.c below 1 PASS0.341
while_infinite_loop_3_safe.c below 1 PASS0.337
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 461.41
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.545
blogger_simplified1.c below 3 PASS1.687
divided_difference2.c below TIMEOUT 300.009
mult-proc.c below 3 PASS0.521
mult-proc-params.c below 3 PASS0.546
popall.c below 1 PASS0.933
simulated_scc.c below 1 PASS0.865
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.106
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.411
degree2_binomial.c below 1 PASS0.866
degree2_monomial.c below 1 PASS0.469
degree3_binomial.c below 1 FAIL4.888
degree3_monomial.c below 1 PASS0.956
degree4_binomial.c below 1 FAIL5.095
degree4_monomial.c below 1 PASS1.623
degree5_binomial.c below 1 FAIL16.205
degree5_monomial.c below 1 PASS3.031
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 33.544
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.519
cubic_with_square_interproc.c below 2 FAIL0.716
cubic_with_square_nonlinear.c below 1 FAIL0.659
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.74
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.657
cubic_with_square_unsafe.c below 1 OKAY0.524
multi-input.c below 1 FAIL10.364
multi-input_unsafe.c below 1 OKAY10.15
nondet_loop_bound.c below 1 FAIL0.581
nondet_loop_bound_quartic.c below 1 FAIL0.723
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.778
nondet_loop_bound_unsafe.c below 1 OKAY0.581
nonlinear_stratified.c below 1 PASS123.846
nonlinear_stratified_unsafe.c below 1 OKAY67.119
quartic_with_cube.c below 1 FAIL0.676
quartic_with_cube_nonlinear.c below 1 FAIL1.002
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.966
quartic_with_cube_unsafe.c below 1 OKAY0.559
quintic_with_quartic.c below 1 PASS1.071
quintic_with_quartic_nonlinear.c below 1 PASS1.19
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.142
quintic_with_quartic_unsafe.c below 1 OKAY1.123
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 225.686
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.001
degree2_FD_AllAux_AllAssm.c below 1 PASS102.303
degree2_FD_AllAux_FewAssm.c below 1 PASS6.974
degree2_FD_FewAux_FewAssm.c below 1 PASS1.346
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.369
degree3.c below 1 PASS1.133
degree3_FD.c below 1 PASS1.232
degree4.c below 1 PASS1.883
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 117.241
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.533
loop_unsafe.c below 1 OKAY0.519
simulated_lese_parser.c below 1 PASS0.399
simulated_lese_sentinel.c below 1 PASS0.397
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.397
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.397
/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.384
array_false-unreach-call2.c below 1 OKAY0.403
array_false-unreach-call3.c below 1 OKAY0.399
array_true-unreach-call1.c below 1 FAIL0.396
array_true-unreach-call2.c below 1 FAIL0.399
array_true-unreach-call3.c below 1 PASS0.405
array_true-unreach-call4.c below 1 FAIL0.382
const_false-unreach-call1.c below 1 OKAY0.405
const_true-unreach-call1.c below 1 PASS0.403
diamond_false-unreach-call1.c below 1 OKAY0.382
diamond_true-unreach-call1.c below 1 PASS0.387
diamond_true-unreach-call2.c below 1 PASS0.411
functions_false-unreach-call1.c below 3 OKAY0.515
functions_true-unreach-call1.c below 3 PASS0.526
multivar_false-unreach-call1.c below 1 OKAY0.421
multivar_true-unreach-call1.c below 1 PASS0.41
nested_false-unreach-call1.c below 1 OKAY0.478
nested_true-unreach-call1.c below 1 PASS0.465
overflow_true-unreach-call1.c below 1 PASS0.354
phases_false-unreach-call1.c below 1 OKAY0.488
phases_false-unreach-call2.c below 1 OKAY0.397
phases_true-unreach-call1.c below 1 PASS0.483
phases_true-unreach-call2.c below 1 PASS0.39
simple_false-unreach-call1.c below 1 OKAY0.367
simple_false-unreach-call2.c below 1 OKAY0.36
simple_false-unreach-call3.c below 1 OKAY0.36
simple_false-unreach-call4.c below 1 OKAY0.375
simple_true-unreach-call1.c below 1 PASS0.363
simple_true-unreach-call2.c below 1 PASS0.361
simple_true-unreach-call3.c below 1 PASS0.365
simple_true-unreach-call4.c below 1 PASS0.356
underapprox_false-unreach-call1.c below 1 OKAY0.412
underapprox_false-unreach-call2.c below 1 OKAY0.392
underapprox_true-unreach-call1.c below 1 FAIL0.402
underapprox_true-unreach-call2.c below 1 PASS0.449
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.245
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.658
apache-get-tag_true-unreach-call.c below 1 FAIL0.581
down_true-unreach-call.c below 1 PASS0.473
fragtest_simple_true-unreach-call.c below 1 PASS0.585
half_2_true-unreach-call.c below 1 PASS0.472
heapsort_true-unreach-call.c below 1 PASS2.261
id_build_true-unreach-call.c below 1 PASS0.442
id_trans_false-unreach-call.c below 1 OKAY0.37
id_trans_true-unreach-call.c below 1 PASS0.389
large_const_true-unreach-call.c below 1 PASS0.526
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.448
nested6_true-unreach-call.c below 1 FAIL0.64
nested9_true-unreach-call.c below 1 PASS0.691
nest-if3_true-unreach-call.c below 1 PASS0.56
NetBSD_loop_true-unreach-call.c below 1 PASS0.384
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.5
seq_true-unreach-call.c below 1 PASS0.551
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.607
string_concat-noarr_true-unreach-call.c below 1 PASS0.499
up_true-unreach-call.c below 1 PASS0.48
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.117
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.427
bhmr2007_true-unreach-call.c below 1 PASS0.451
cggmp2005b_true-unreach-call.c below 1 PASS0.629
cggmp2005_true-unreach-call.c below 1 PASS0.412
cggmp2005_variant_true-unreach-call.c below 1 PASS0.409
css2003_true-unreach-call.c below 1 PASS1.111
ddlm2013_true-unreach-call.c below 1 PASS0.624
gcnr2008_false-unreach-call.c below 1 OKAY1.119
gj2007b_true-unreach-call.c below 1 FAIL0.434
gj2007_true-unreach-call.c below 1 PASS0.582
gr2006_true-unreach-call.c below 1 PASS0.558
gsv2008_true-unreach-call.c below 1 PASS0.4
hhk2008_true-unreach-call.c below 1 PASS0.382
jm2006_true-unreach-call.c below 1 PASS0.532
jm2006_variant_true-unreach-call.c below 1 PASS0.633
mcmillan2006_true-unreach-call.c below 1 FAIL0.461
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.164
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.364
count_by_1_variant_true-unreach-call.c below 1 PASS0.463
count_by_2_true-unreach-call.c below 1 PASS0.385
count_by_k_true-unreach-call.c below 1 PASS0.369
count_by_nondet_true-unreach-call.c below 1 PASS0.393
gauss_sum_true-unreach-call.c below 1 PASS0.432
half_true-unreach-call.c below 1 FAIL0.427
nested_true-unreach-call.c below 1 PASS0.516
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.349
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.432
array_true-unreach-call.c below 1 FAIL0.442
bubble_sort_false-unreach-call.c below 4 OKAY77.782
bubble_sort_true-unreach-call.c below 1 PASS5.11
compact_false-unreach-call.c below 1 OKAY0.451
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.389
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.41
eureka_01_false-unreach-call.c below 1 OKAY2.707
eureka_01_true-unreach-call.c below 1 FAIL1.578
eureka_05_true-unreach-call.c below 1 FAIL0.879
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.367
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.39
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.364
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.351
heavy_false-unreach-call.c below 1 OKAY0.612
heavy_true-unreach-call.c below 1 PASS0.589
insertion_sort_false-unreach-call.c below 1 OKAY1.556
insertion_sort_true-unreach-call.c below 1 FAIL0.638
invert_string_false-unreach-call.c below 1 OKAY0.597
invert_string_true-unreach-call.c below 1 FAIL0.623
linear_sea.ch_true-unreach-call.c below 1 FAIL0.414
linear_search_false-unreach-call.c below 1 OKAY0.45
lu.cmp_true-unreach-call.c below 3 PASS27.19
ludcmp_false-unreach-call.c below 3 OKAY27.222
matrix_false-unreach-call_true-termination.c below 1 OKAY1.366
matrix_true-unreach-call_true-termination.c below 1 FAIL0.507
n.c11_true-unreach-call.c below 3 FAIL0.585
n.c24_false-unreach-call.c below 3 OKAY5.183
n.c40_true-unreach-call.c below 1 FAIL0.414
nec11_false-unreach-call.c below 1 OKAY0.401
nec20_false-unreach-call.c below 1 OKAY0.434
nec40_true-unreach-call.c below 1 FAIL0.398
string_false-unreach-call.c below 1 OKAY0.778
string_true-unreach-call.c below 1 FAIL0.734
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.717
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.386
sum01_false-unreach-call_true-termination.c below 1 OKAY0.558
sum01_true-unreach-call_true-termination.c below 1 PASS0.397
sum03_false-unreach-call_true-termination.c below 1 OKAY0.649
sum03_true-unreach-call_false-termination.c below 1 PASS0.516
sum04_false-unreach-call_true-termination.c below 1 OKAY0.6
sum04_true-unreach-call_true-termination.c below 1 PASS0.398
sum_array_false-unreach-call.c below 1 OKAY0.67
sum_array_true-unreach-call.c below 1 FAIL0.699
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.347
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.611
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.432
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.364
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.371
trex01_false-unreach-call_true-termination.c below 3 OKAY0.654
trex01_true-unreach-call.c below 3 PASS0.905
trex02_false-unreach-call_true-termination.c below 3 OKAY0.541
trex02_true-unreach-call_true-termination.c below 3 PASS0.54
trex03_false-unreach-call_true-termination.c below 3 OKAY0.864
trex03_true-unreach-call.c below 3 PASS0.875
trex04_true-unreach-call_false-termination.c below 1 PASS0.439
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.4
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.225
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.419
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.412
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.012
vogal_false-unreach-call.c below 1 OKAY0.945
vogal_true-unreach-call.c below 1 FAIL0.968
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.334
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.332
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.334
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.348
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 194.605
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.543
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.518
Ackermann03_true-unreach-call.c below 7 FAIL1.586
Ackermann04_true-unreach-call.c below 7 FAIL1.598
Addition01_true-unreach-call_true-termination.c below 2 PASS0.834
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.797
Addition03_false-no-overflow.c below 2 PASS0.79
Addition03_true-unreach-call.c below 2 PASS0.839
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.604
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.559
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.579
Fibonacci01_true-unreach-call.c below TIMEOUT 300.005
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.005
gcd01_true-unreach-call_true-termination.c below 2 PASS0.744
gcd02_true-unreach-call.c below 2 FAIL1.363
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.242
McCarthy91_true-unreach-call.c below 7 FAIL1.258
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.76
Primes_true-unreach-call.c below 3 FAIL2.199
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.495
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.506
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.522
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.36
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.581
afterrec_2calls_true-unreach-call.c below 2 PASS0.566
afterrec_false-unreach-call.c below 2 OKAY0.46
afterrec_true-unreach-call.c below 2 PASS0.481
fibo_10_false-unreach-call.c below TIMEOUT 300.006
fibo_10_true-unreach-call.c below TIMEOUT 300.004
fibo_15_false-unreach-call.c below TIMEOUT 300.005
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.005
fibo_25_false-unreach-call.c below TIMEOUT 300.005
fibo_25_true-unreach-call.c below TIMEOUT 300.004
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.014
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.006
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.004
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.005
fibo_5_false-unreach-call.c below TIMEOUT 300.004
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.006
id2_b2_o3_true-unreach-call.c below 2 PASS0.948
id2_b3_o2_false-unreach-call.c below 2 OKAY0.952
id2_b3_o5_true-unreach-call.c below 2 PASS0.915
id2_b5_o10_true-unreach-call.c below 2 PASS0.931
id2_i5_o5_false-unreach-call.c below 2 OKAY0.581
id2_i5_o5_true-unreach-call.c below 2 PASS0.562
id_b2_o3_true-unreach-call.c below 2 PASS0.819
id_b3_o2_false-unreach-call.c below 2 OKAY0.834
id_b3_o5_true-unreach-call.c below 2 PASS0.832
id_b5_o10_true-unreach-call.c below 2 PASS0.873
id_i10_o10_false-unreach-call.c below 2 OKAY0.524
id_i10_o10_true-unreach-call.c below 2 PASS0.51
id_i15_o15_false-unreach-call.c below 2 OKAY0.521
id_i15_o15_true-unreach-call.c below 2 PASS0.507
id_i20_o20_false-unreach-call.c below 2 OKAY0.514
id_i20_o20_true-unreach-call.c below 2 PASS0.519
id_i25_o25_false-unreach-call.c below 2 OKAY0.512
id_i25_o25_true-unreach-call.c below 2 PASS0.519
id_i5_o5_false-unreach-call.c below 2 OKAY0.505
id_i5_o5_true-unreach-call.c below 2 PASS0.513
id_o1000_false-unreach-call.c below 2 OKAY0.519
id_o100_false-unreach-call.c below 2 OKAY0.509
id_o10_false-unreach-call.c below 2 OKAY0.496
id_o200_false-unreach-call.c below 2 OKAY0.497
id_o20_false-unreach-call.c below 2 OKAY0.501
id_o3_false-unreach-call.c below 2 OKAY0.505
sum_10x0_false-unreach-call.c below 2 OKAY0.562
sum_10x0_true-unreach-call.c below 2 PASS0.57
sum_15x0_false-unreach-call.c below 2 OKAY0.563
sum_15x0_true-unreach-call.c below 2 PASS0.583
sum_20x0_false-unreach-call.c below 2 OKAY0.574
sum_20x0_true-unreach-call.c below 2 PASS0.574
sum_25x0_false-unreach-call.c below 2 OKAY0.562
sum_25x0_true-unreach-call.c below 2 PASS0.577
sum_2x3_false-unreach-call.c below 2 OKAY0.566
sum_2x3_true-unreach-call.c below 2 PASS0.553
sum_non_eq_false-unreach-call.c below 2 OKAY0.571
sum_non_eq_true-unreach-call.c below 2 PASS0.566
sum_non_false-unreach-call.c below 2 OKAY0.569
sum_non_true-unreach-call.c below 2 PASS0.555
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.622
/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.574
rec-bhmr2007_true-unreach-call.c below 2 PASS0.574
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.091
rec-cggmp2005_true-unreach-call.c below 2 PASS0.506
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.551
rec-css2003_true-unreach-call.c below 2 PASS1.43
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.097
rec-gj2007b_true-unreach-call.c below 2 FAIL0.513
rec-gj2007_true-unreach-call.c below 2 FAIL0.662
rec-gr2006_true-unreach-call.c below 2 FAIL0.665
rec-gsv2008_true-unreach-call.c below 2 PASS0.556
rec-hhk2008_true-unreach-call.c below 2 PASS0.52
rec-jm2006_true-unreach-call.c below 2 PASS0.634
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.717
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.625
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.719
/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.469
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.549
rec-count_by_2_true-unreach-call.c below 2 PASS0.467
rec-count_by_k_true-unreach-call.c below 2 PASS0.479
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.528
rec-gauss_sum_true-unreach-call.c below 2 PASS0.546
rec-half_true-unreach-call.c below 2 FAIL0.543
rec-nested_true-unreach-call.c below 3 FAIL0.851
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.432
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.61
cubic_polynomial_unsafe.c below 2 OKAY0.633
edit_distance_bottom_up.c below 3 FAIL189.014
edit_distance_top_down.c below 3 FAIL5.137
log_log_n_solution.c below 3 FAIL0.607
log_log_n_solution_unsafe.c below 3 OKAY0.575
log_n_solution.c below 2 FAIL0.594
log_n_solution_unsafe.c below 2 OKAY0.586
multivariate_1.c below TIMEOUT 300.094
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL3.463
multivariate_higher_order_unsafe.c below 7 OKAY3.495
n_cubed_solution.c below EXCEPTION 100.918
n_cubed_solution_unsafe.c below EXCEPTION 0.024
n_log_n_solution.c below 8 FAIL1.607
n_log_n_solution_unsafe.c below 8 OKAY1.605
n_squared_two_base_case_even.c below 2 PASS0.697
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.721
n_squared_two_base_case_odd.c below 2 PASS0.7
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.719
pascals_dynamic.c below 3 FAIL2.66
pascals_dynamic_unsafe.c below 3 OKAY2.678
pascals_iterative.c below 1 FAIL4.912
pascals_iterative_unsafe.c below 1 OKAY4.856
pascals_recursive.c below 8 FAIL3.619
pascals_recursive_unsafe.c below 8 OKAY3.636
squared_solution.c below 8 FAIL3.101
squared_solution_unsafe.c below 8 OKAY3.097
two_n_even.c below 2 PASS0.529
two_n_even_unsafe.c below 2 OKAY0.547
two_n_odd.c below 2 PASS0.54
two_n_odd_unsafe.c below 2 OKAY0.533
two_to_n_over_two_even.c below 7 FAIL126.377
two_to_n_over_two_even_unsafe.c below 7 OKAY146.153
two_to_n_over_two_odd.c below 7 FAIL245.133
two_to_n_over_two_odd_unsafe.c below 7 OKAY147.5
two_to_n_squared.c below 5 FAIL19.761
two_to_n_squared_unsafe.c below 5 OKAY19.784
two_to_two_to_n.c below 7 FAIL1.417
two_to_two_to_n_unsafe.c below 7 OKAY1.483
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1650.121
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.414
adding_and_mult_unsafe.c below 1 OKAY0.413
binary_search_array_tree.c below 1 FAIL0.812
exp_add_linear.c below 1 PASS0.52
exp_add_linear_unsafe.c below 1 OKAY0.529
exp_add_loop_rec.c below 1 FAIL0.411
exp_add_loop_rec_unsafe.c below 1 OKAY0.407
exp_add_loop_variable.c below 1 PASS0.494
exp_add_loop_variable_unsafe.c below 1 OKAY0.492
exp_with_linear_inner_loop.c below 1 FAIL0.631
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.616
halving_log1.c below 1 FAIL0.688
linear_two_to_n.c below 7 FAIL1.728
linear_two_to_n_unsafe.c below 7 OKAY1.718
loop_five_to_n.c below 1 PASS0.477
loop_five_to_n_unsafe.c below 1 OKAY0.486
non_loop_five_to_n.c below 7 FAIL54.876
non_loop_five_to_n_unsafe.c below 7 OKAY55.012
power_log_modified.c below 1 PASS0.678
simple_exponential.c below 1 PASS0.465
simple_exponential_for.c below 1 PASS0.466
simple_exponential_for_unsafe.c below 1 OKAY0.498
simple_exponential_unsafe.c below 1 OKAY0.466
two_to_n_minus_n.c below 7 FAIL2.377
two_to_n_minus_n_loop.c below TIMEOUT 300.004
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.007
two_to_n_minus_n_unsafe.c below 7 OKAY2.499
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 728.184
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.722
02.c below 3 FAIL0.994
03.c below 1 PASS0.56
04.c below 1 PASS0.428
05.c below 3 PASS1.357
06.c below 3 FAIL10.582
07.c below 3 PASS0.741
08.c below 3 PASS1.681
09.c below 3 PASS1.193
10.c below 3 FAIL1.328
11.c below 1 PASS0.432
12.c below 3 PASS1.679
13.c below 3 PASS0.748
14.c below 3 PASS0.595
15.c below 1 PASS0.386
16.c below 1 PASS0.55
17.c below 1 PASS3.66
18.c below 1 PASS0.478
19.c below 1 PASS0.583
20.c below 3 FAIL0.822
21.c below 3 PASS0.721
22.c below 3 FAIL0.989
23.c below 1 PASS0.47
24.c below 1 PASS0.514
25.c below 3 FAIL1.858
26.c below TIMEOUT 300.006
27.c below 1 PASS0.549
28.c below 3 PASS0.702
29.c below 3 PASS1.182
30.c below 1 PASS0.415
31.c below 3 PASS1.288
32.c below 1 FAIL0.43
33.c below 3 PASS1.394
34.c below 1 FAIL0.458
35.c below 1 PASS0.369
36.c below 3 PASS2.9
37.c below 3 FAIL0.665
38.c below 1 FAIL0.464
39.c below 3 PASS0.556
40.c below 3 PASS0.992
41.c below 1 PASS0.454
42.c below 3 PASS0.994
43.c below 3 PASS0.687
44.c below 1 PASS0.429
45.c below 3 FAIL2.9
46.c below 3 FAIL2.055
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 353.96
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.517
AGHKTW2017_foo.c below 1 PASS0.509
AGHKTW2017_loginSafe.c below 1 PASS1.032
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.591
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.575
BCK2011_gauss.c below 1 PASS0.528
BCK2011_strength_reduction.c below 1 PASS0.823
BCK2011_strength_reduction_linear.c below 1 PASS0.532
CFD17-add-const_product.c below 1 PASS0.384
CFD17-add-const_product-syntax.c below 1 PASS0.508
CFD17-add-const_self-comp.c below 1 FAIL0.477
collatz_product-syntax.c below 1 FAIL18.003
collatz_self-comp.c below 1 FAIL1.95
fibonacci_information_flow.c below 1 PASS0.696
halving_log1_product.c below 1 PASS0.805
halving_log1_product-syntax.c below 1 PASS0.879
halving_log1_self-comp.c below 1 FAIL0.589
loop_splitting_test_safe.c below 1 PASS0.693
TA2005_fib2.c below 1 PASS0.733
TA2005_fib.c below 1 PASS0.592
top-level-if-add-const_product.c below 1 PASS1.113
top-level-if-add-const_self-comp.c below 1 FAIL0.591
ICRA Assertions (True) = 16/21
ICRA Assertions (False) = 1/1
ICRA Time = 33.12
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.834
c3_cleanup_better.c below 3 PASS1.783
c3_cleanup.c below 3 PASS1.735
c3_intermediate.c below 3 PASS1.797
c3_noinv.c below 3 FAIL1.484
doublers.c below 1 FAIL0.647
doublers_easier.c below 3 FAIL1.276
doublers_easy.c below 1 FAIL0.756
exp_mult.c below 1 FAIL0.433
fig1_rotation_unsafe.c below 1 OKAY0.465
guessing_game.c below 3 FAIL0.624
not_P_solvable.c below 1 PASS0.383
ICRA Assertions (True) = 5/11
ICRA Assertions (False) = 1/1
ICRA Time = 12.217
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.44
maxequals_linear_1.c below 1 PASS0.645
maxequals_linear_2.c below 1 PASS0.643
maxequals_linear_3.c below 1 FAIL0.438
maxequals_linear_4.c below 1 PASS0.425
maxequals_linear_5.c below 1 PASS0.443
maxequals_linear_6.c below 1 FAIL0.472
maxequals_matrix1.c below 3 FAIL1.708
maxequals_matrix2.c below 3 FAIL1.601
maxequals_quadratic1.c below 1 FAIL0.445
maxequals_quadratic2.c below 1 PASS0.433
maxequals_stratified1.c below 3 PASS4.991
maxequals_stratified2.c below 3 PASS5.535
maxequals_stratified3.c below 3 FAIL5.373
nine.c below 1 FAIL0.457
nine_nondecreasing.c below 1 PASS0.693
sum_interval_1.c below 1 FAIL0.531
sum_interval_2.c below 1 FAIL0.483
sum_interval_3.c below 1 FAIL0.514
TrackingObjectFields.c below 3 PASS11.018
TrackingObjectFields_inlined.c below 1 PASS3.307
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 40.595
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.491
bobble2_varloop.c below 1 PASS0.496
bobble3.c below TIMEOUT 300.004
bobble4.c below 1 FAIL0.486
bobble5.c below 1 FAIL0.501
bobble.c below 1 PASS0.478
inchworm2.c below 1 TIMEOUT300.006
inchworm3.c below 1 PASS0.513
inchworm4.c below 1 PASS0.546
inchworm5.c below 1 PASS0.51
inchworm6_unsafe.c below 1 OKAY0.49
inchworm.c below 1 FAIL0.484
leapdiff2.c below 1 TIMEOUT300.004
leapfrog_annotated.c below 1 FAIL0.481
leapfrog_annotated_disjunction.c below 1 PASS0.48
leapfrog_asymmetric2.c below 1 FAIL0.547
leapfrog_asymmetric3.c below 1 FAIL0.555
leapfrog_asymmetric.c below 1 FAIL0.524
leapfrog.c below 1 FAIL0.464
leapfrog_materialized.c below 1 FAIL0.526
leapfrog_verbose.c below 1 FAIL0.534
leapspin.c below 1 FAIL0.457
leapsum2.c below 1 TIMEOUT300.005
leapthree.c below 1 FAIL0.469
microbobble2.c below 1 PASS0.429
microbobble3.c below 1 PASS0.448
microbobble_asymmetric.c below 1 PASS0.454
microbobble.c below 1 FAIL0.433
simple_bl2.c below 1 FAIL0.476
simple_bl3.c below 1 FAIL0.421
simple_bl.c below 1 FAIL0.485
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1213.197
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.354
binval_example_2_unsafe.c below 1 OKAY0.361
binval_example_3_unsafe.c below 1 OKAY0.347
binval_example_4.c below 1 PASS0.439
binval_example_4_unsafe.c below 1 OKAY0.409
binval_example_5.c below 1 FAIL1.606
binval_example_5_unsafe.c below 1 OKAY3.765
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 7.281