[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.342
qsort.c below 4 PASS1.247
speed_pldi09_fig1.c below 1 PASS0.666
speed_pldi09_fig4_2.c below 1 FAIL0.459
speed_pldi09_fig4_4.c below 1 PASS0.591
speed_pldi09_fig4_5.c below 1 PASS0.502
speed_pldi10_ex1.c below 1 PASS1.701
speed_pldi10_ex3.c below 1 PASS0.68
speed_pldi10_ex4.c below 1 PASS0.736
speed_popl10_fig2_1.c below 1 PASS0.62
speed_popl10_fig2_2.c below 1 FAIL0.431
speed_popl10_nested_multiple.c below 1 PASS0.575
speed_popl10_nested_single.c below 1 PASS0.549
speed_popl10_sequential_single.c below 1 PASS0.511
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.418
t07.c below 1 PASS0.57
t08.c below 1 PASS0.523
t09.c below 1 PASS0.456
t10.c below 1 PASS0.415
t11.c below 1 PASS0.624
t13.c below 1 FAIL0.538
t15.c below 1 PASS0.543
t16.c below 1 PASS0.468
t19.c below 1 PASS0.492
t20.c below 1 PASS0.467
t27.c below 1 PASS0.768
t28.c below 1 PASS0.739
t30.c below 1 FAIL0.467
t37.c below 2 PASS0.893
t39.c below 2 PASS0.766
t46.c below 1 PASS0.514
t47.c below 1 PASS0.662
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.981
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.489
qsort_full.c below 4 PASS11.569
rec1-param_safe.c below 2 PASS0.526
rec1-param_unsafe.c below 2 OKAY0.497
rec1_safe.c below 2 PASS0.484
rec1_unsafe.c below 2 OKAY0.476
rec2-param_safe.c below 2 PASS0.473
rec2-param_unsafe.c below 2 OKAY0.479
rec2_safe.c below 2 PASS0.475
rec2_unsafe.c below 2 OKAY0.47
rec-test.c below 2 PASS0.464
sas03_bothbranches.c below 7 PASS1.243
sas03.c below 2 PASS0.898
simulated_lese_recursive.c below 2 PASS0.62
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 19.163
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.382
count_up_down_unsafe.c below 1 OKAY0.391
divide.c below 1 PASS0.387
factor_unsafe.c below 1 OKAY0.367
for_infinite_loop_1_safe.c below 1 PASS0.373
for_infinite_loop_2_safe.c below 1 PASS0.352
interproc.c below 1 PASS0.315
mult.c below 1 PASS0.377
pointer_arith.c below 1 PASS0.323
quotient.c below 3 PASS0.716
subtract.c below 1 PASS0.38
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.37
sum01_bug02_unsafe.c below 1 OKAY0.728
sum01_real_safe.c below 1 PASS0.374
sum01_safe.c below 1 PASS0.397
sum01_unsafe.c below 1 OKAY0.584
sum02_safe.c below 1 PASS0.429
sum03_safe.c below 1 PASS0.467
sum03_unsafe.c below 1 OKAY0.589
sum04_safe.c below 1 PASS0.407
sum04_unsafe.c below 1 OKAY0.594
terminator_02_safe.c below 1 PASS0.353
terminator_02_unsafe.c below 1 OKAY0.408
terminator_03_safe.c below 1 PASS0.359
terminator_03_unsafe.c below 1 OKAY0.37
token_ring01_safe.c below 4 FAIL124.954
token_ring01_unsafe.c below 4 OKAY203.146
toy_safe.c below EXCEPTION 129.519
trex01_safe.c below 1 PASS0.827
trex01_unsafe.c below 1 OKAY0.442
trex02_safe2.c below 3 PASS0.554
trex02_safe.c below 3 PASS0.531
trex02_unsafe.c below 3 OKAY0.538
trex03_safe.c below 1 PASS0.511
trex03_unsafe.c below 1 OKAY0.492
trex04_safe.c below 1 PASS0.382
while_infinite_loop_1_safe.c below 1 PASS0.343
while_infinite_loop_2_safe.c below 1 PASS0.341
while_infinite_loop_3_safe.c below 1 PASS0.346
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 473.718
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.55
blogger_simplified1.c below 3 PASS1.596
divided_difference2.c below TIMEOUT 300.011
mult-proc.c below 3 PASS0.544
mult-proc-params.c below 3 PASS0.531
popall.c below 1 PASS0.929
simulated_scc.c below 1 PASS0.848
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.009
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.407
degree2_binomial.c below 1 PASS0.917
degree2_monomial.c below 1 PASS0.503
degree3_binomial.c below 1 FAIL5.006
degree3_monomial.c below 1 PASS0.974
degree4_binomial.c below 1 FAIL5.113
degree4_monomial.c below 1 PASS1.656
degree5_binomial.c below 1 FAIL16.036
degree5_monomial.c below 1 PASS3.079
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 33.691
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.527
cubic_with_square_interproc.c below 2 FAIL0.717
cubic_with_square_nonlinear.c below 1 FAIL0.647
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.725
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.636
cubic_with_square_unsafe.c below 1 OKAY0.503
multi-input.c below 1 FAIL10.577
multi-input_unsafe.c below 1 OKAY10.691
nondet_loop_bound.c below 1 FAIL0.556
nondet_loop_bound_quartic.c below 1 FAIL0.731
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.786
nondet_loop_bound_unsafe.c below 1 OKAY0.582
nonlinear_stratified.c below 1 PASS125.554
nonlinear_stratified_unsafe.c below 1 OKAY69.741
quartic_with_cube.c below 1 FAIL0.714
quartic_with_cube_nonlinear.c below 1 FAIL0.969
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.981
quartic_with_cube_unsafe.c below 1 OKAY0.573
quintic_with_quartic.c below 1 PASS1.178
quintic_with_quartic_nonlinear.c below 1 PASS1.16
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.156
quintic_with_quartic_unsafe.c below 1 OKAY1.138
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 230.842
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.009
degree2_FD_AllAux_AllAssm.c below 1 PASS108.442
degree2_FD_AllAux_FewAssm.c below 1 PASS6.908
degree2_FD_FewAux_FewAssm.c below 1 PASS1.329
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.33
degree3.c below 1 PASS1.105
degree3_FD.c below 1 PASS1.287
degree4.c below 1 PASS1.894
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 123.304
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.538
loop_unsafe.c below 1 OKAY0.53
simulated_lese_parser.c below 1 PASS0.403
simulated_lese_sentinel.c below 1 PASS0.396
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.867
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.417
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.417
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.008
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.008
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.396
array_false-unreach-call2.c below 1 OKAY0.411
array_false-unreach-call3.c below 1 OKAY0.403
array_true-unreach-call1.c below 1 FAIL0.384
array_true-unreach-call2.c below 1 FAIL0.416
array_true-unreach-call3.c below 1 PASS0.389
array_true-unreach-call4.c below 1 FAIL0.384
const_false-unreach-call1.c below 1 OKAY0.403
const_true-unreach-call1.c below 1 PASS0.4
diamond_false-unreach-call1.c below 1 OKAY0.393
diamond_true-unreach-call1.c below 1 PASS0.386
diamond_true-unreach-call2.c below 1 PASS0.405
functions_false-unreach-call1.c below 3 OKAY0.53
functions_true-unreach-call1.c below 3 PASS0.532
multivar_false-unreach-call1.c below 1 OKAY0.394
multivar_true-unreach-call1.c below 1 PASS0.4
nested_false-unreach-call1.c below 1 OKAY0.465
nested_true-unreach-call1.c below 1 PASS0.463
overflow_true-unreach-call1.c below 1 PASS0.364
phases_false-unreach-call1.c below 1 OKAY0.498
phases_false-unreach-call2.c below 1 OKAY0.391
phases_true-unreach-call1.c below 1 PASS0.515
phases_true-unreach-call2.c below 1 PASS0.372
simple_false-unreach-call1.c below 1 OKAY0.362
simple_false-unreach-call2.c below 1 OKAY0.356
simple_false-unreach-call3.c below 1 OKAY0.359
simple_false-unreach-call4.c below 1 OKAY0.357
simple_true-unreach-call1.c below 1 PASS0.358
simple_true-unreach-call2.c below 1 PASS0.36
simple_true-unreach-call3.c below 1 PASS0.356
simple_true-unreach-call4.c below 1 PASS0.361
underapprox_false-unreach-call1.c below 1 OKAY0.409
underapprox_false-unreach-call2.c below 1 OKAY0.393
underapprox_true-unreach-call1.c below 1 FAIL0.412
underapprox_true-unreach-call2.c below 1 PASS0.393
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.17
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.535
apache-get-tag_true-unreach-call.c below 1 FAIL0.596
down_true-unreach-call.c below 1 PASS0.456
fragtest_simple_true-unreach-call.c below 1 PASS0.577
half_2_true-unreach-call.c below 1 PASS0.507
heapsort_true-unreach-call.c below 1 PASS2.227
id_build_true-unreach-call.c below 1 PASS0.441
id_trans_false-unreach-call.c below 1 OKAY0.378
id_trans_true-unreach-call.c below 1 PASS0.382
large_const_true-unreach-call.c below 1 PASS0.538
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.464
nested6_true-unreach-call.c below 1 FAIL0.639
nested9_true-unreach-call.c below 1 PASS0.727
nest-if3_true-unreach-call.c below 1 PASS0.567
NetBSD_loop_true-unreach-call.c below 1 PASS0.408
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.494
seq_true-unreach-call.c below 1 PASS0.558
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.601
string_concat-noarr_true-unreach-call.c below 1 PASS0.52
up_true-unreach-call.c below 1 PASS0.479
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.094
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.425
bhmr2007_true-unreach-call.c below 1 PASS0.437
cggmp2005b_true-unreach-call.c below 1 PASS0.647
cggmp2005_true-unreach-call.c below 1 PASS0.406
cggmp2005_variant_true-unreach-call.c below 1 PASS0.407
css2003_true-unreach-call.c below 1 PASS1.093
ddlm2013_true-unreach-call.c below 1 PASS0.649
gcnr2008_false-unreach-call.c below 1 OKAY1.109
gj2007b_true-unreach-call.c below 1 FAIL0.448
gj2007_true-unreach-call.c below 1 PASS0.592
gr2006_true-unreach-call.c below 1 PASS0.542
gsv2008_true-unreach-call.c below 1 PASS0.417
hhk2008_true-unreach-call.c below 1 PASS0.386
jm2006_true-unreach-call.c below 1 PASS0.528
jm2006_variant_true-unreach-call.c below 1 PASS0.617
mcmillan2006_true-unreach-call.c below 1 FAIL0.459
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.162
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.37
count_by_1_variant_true-unreach-call.c below 1 PASS0.481
count_by_2_true-unreach-call.c below 1 PASS0.359
count_by_k_true-unreach-call.c below 1 PASS0.377
count_by_nondet_true-unreach-call.c below 1 PASS0.394
gauss_sum_true-unreach-call.c below 1 PASS0.428
half_true-unreach-call.c below 1 FAIL0.411
nested_true-unreach-call.c below 1 PASS0.518
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.338
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.442
array_true-unreach-call.c below 1 FAIL0.451
bubble_sort_false-unreach-call.c below 4 OKAY76.396
bubble_sort_true-unreach-call.c below 1 PASS5.226
compact_false-unreach-call.c below 1 OKAY0.466
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.39
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.397
eureka_01_false-unreach-call.c below 1 OKAY2.617
eureka_01_true-unreach-call.c below 1 FAIL1.611
eureka_05_true-unreach-call.c below 1 FAIL0.871
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.366
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.396
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.345
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.359
heavy_false-unreach-call.c below 1 OKAY0.597
heavy_true-unreach-call.c below 1 PASS0.581
insertion_sort_false-unreach-call.c below 1 OKAY1.504
insertion_sort_true-unreach-call.c below 1 FAIL0.637
invert_string_false-unreach-call.c below 1 OKAY0.591
invert_string_true-unreach-call.c below 1 FAIL0.646
linear_sea.ch_true-unreach-call.c below 1 FAIL0.417
linear_search_false-unreach-call.c below 1 OKAY0.456
lu.cmp_true-unreach-call.c below 3 PASS27.938
ludcmp_false-unreach-call.c below 3 OKAY27.929
matrix_false-unreach-call_true-termination.c below 1 OKAY1.373
matrix_true-unreach-call_true-termination.c below 1 FAIL0.499
n.c11_true-unreach-call.c below 3 FAIL0.58
n.c24_false-unreach-call.c below 3 OKAY5.236
n.c40_true-unreach-call.c below 1 FAIL0.401
nec11_false-unreach-call.c below 1 OKAY0.401
nec20_false-unreach-call.c below 1 OKAY0.449
nec40_true-unreach-call.c below 1 FAIL0.409
string_false-unreach-call.c below 1 OKAY0.793
string_true-unreach-call.c below 1 FAIL0.754
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.719
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.376
sum01_false-unreach-call_true-termination.c below 1 OKAY0.567
sum01_true-unreach-call_true-termination.c below 1 PASS0.391
sum03_false-unreach-call_true-termination.c below 1 OKAY0.623
sum03_true-unreach-call_false-termination.c below 1 PASS0.495
sum04_false-unreach-call_true-termination.c below 1 OKAY0.605
sum04_true-unreach-call_true-termination.c below 1 PASS0.407
sum_array_false-unreach-call.c below 1 OKAY0.648
sum_array_true-unreach-call.c below 1 FAIL0.734
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.347
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.616
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.516
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.38
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.415
trex01_false-unreach-call_true-termination.c below 3 OKAY0.637
trex01_true-unreach-call.c below 3 PASS0.903
trex02_false-unreach-call_true-termination.c below 3 OKAY0.549
trex02_true-unreach-call_true-termination.c below 3 PASS0.539
trex03_false-unreach-call_true-termination.c below 3 OKAY0.861
trex03_true-unreach-call.c below 3 PASS0.876
trex04_true-unreach-call_false-termination.c below 1 PASS0.444
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.414
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS9.474
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.41
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.057
vogal_false-unreach-call.c below 1 OKAY0.917
vogal_true-unreach-call.c below 1 FAIL0.96
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.357
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.343
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.343
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.204
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.544
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.566
Ackermann03_true-unreach-call.c below 7 FAIL1.546
Ackermann04_true-unreach-call.c below 7 FAIL1.546
Addition01_true-unreach-call_true-termination.c below 2 PASS0.794
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.834
Addition03_false-no-overflow.c below 2 PASS0.825
Addition03_true-unreach-call.c below 2 PASS0.801
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.649
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.586
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.567
Fibonacci01_true-unreach-call.c below TIMEOUT 300.006
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.007
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.004
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.004
gcd01_true-unreach-call_true-termination.c below 2 PASS0.736
gcd02_true-unreach-call.c below 2 FAIL1.375
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.263
McCarthy91_true-unreach-call.c below 7 FAIL1.269
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.763
Primes_true-unreach-call.c below 3 FAIL2.285
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.538
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.514
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.535
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1523.561
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.58
afterrec_2calls_true-unreach-call.c below 2 PASS0.562
afterrec_false-unreach-call.c below 2 OKAY0.483
afterrec_true-unreach-call.c below 2 PASS0.467
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.006
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.004
fibo_25_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.006
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.004
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.005
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.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.004
fibo_7_true-unreach-call.c below TIMEOUT 300.007
id2_b2_o3_true-unreach-call.c below 2 PASS0.979
id2_b3_o2_false-unreach-call.c below 2 OKAY0.956
id2_b3_o5_true-unreach-call.c below 2 PASS0.968
id2_b5_o10_true-unreach-call.c below 2 PASS0.929
id2_i5_o5_false-unreach-call.c below 2 OKAY0.544
id2_i5_o5_true-unreach-call.c below 2 PASS0.557
id_b2_o3_true-unreach-call.c below 2 PASS0.826
id_b3_o2_false-unreach-call.c below 2 OKAY0.834
id_b3_o5_true-unreach-call.c below 2 PASS0.806
id_b5_o10_true-unreach-call.c below 2 PASS0.782
id_i10_o10_false-unreach-call.c below 2 OKAY0.496
id_i10_o10_true-unreach-call.c below 2 PASS0.499
id_i15_o15_false-unreach-call.c below 2 OKAY0.482
id_i15_o15_true-unreach-call.c below 2 PASS0.475
id_i20_o20_false-unreach-call.c below 2 OKAY0.505
id_i20_o20_true-unreach-call.c below 2 PASS0.486
id_i25_o25_false-unreach-call.c below 2 OKAY0.494
id_i25_o25_true-unreach-call.c below 2 PASS0.497
id_i5_o5_false-unreach-call.c below 2 OKAY0.503
id_i5_o5_true-unreach-call.c below 2 PASS0.486
id_o1000_false-unreach-call.c below 2 OKAY0.506
id_o100_false-unreach-call.c below 2 OKAY0.503
id_o10_false-unreach-call.c below 2 OKAY0.51
id_o200_false-unreach-call.c below 2 OKAY0.5
id_o20_false-unreach-call.c below 2 OKAY0.506
id_o3_false-unreach-call.c below 2 OKAY0.505
sum_10x0_false-unreach-call.c below 2 OKAY0.554
sum_10x0_true-unreach-call.c below 2 PASS0.542
sum_15x0_false-unreach-call.c below 2 OKAY0.577
sum_15x0_true-unreach-call.c below 2 PASS0.58
sum_20x0_false-unreach-call.c below 2 OKAY0.573
sum_20x0_true-unreach-call.c below 2 PASS0.553
sum_25x0_false-unreach-call.c below 2 OKAY0.559
sum_25x0_true-unreach-call.c below 2 PASS0.551
sum_2x3_false-unreach-call.c below 2 OKAY0.547
sum_2x3_true-unreach-call.c below 2 PASS0.556
sum_non_eq_false-unreach-call.c below 2 OKAY0.572
sum_non_eq_true-unreach-call.c below 2 PASS0.564
sum_non_false-unreach-call.c below 2 OKAY0.548
sum_non_true-unreach-call.c below 2 PASS0.567
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9026.233
/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.561
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.108
rec-cggmp2005_true-unreach-call.c below 2 PASS0.511
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.554
rec-css2003_true-unreach-call.c below 2 PASS1.494
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.077
rec-gj2007b_true-unreach-call.c below 2 FAIL0.51
rec-gj2007_true-unreach-call.c below 2 FAIL0.68
rec-gr2006_true-unreach-call.c below 2 FAIL0.662
rec-gsv2008_true-unreach-call.c below 2 PASS0.543
rec-hhk2008_true-unreach-call.c below 2 PASS0.511
rec-jm2006_true-unreach-call.c below 2 PASS0.638
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.729
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.63
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 310.773
/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.464
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.557
rec-count_by_2_true-unreach-call.c below 2 PASS0.454
rec-count_by_k_true-unreach-call.c below 2 PASS0.475
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.527
rec-gauss_sum_true-unreach-call.c below 2 PASS0.565
rec-half_true-unreach-call.c below 2 FAIL0.536
rec-nested_true-unreach-call.c below 3 FAIL0.866
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.444
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.626
cubic_polynomial_unsafe.c below 2 OKAY0.602
edit_distance_bottom_up.c below 3 FAIL181.872
edit_distance_top_down.c below 3 FAIL5.265
log_log_n_solution.c below 3 FAIL0.599
log_log_n_solution_unsafe.c below 3 OKAY0.602
log_n_solution.c below 2 FAIL0.617
log_n_solution_unsafe.c below 2 OKAY0.595
multivariate_1.c below TIMEOUT 300.093
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL3.547
multivariate_higher_order_unsafe.c below 7 OKAY3.46
n_cubed_solution.c below EXCEPTION 101.392
n_cubed_solution_unsafe.c below EXCEPTION 0.026
n_log_n_solution.c below 8 FAIL1.6
n_log_n_solution_unsafe.c below 8 OKAY1.635
n_squared_two_base_case_even.c below 2 PASS0.685
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.72
n_squared_two_base_case_odd.c below 2 PASS0.686
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.696
pascals_dynamic.c below 3 FAIL2.646
pascals_dynamic_unsafe.c below 3 OKAY2.681
pascals_iterative.c below 1 FAIL4.868
pascals_iterative_unsafe.c below 1 OKAY4.931
pascals_recursive.c below 8 FAIL3.665
pascals_recursive_unsafe.c below 8 OKAY3.704
squared_solution.c below 8 FAIL3.172
squared_solution_unsafe.c below 8 OKAY3.109
two_n_even.c below 2 PASS0.555
two_n_even_unsafe.c below 2 OKAY0.552
two_n_odd.c below 2 PASS0.55
two_n_odd_unsafe.c below 2 OKAY0.531
two_to_n_over_two_even.c below 7 FAIL127.515
two_to_n_over_two_even_unsafe.c below 7 OKAY286.071
two_to_n_over_two_odd.c below 7 FAIL244.793
two_to_n_over_two_odd_unsafe.c below 7 OKAY150.219
two_to_n_squared.c below 5 FAIL20.493
two_to_n_squared_unsafe.c below 5 OKAY20.7
two_to_two_to_n.c below 7 FAIL1.622
two_to_two_to_n_unsafe.c below 7 OKAY1.596
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1789.297
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.439
adding_and_mult_unsafe.c below 1 OKAY0.442
binary_search_array_tree.c below 1 FAIL0.783
exp_add_linear.c below 1 PASS0.535
exp_add_linear_unsafe.c below 1 OKAY0.532
exp_add_loop_rec.c below 1 FAIL0.42
exp_add_loop_rec_unsafe.c below 1 OKAY0.411
exp_add_loop_variable.c below 1 PASS0.52
exp_add_loop_variable_unsafe.c below 1 OKAY0.525
exp_with_linear_inner_loop.c below 1 FAIL0.647
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.628
halving_log1.c below 1 FAIL0.656
linear_two_to_n.c below 7 FAIL1.76
linear_two_to_n_unsafe.c below 7 OKAY1.724
loop_five_to_n.c below 1 PASS0.484
loop_five_to_n_unsafe.c below 1 OKAY0.497
non_loop_five_to_n.c below 7 FAIL56.53
non_loop_five_to_n_unsafe.c below 7 OKAY55.76
power_log_modified.c below 1 PASS0.727
simple_exponential.c below 1 PASS0.47
simple_exponential_for.c below 1 PASS0.484
simple_exponential_for_unsafe.c below 1 OKAY0.491
simple_exponential_unsafe.c below 1 OKAY0.475
two_to_n_minus_n.c below 7 FAIL2.471
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.498
ICRA Assertions (True) = 7/15
ICRA Assertions (False) = 11/12
ICRA Time = 730.921
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.712
02.c below 3 FAIL0.902
03.c below 1 PASS0.576
04.c below 1 PASS0.418
05.c below 3 PASS1.312
06.c below 3 FAIL10.818
07.c below 3 PASS0.712
08.c below 3 PASS1.597
09.c below 3 PASS1.088
10.c below 3 FAIL1.265
11.c below 1 PASS0.395
12.c below 3 PASS1.637
13.c below 3 PASS0.707
14.c below 3 PASS0.613
15.c below 1 PASS0.385
16.c below 1 PASS0.548
17.c below 1 PASS3.742
18.c below 1 PASS0.48
19.c below 1 PASS0.573
20.c below 3 FAIL0.82
21.c below 3 PASS0.692
22.c below 3 FAIL0.959
23.c below 1 PASS0.423
24.c below 1 PASS0.494
25.c below 3 FAIL1.716
26.c below TIMEOUT 300.004
27.c below 1 PASS0.55
28.c below 3 PASS0.685
29.c below 3 PASS1.188
30.c below 1 PASS0.406
31.c below 3 PASS1.302
32.c below 1 FAIL0.441
33.c below 3 PASS1.428
34.c below 1 FAIL0.444
35.c below 1 PASS0.365
36.c below 3 PASS2.849
37.c below 3 FAIL0.663
38.c below 1 FAIL0.44
39.c below 3 PASS0.564
40.c below 3 PASS0.97
41.c below 1 PASS0.445
42.c below 3 PASS1.006
43.c below 3 PASS0.687
44.c below 1 PASS0.403
45.c below 3 FAIL2.944
46.c below 3 FAIL2.012
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 353.38
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.504
AGHKTW2017_foo.c below 1 PASS0.497
AGHKTW2017_loginSafe.c below 1 PASS0.988
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.569
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.578
BCK2011_gauss.c below 1 PASS0.546
BCK2011_strength_reduction.c below 1 PASS0.869
BCK2011_strength_reduction_linear.c below 1 PASS0.539
fibonacci_information_flow.c below 1 PASS0.71
loop_splitting_test_safe.c below 1 PASS0.727
TA2005_fib2.c below 1 PASS0.729
TA2005_fib.c below 1 PASS0.578
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 7.834
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below 1 PASS0.914
c3_cleanup_better.c below 3 PASS1.724
c3_cleanup.c below 3 PASS1.753
c3_intermediate.c below 3 PASS1.66
c3_noinv.c below 3 FAIL1.51
doublers.c below 1 FAIL0.665
doublers_easier.c below 3 FAIL1.324
doublers_easy.c below 1 FAIL0.766
exp_mult.c below 1 FAIL0.435
fig1_rotation_unsafe.c below 1 OKAY0.475
not_P_solvable.c below 1 PASS0.41
ICRA Assertions (True) = 5/10
ICRA Assertions (False) = 1/1
ICRA Time = 11.636
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below 1 FAIL0.453
maxequals_linear_1.c below 1 PASS0.669
maxequals_linear_2.c below 1 PASS0.635
maxequals_linear_3.c below 1 FAIL0.464
maxequals_linear_4.c below 1 PASS0.412
maxequals_linear_5.c below 1 PASS0.42
maxequals_linear_6.c below 1 FAIL0.433
maxequals_matrix1.c below 3 FAIL1.641
maxequals_matrix2.c below 3 FAIL1.689
maxequals_quadratic1.c below 1 FAIL0.447
maxequals_quadratic2.c below 1 PASS0.436
maxequals_stratified1.c below 3 PASS5.019
maxequals_stratified2.c below 3 PASS5.554
maxequals_stratified3.c below 3 FAIL5.548
nine.c below 1 FAIL0.429
nine_nondecreasing.c below 1 PASS0.668
sum_interval_1.c below 1 FAIL0.511
sum_interval_2.c below 1 FAIL0.501
sum_interval_3.c below 1 FAIL0.514
TrackingObjectFields.c below 3 PASS11.144
TrackingObjectFields_inlined.c below 1 PASS3.247
ICRA Assertions (True) = 10/21
ICRA Assertions (False) = 0/0
ICRA Time = 40.834
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below 1 PASS0.5
bobble2_varloop.c below 1 PASS0.496
bobble3.c below TIMEOUT 300.004
bobble4.c below 1 FAIL0.46
bobble5.c below 1 FAIL0.474
bobble.c below 1 PASS0.471
inchworm2.c below 1 TIMEOUT300.004
inchworm3.c below 1 PASS0.497
inchworm4.c below 1 PASS0.504
inchworm5.c below 1 PASS0.464
inchworm6_unsafe.c below 1 OKAY0.454
inchworm.c below 1 FAIL0.469
leapdiff2.c below 1 TIMEOUT300.006
leapfrog_annotated.c below 1 FAIL0.442
leapfrog_annotated_disjunction.c below 1 PASS0.493
leapfrog_asymmetric2.c below 1 FAIL0.539
leapfrog_asymmetric3.c below 1 FAIL0.566
leapfrog_asymmetric.c below 1 FAIL0.489
leapfrog.c below 1 FAIL0.437
leapfrog_materialized.c below 1 FAIL0.478
leapfrog_verbose.c below 1 FAIL0.484
leapspin.c below 1 FAIL0.417
leapsum2.c below 1 TIMEOUT300.007
leapthree.c below 1 FAIL0.477
microbobble2.c below 1 PASS0.448
microbobble3.c below 1 PASS0.436
microbobble_asymmetric.c below 1 PASS0.449
microbobble.c below 1 FAIL0.423
simple_bl2.c below 1 FAIL0.499
simple_bl3.c below 1 FAIL0.404
simple_bl.c below 1 FAIL0.46
ICRA Assertions (True) = 10/30
ICRA Assertions (False) = 1/1
ICRA Time = 1212.751
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below 1 PASS0.359
binval_example_2_unsafe.c below 1 OKAY0.366
binval_example_3_unsafe.c below 1 OKAY0.351
binval_example_4.c below 1 PASS0.424
binval_example_4_unsafe.c below 1 OKAY0.401
binval_example_5.c below 1 FAIL1.47
binval_example_5_unsafe.c below 1 OKAY3.477
ICRA Assertions (True) = 2/3
ICRA Assertions (False) = 4/4
ICRA Time = 6.848