[Version Information]
WALi-OpenNWA version: 69809d4d2d7bd9923495248d4fc353f05cc8d429 (2017-10-31 11:52:44 -0500) "Small cleanup steps to latest suites"
duet version: 00e752f1bd69031eec9553485112adb3c28de7fe (2017-11-02 17:14:55 -0400) "Catch OCRS translation exceptions"
# 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.412
kmp.c below 1 PASS1.375
qsort.c below 4 PASS1.278
speed_pldi09_fig1.c below 1 PASS0.682
speed_pldi09_fig4_2.c below 1 FAIL0.449
speed_pldi09_fig4_4.c below 1 PASS0.644
speed_pldi09_fig4_5.c below 1 PASS0.504
speed_pldi10_ex1.c below 1 PASS1.685
speed_pldi10_ex3.c below 1 PASS0.694
speed_pldi10_ex4.c below 1 PASS0.747
speed_popl10_fig2_1.c below 1 PASS0.614
speed_popl10_fig2_2.c below 1 FAIL0.426
speed_popl10_nested_multiple.c below 1 PASS0.569
speed_popl10_nested_single.c below 1 PASS0.545
speed_popl10_sequential_single.c below 1 PASS0.49
speed_popl10_simple_multiple.c below 1 PASS0.716
speed_popl10_simple_single_2.c below 1 PASS0.92
speed_popl10_simple_single.c below 1 PASS0.39
t07.c below 1 PASS0.556
t08.c below 1 PASS0.482
t09.c below 1 PASS0.447
t10.c below 1 PASS0.442
t11.c below 1 PASS0.637
t13.c below 1 FAIL0.527
t15.c below 1 PASS0.514
t16.c below 1 PASS0.491
t19.c below 1 PASS0.498
t20.c below 1 PASS0.456
t27.c below 1 PASS0.761
t28.c below 1 PASS0.727
t30.c below 1 FAIL0.479
t37.c below 2 PASS0.918
t39.c below 2 PASS0.767
t46.c below 1 PASS0.528
t47.c below 1 PASS0.681
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.051
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.498
qsort_full.c below 4 PASS11.938
rec1-param_safe.c below 2 PASS0.527
rec1-param_unsafe.c below 2 OKAY0.502
rec1_safe.c below 2 PASS0.48
rec1_unsafe.c below 2 OKAY0.472
rec2-param_safe.c below 2 PASS0.492
rec2-param_unsafe.c below 2 OKAY0.473
rec2_safe.c below 2 PASS0.465
rec2_unsafe.c below 2 OKAY0.466
rec-test.c below 2 PASS0.455
sas03_bothbranches.c below 7 PASS1.224
sas03.c below 2 PASS0.893
simulated_lese_recursive.c below 2 PASS0.61
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.495
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.389
count_up_down_unsafe.c below 1 OKAY0.399
divide.c below 1 PASS0.399
factor_unsafe.c below 1 OKAY0.38
for_infinite_loop_1_safe.c below 1 PASS0.366
for_infinite_loop_2_safe.c below 1 PASS0.366
interproc.c below 1 PASS0.337
mult.c below 1 PASS0.381
pointer_arith.c below 1 PASS0.325
quotient.c below 3 PASS0.697
subtract.c below 1 PASS0.378
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.379
sum01_bug02_unsafe.c below 1 OKAY0.738
sum01_real_safe.c below 1 PASS0.376
sum01_safe.c below 1 PASS0.384
sum01_unsafe.c below 1 OKAY0.577
sum02_safe.c below 1 PASS0.418
sum03_safe.c below 1 PASS0.492
sum03_unsafe.c below 1 OKAY0.586
sum04_safe.c below 1 PASS0.419
sum04_unsafe.c below 1 OKAY0.613
terminator_02_safe.c below 1 PASS0.367
terminator_02_unsafe.c below 1 OKAY0.425
terminator_03_safe.c below 1 PASS0.371
terminator_03_unsafe.c below 1 OKAY0.37
token_ring01_safe.c below 4 FAIL127.698
token_ring01_unsafe.c below 4 OKAY198.455
toy_safe.c below EXCEPTION 134.939
trex01_safe.c below 1 PASS0.759
trex01_unsafe.c below 1 OKAY0.444
trex02_safe2.c below 3 PASS0.538
trex02_safe.c below 3 PASS0.544
trex02_unsafe.c below 3 OKAY0.542
trex03_safe.c below 1 PASS0.514
trex03_unsafe.c below 1 OKAY0.517
trex04_safe.c below 1 PASS0.393
while_infinite_loop_1_safe.c below 1 PASS0.334
while_infinite_loop_2_safe.c below 1 PASS0.336
while_infinite_loop_3_safe.c below 1 PASS0.335
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 477.28
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.553
blogger_simplified1.c below 3 PASS1.647
divided_difference2.c below TIMEOUT 300.01
mult-proc.c below 3 PASS0.538
mult-proc-params.c below 3 PASS0.548
popall.c below 1 PASS0.937
simulated_scc.c below 1 PASS0.868
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.101
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.429
degree2_binomial.c below 1 PASS0.894
degree2_monomial.c below 1 PASS0.497
degree3_binomial.c below 1 FAIL4.884
degree3_monomial.c below 1 PASS1.007
degree4_binomial.c below 1 FAIL5.283
degree4_monomial.c below 1 PASS1.697
degree5_binomial.c below 1 FAIL16.437
degree5_monomial.c below 1 PASS3.144
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 34.272
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.511
cubic_with_square_interproc.c below 2 FAIL0.731
cubic_with_square_nonlinear.c below 1 FAIL0.671
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.746
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.655
cubic_with_square_unsafe.c below 1 OKAY0.512
multi-input.c below 1 FAIL11.189
multi-input_unsafe.c below 1 OKAY10.937
nondet_loop_bound.c below 1 FAIL0.57
nondet_loop_bound_quartic.c below 1 FAIL0.757
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.773
nondet_loop_bound_unsafe.c below 1 OKAY0.574
nonlinear_stratified.c below 1 PASS129.405
nonlinear_stratified_unsafe.c below 1 OKAY69.972
quartic_with_cube.c below 1 FAIL0.726
quartic_with_cube_nonlinear.c below 1 FAIL1.022
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.977
quartic_with_cube_unsafe.c below 1 OKAY0.564
quintic_with_quartic.c below 1 PASS1.129
quintic_with_quartic_nonlinear.c below 1 PASS1.166
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.173
quintic_with_quartic_unsafe.c below 1 OKAY1.138
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 235.898
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.007
degree2_FD_AllAux_AllAssm.c below 1 PASS109.118
degree2_FD_AllAux_FewAssm.c below 1 PASS7.259
degree2_FD_FewAux_FewAssm.c below 1 PASS1.369
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.459
degree3.c below 1 PASS1.151
degree3_FD.c below 1 PASS1.305
degree4.c below 1 PASS1.906
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 124.574
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.531
loop_unsafe.c below 1 OKAY0.556
simulated_lese_parser.c below 1 PASS0.395
simulated_lese_sentinel.c below 1 PASS0.417
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.899
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.42
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.42
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.007
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.007
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.399
array_false-unreach-call2.c below 1 OKAY0.407
array_false-unreach-call3.c below 1 OKAY0.394
array_true-unreach-call1.c below 1 FAIL0.383
array_true-unreach-call2.c below 1 FAIL0.417
array_true-unreach-call3.c below 1 PASS0.396
array_true-unreach-call4.c below 1 FAIL0.39
const_false-unreach-call1.c below 1 OKAY0.415
const_true-unreach-call1.c below 1 PASS0.419
diamond_false-unreach-call1.c below 1 OKAY0.396
diamond_true-unreach-call1.c below 1 PASS0.396
diamond_true-unreach-call2.c below 1 PASS0.42
functions_false-unreach-call1.c below 3 OKAY0.513
functions_true-unreach-call1.c below 3 PASS0.524
multivar_false-unreach-call1.c below 1 OKAY0.407
multivar_true-unreach-call1.c below 1 PASS0.416
nested_false-unreach-call1.c below 1 OKAY0.446
nested_true-unreach-call1.c below 1 PASS0.455
overflow_true-unreach-call1.c below 1 PASS0.347
phases_false-unreach-call1.c below 1 OKAY0.508
phases_false-unreach-call2.c below 1 OKAY0.389
phases_true-unreach-call1.c below 1 PASS0.503
phases_true-unreach-call2.c below 1 PASS0.384
simple_false-unreach-call1.c below 1 OKAY0.365
simple_false-unreach-call2.c below 1 OKAY0.348
simple_false-unreach-call3.c below 1 OKAY0.359
simple_false-unreach-call4.c below 1 OKAY0.373
simple_true-unreach-call1.c below 1 PASS0.372
simple_true-unreach-call2.c below 1 PASS0.364
simple_true-unreach-call3.c below 1 PASS0.358
simple_true-unreach-call4.c below 1 PASS0.37
underapprox_false-unreach-call1.c below 1 OKAY0.403
underapprox_false-unreach-call2.c below 1 OKAY0.404
underapprox_true-unreach-call1.c below 1 FAIL0.406
underapprox_true-unreach-call2.c below 1 PASS0.397
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.243
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.582
apache-get-tag_true-unreach-call.c below 1 FAIL0.596
down_true-unreach-call.c below 1 PASS0.465
fragtest_simple_true-unreach-call.c below 1 PASS0.594
half_2_true-unreach-call.c below 1 PASS0.507
heapsort_true-unreach-call.c below 1 PASS2.343
id_build_true-unreach-call.c below 1 PASS0.421
id_trans_false-unreach-call.c below 1 OKAY0.371
id_trans_true-unreach-call.c below 1 PASS0.376
large_const_true-unreach-call.c below 1 PASS0.529
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.464
nested6_true-unreach-call.c below 1 FAIL0.659
nested9_true-unreach-call.c below 1 PASS0.719
nest-if3_true-unreach-call.c below 1 PASS0.561
NetBSD_loop_true-unreach-call.c below 1 PASS0.388
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.497
seq_true-unreach-call.c below 1 PASS0.525
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.634
string_concat-noarr_true-unreach-call.c below 1 PASS0.522
up_true-unreach-call.c below 1 PASS0.455
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.208
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.424
bhmr2007_true-unreach-call.c below 1 PASS0.45
cggmp2005b_true-unreach-call.c below 1 PASS0.663
cggmp2005_true-unreach-call.c below 1 PASS0.403
cggmp2005_variant_true-unreach-call.c below 1 PASS0.421
css2003_true-unreach-call.c below 1 PASS1.101
ddlm2013_true-unreach-call.c below 1 PASS0.625
gcnr2008_false-unreach-call.c below 1 OKAY1.147
gj2007b_true-unreach-call.c below 1 FAIL0.443
gj2007_true-unreach-call.c below 1 PASS0.577
gr2006_true-unreach-call.c below 1 PASS0.564
gsv2008_true-unreach-call.c below 1 PASS0.403
hhk2008_true-unreach-call.c below 1 PASS0.393
jm2006_true-unreach-call.c below 1 PASS0.539
jm2006_variant_true-unreach-call.c below 1 PASS0.639
mcmillan2006_true-unreach-call.c below 1 FAIL0.458
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.25
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.38
count_by_1_variant_true-unreach-call.c below 1 PASS0.49
count_by_2_true-unreach-call.c below 1 PASS0.371
count_by_k_true-unreach-call.c below 1 PASS0.363
count_by_nondet_true-unreach-call.c below 1 PASS0.408
gauss_sum_true-unreach-call.c below 1 PASS0.438
half_true-unreach-call.c below 1 FAIL0.431
nested_true-unreach-call.c below 1 PASS0.549
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.43
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.435
array_true-unreach-call.c below 1 FAIL0.449
bubble_sort_false-unreach-call.c below 4 OKAY80.785
bubble_sort_true-unreach-call.c below 1 PASS5.464
compact_false-unreach-call.c below 1 OKAY0.464
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.404
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.405
eureka_01_false-unreach-call.c below 1 OKAY2.768
eureka_01_true-unreach-call.c below 1 FAIL1.637
eureka_05_true-unreach-call.c below 1 FAIL0.887
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.386
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.383
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.352
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.354
heavy_false-unreach-call.c below 1 OKAY0.617
heavy_true-unreach-call.c below 1 PASS0.601
insertion_sort_false-unreach-call.c below 1 OKAY1.573
insertion_sort_true-unreach-call.c below 1 FAIL0.631
invert_string_false-unreach-call.c below 1 OKAY0.603
invert_string_true-unreach-call.c below 1 FAIL0.647
linear_sea.ch_true-unreach-call.c below 1 FAIL0.427
linear_search_false-unreach-call.c below 1 OKAY0.45
lu.cmp_true-unreach-call.c below 3 PASS28.779
ludcmp_false-unreach-call.c below 3 OKAY28.453
matrix_false-unreach-call_true-termination.c below 1 OKAY1.354
matrix_true-unreach-call_true-termination.c below 1 FAIL0.53
n.c11_true-unreach-call.c below 3 FAIL0.595
n.c24_false-unreach-call.c below 3 OKAY5.33
n.c40_true-unreach-call.c below 1 FAIL0.406
nec11_false-unreach-call.c below 1 OKAY0.418
nec20_false-unreach-call.c below 1 OKAY0.433
nec40_true-unreach-call.c below 1 FAIL0.387
string_false-unreach-call.c below 1 OKAY0.769
string_true-unreach-call.c below 1 FAIL0.76
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.728
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.38
sum01_false-unreach-call_true-termination.c below 1 OKAY0.606
sum01_true-unreach-call_true-termination.c below 1 PASS0.402
sum03_false-unreach-call_true-termination.c below 1 OKAY0.643
sum03_true-unreach-call_false-termination.c below 1 PASS0.503
sum04_false-unreach-call_true-termination.c below 1 OKAY0.591
sum04_true-unreach-call_true-termination.c below 1 PASS0.414
sum_array_false-unreach-call.c below 1 OKAY0.661
sum_array_true-unreach-call.c below 1 FAIL0.71
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.364
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.627
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.441
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.379
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.38
trex01_false-unreach-call_true-termination.c below 3 OKAY0.617
trex01_true-unreach-call.c below 3 PASS0.902
trex02_false-unreach-call_true-termination.c below 3 OKAY0.559
trex02_true-unreach-call_true-termination.c below 3 PASS0.531
trex03_false-unreach-call_true-termination.c below 3 OKAY0.884
trex03_true-unreach-call.c below 3 PASS0.868
trex04_true-unreach-call_false-termination.c below 1 PASS0.423
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.398
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.784
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.413
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.406
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.299
vogal_false-unreach-call.c below 1 OKAY0.967
vogal_true-unreach-call.c below 1 FAIL0.953
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.333
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.351
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.339
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.352
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 202.144
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.6
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.575
Ackermann03_true-unreach-call.c below 7 FAIL1.62
Ackermann04_true-unreach-call.c below 7 FAIL1.647
Addition01_true-unreach-call_true-termination.c below 2 PASS0.85
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.859
Addition03_false-no-overflow.c below 2 PASS0.832
Addition03_true-unreach-call.c below 2 PASS0.849
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.607
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.574
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.572
Fibonacci01_true-unreach-call.c below TIMEOUT 300.004
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.007
gcd01_true-unreach-call_true-termination.c below 2 PASS0.767
gcd02_true-unreach-call.c below 2 FAIL1.459
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.261
McCarthy91_true-unreach-call.c below 7 FAIL1.306
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.753
Primes_true-unreach-call.c below 3 FAIL2.287
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.639
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.514
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.518
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1524.116
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.597
afterrec_2calls_true-unreach-call.c below 2 PASS0.559
afterrec_false-unreach-call.c below 2 OKAY0.48
afterrec_true-unreach-call.c below 2 PASS0.47
fibo_10_false-unreach-call.c below TIMEOUT 300.006
fibo_10_true-unreach-call.c below TIMEOUT 300.006
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.006
fibo_25_false-unreach-call.c below TIMEOUT 300.006
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.013
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.006
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.005
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.006
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.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.993
id2_b3_o2_false-unreach-call.c below 2 OKAY0.991
id2_b3_o5_true-unreach-call.c below 2 PASS0.947
id2_b5_o10_true-unreach-call.c below 2 PASS0.982
id2_i5_o5_false-unreach-call.c below 2 OKAY0.539
id2_i5_o5_true-unreach-call.c below 2 PASS0.587
id_b2_o3_true-unreach-call.c below 2 PASS0.825
id_b3_o2_false-unreach-call.c below 2 OKAY0.842
id_b3_o5_true-unreach-call.c below 2 PASS0.809
id_b5_o10_true-unreach-call.c below 2 PASS0.875
id_i10_o10_false-unreach-call.c below 2 OKAY0.515
id_i10_o10_true-unreach-call.c below 2 PASS0.497
id_i15_o15_false-unreach-call.c below 2 OKAY0.515
id_i15_o15_true-unreach-call.c below 2 PASS0.532
id_i20_o20_false-unreach-call.c below 2 OKAY0.521
id_i20_o20_true-unreach-call.c below 2 PASS0.512
id_i25_o25_false-unreach-call.c below 2 OKAY0.506
id_i25_o25_true-unreach-call.c below 2 PASS0.505
id_i5_o5_false-unreach-call.c below 2 OKAY0.51
id_i5_o5_true-unreach-call.c below 2 PASS0.505
id_o1000_false-unreach-call.c below 2 OKAY0.516
id_o100_false-unreach-call.c below 2 OKAY0.502
id_o10_false-unreach-call.c below 2 OKAY0.51
id_o200_false-unreach-call.c below 2 OKAY0.513
id_o20_false-unreach-call.c below 2 OKAY0.514
id_o3_false-unreach-call.c below 2 OKAY0.521
sum_10x0_false-unreach-call.c below 2 OKAY0.591
sum_10x0_true-unreach-call.c below 2 PASS0.548
sum_15x0_false-unreach-call.c below 2 OKAY0.584
sum_15x0_true-unreach-call.c below 2 PASS0.57
sum_20x0_false-unreach-call.c below 2 OKAY0.578
sum_20x0_true-unreach-call.c below 2 PASS0.564
sum_25x0_false-unreach-call.c below 2 OKAY0.602
sum_25x0_true-unreach-call.c below 2 PASS0.552
sum_2x3_false-unreach-call.c below 2 OKAY0.562
sum_2x3_true-unreach-call.c below 2 PASS0.548
sum_non_eq_false-unreach-call.c below 2 OKAY0.571
sum_non_eq_true-unreach-call.c below 2 PASS0.56
sum_non_false-unreach-call.c below 2 OKAY0.579
sum_non_true-unreach-call.c below 2 PASS0.553
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.83
/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.561
rec-bhmr2007_true-unreach-call.c below 2 PASS0.544
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.079
rec-cggmp2005_true-unreach-call.c below 2 PASS0.512
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.555
rec-css2003_true-unreach-call.c below 2 PASS1.504
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.005
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.106
rec-gj2007b_true-unreach-call.c below 2 FAIL0.52
rec-gj2007_true-unreach-call.c below 2 FAIL0.692
rec-gr2006_true-unreach-call.c below 2 FAIL0.678
rec-gsv2008_true-unreach-call.c below 2 PASS0.569
rec-hhk2008_true-unreach-call.c below 2 PASS0.511
rec-jm2006_true-unreach-call.c below 2 PASS0.67
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.762
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.63
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.898
/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.466
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.544
rec-count_by_2_true-unreach-call.c below 2 PASS0.482
rec-count_by_k_true-unreach-call.c below 2 PASS0.511
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.512
rec-gauss_sum_true-unreach-call.c below 2 PASS0.568
rec-half_true-unreach-call.c below 2 FAIL0.527
rec-nested_true-unreach-call.c below 3 FAIL0.864
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.474
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.662
cubic_polynomial_unsafe.c below 2 OKAY0.64
edit_distance_bottom_up.c below 3 FAIL186.713
edit_distance_top_down.c below 3 FAIL5.304
log_log_n_solution.c below 3 FAIL0.595
log_log_n_solution_unsafe.c below 3 OKAY0.622
log_n_solution.c below 2 FAIL0.609
log_n_solution_unsafe.c below 2 OKAY0.615
multivariate_1.c below TIMEOUT 300.095
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL3.553
multivariate_higher_order_unsafe.c below 7 OKAY3.539
n_cubed_solution.c below EXCEPTION 103.688
n_cubed_solution_unsafe.c below EXCEPTION 0.025
n_log_n_solution.c below 8 FAIL1.655
n_log_n_solution_unsafe.c below 8 OKAY1.651
n_squared_two_base_case_even.c below 2 PASS0.688
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.705
n_squared_two_base_case_odd.c below 2 PASS0.684
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.709
pascals_dynamic.c below 3 FAIL2.746
pascals_dynamic_unsafe.c below 3 OKAY2.892
pascals_iterative.c below 1 FAIL5.18
pascals_iterative_unsafe.c below 1 OKAY5.127
pascals_recursive.c below 8 FAIL3.846
pascals_recursive_unsafe.c below 8 OKAY3.731
squared_solution.c below 8 FAIL3.269
squared_solution_unsafe.c below 8 OKAY3.233
two_n_even.c below 2 PASS0.53
two_n_even_unsafe.c below 2 OKAY0.567
two_n_odd.c below 2 PASS0.547
two_n_odd_unsafe.c below 2 OKAY0.541
two_to_n_over_two_even.c below 7 FAIL130.352
two_to_n_over_two_even_unsafe.c below 7 OKAY294.584
two_to_n_over_two_odd.c below 7 FAIL250.881
two_to_n_over_two_odd_unsafe.c below 7 OKAY119.062
two_to_n_squared.c below 5 FAIL20.433
two_to_n_squared_unsafe.c below 5 OKAY20.522
two_to_two_to_n.c below 7 FAIL1.464
two_to_two_to_n_unsafe.c below 7 OKAY1.434
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1783.698
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.412
adding_and_mult_unsafe.c below 1 OKAY0.42
binary_search_array_tree.c below 1 FAIL0.79
exp_add_linear.c below 1 PASS0.537
exp_add_linear_unsafe.c below 1 OKAY0.535
exp_add_loop_rec.c below 1 FAIL0.409
exp_add_loop_rec_unsafe.c below 1 OKAY0.43
exp_add_loop_variable.c below 1 PASS0.515
exp_add_loop_variable_unsafe.c below 1 OKAY0.507
exp_with_linear_inner_loop.c below 1 FAIL0.628
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.611
halving_log1.c below 1 FAIL0.688
linear_two_to_n.c below 7 FAIL1.84
linear_two_to_n_unsafe.c below 7 OKAY1.753
loop_five_to_n.c below 1 PASS0.475
loop_five_to_n_unsafe.c below 1 OKAY0.487
non_loop_five_to_n.c below 7 FAIL55.876
non_loop_five_to_n_unsafe.c below 7 OKAY55.313
power_log_modified.c below 1 PASS0.73
simple_exponential.c below 1 PASS0.47
simple_exponential_for.c below 1 PASS0.531
simple_exponential_for_unsafe.c below 1 OKAY0.522
simple_exponential_unsafe.c below 1 OKAY0.488
two_to_n_minus_n.c below 7 FAIL2.555
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.608
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 730.141
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.74
02.c below 3 FAIL1.037
03.c below 1 PASS0.575
04.c below 1 PASS0.397
05.c below 3 PASS1.303
06.c below 3 FAIL10.82
07.c below 3 PASS0.731
08.c below 3 PASS1.667
09.c below 3 PASS1.156
10.c below 3 FAIL1.382
11.c below 1 PASS0.424
12.c below 3 PASS1.69
13.c below 3 PASS0.715
14.c below 3 PASS0.606
15.c below 1 PASS0.417
16.c below 1 PASS0.571
17.c below 1 PASS3.73
18.c below 1 PASS0.488
19.c below 1 PASS0.572
20.c below 3 FAIL0.875
21.c below 3 PASS0.701
22.c below 3 FAIL0.954
23.c below 1 PASS0.434
24.c below 1 PASS0.503
25.c below 3 FAIL1.795
26.c below TIMEOUT 300.004
27.c below 1 PASS0.536
28.c below 3 PASS0.744
29.c below 3 PASS1.181
30.c below 1 PASS0.405
31.c below 3 PASS1.337
32.c below 1 FAIL0.447
33.c below 3 PASS1.457
34.c below 1 FAIL0.45
35.c below 1 PASS0.377
36.c below 3 PASS2.823
37.c below 3 FAIL0.659
38.c below 1 FAIL0.455
39.c below 3 PASS0.573
40.c below 3 PASS0.951
41.c below 1 PASS0.453
42.c below 3 PASS1.067
43.c below 3 PASS0.697
44.c below 1 PASS0.429
45.c below 3 FAIL3.015
46.c below 3 FAIL2.09
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 354.433
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.525
AGHKTW2017_foo.c below 1 PASS0.514
AGHKTW2017_loginSafe.c below 1 PASS1.06
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.601
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.575
BCK2011_gauss.c below 1 PASS0.534
BCK2011_strength_reduction.c below 1 PASS0.884
BCK2011_strength_reduction_linear.c below 1 PASS0.544
fibonacci_information_flow.c below 1 PASS0.671
loop_splitting_test_safe.c below 1 PASS0.721
TA2005_fib2.c below 1 PASS0.706
TA2005_fib.c below 1 PASS0.56
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.895
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.832
c3_cleanup_better.c below 3 PASS1.74
c3_cleanup.c below 3 PASS1.847
c3_intermediate.c below 3 PASS1.727
c3_noinv.c below 3 FAIL1.446
doublers.c below 1 FAIL0.653
doublers_easier.c below 3 FAIL1.305
doublers_easy.c below 1 FAIL0.733
exp_mult.c below 1 FAIL0.437
fig1_rotation_unsafe.c below 1 OKAY0.472
not_P_solvable.c below 1 PASS0.467
ICRA Assertions (True) = 5/10
ICRA Assertions (False) = 1/1
ICRA Time = 11.659
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.459
maxequals_linear_1.c below 1 PASS0.731
maxequals_linear_2.c below 1 PASS0.719
maxequals_linear_3.c below 1 FAIL0.426
maxequals_linear_4.c below 1 PASS0.429
maxequals_linear_5.c below 1 PASS0.435
maxequals_linear_6.c below 1 FAIL0.448
maxequals_matrix1.c below 3 FAIL1.664
maxequals_matrix2.c below 3 FAIL1.79
maxequals_quadratic1.c below 1 FAIL0.456
maxequals_quadratic2.c below 1 PASS0.435
maxequals_stratified1.c below 3 PASS5.17
maxequals_stratified2.c below 3 PASS5.249
maxequals_stratified3.c below 3 FAIL5.486
nine.c below 1 FAIL0.448
nine_nondecreasing.c below 1 PASS0.674
sum_interval_1.c below 1 FAIL0.517
sum_interval_2.c below 1 FAIL0.498
sum_interval_3.c below 1 FAIL0.507
TrackingObjectFields.c below 3 PASS11.237
TrackingObjectFields_inlined.c below 1 PASS3.273
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 41.051
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.526
bobble2_varloop.c below 1 PASS0.504
bobble3.c below TIMEOUT 300.005
bobble4.c below 1 FAIL0.474
bobble5.c below 1 FAIL0.497
bobble.c below 1 PASS0.517
inchworm2.c below 1 TIMEOUT300.004
inchworm3.c below 1 PASS0.474
inchworm4.c below 1 PASS0.517
inchworm5.c below 1 PASS0.47
inchworm6_unsafe.c below 1 OKAY0.479
inchworm.c below 1 FAIL0.467
leapdiff2.c below 1 TIMEOUT300.005
leapfrog_annotated.c below 1 FAIL0.507
leapfrog_annotated_disjunction.c below 1 PASS0.522
leapfrog_asymmetric2.c below 1 FAIL0.562
leapfrog_asymmetric3.c below 1 FAIL0.577
leapfrog_asymmetric.c below 1 FAIL0.508
leapfrog.c below 1 FAIL0.468
leapfrog_materialized.c below 1 FAIL0.502
leapfrog_verbose.c below 1 FAIL0.5
leapspin.c below 1 FAIL0.445
leapsum2.c below 1 TIMEOUT300.007
leapthree.c below 1 FAIL0.476
microbobble2.c below 1 PASS0.454
microbobble3.c below 1 PASS0.442
microbobble_asymmetric.c below 1 PASS0.456
microbobble.c below 1 FAIL0.435
simple_bl2.c below 1 FAIL0.489
simple_bl3.c below 1 FAIL0.404
simple_bl.c below 1 FAIL0.485
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1213.178
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.353
binval_example_2_unsafe.c below 1 OKAY0.347
binval_example_3_unsafe.c below 1 OKAY0.35
binval_example_4.c below 1 PASS0.437
binval_example_4_unsafe.c below 1 OKAY0.411
binval_example_5.c below 1 FAIL1.488
binval_example_5_unsafe.c below 1 OKAY3.533
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 6.919