[Version Information]
WALi-OpenNWA version: a7ea0126fa78965d0a011019e89118b81e8e7f9e (2017-09-25 12:47:37 -0500) "Adding command-line argument for -cra-abstraction-timeout"
duet version: ec9d07551bd7fec2dd4591166e41fea7e8c3b7df (2017-10-05 19:28:08 -0400) "Allocate standard z3 solver"
# Installed packages for 4.02.3+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.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
cppo                  1.6.0  Equivalent of the C preprocessor for OCaml programs
cppo_ocamlbuild       1.6.0  ocamlbuild support for cppo, OCaml-friendly source 
deriving           20140904  Extension to OCaml for deriving functions from type
jbuilder         1.0+beta12  Fast, portable and opinionated build system
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               20170817  Recurrence solver based on operational calculus
optcomp                 1.6  Optional compilation with cpp-like directives
ounit                 2.0.0  Unit testing framework loosely based on HUnit. It i
ppx_deriving            4.1  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
result                  1.2  Compatibility Result module
Z3                 20161217  Z3 SMT solver

Test Name Output No. of Rounds Result Run Time
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below 1 FAIL0.437
kmp.c below 1 PASS1.457
qsort.c below 4 PASS1.351
speed_pldi09_fig1.c below 1 PASS0.705
speed_pldi09_fig4_2.c below 1 FAIL0.455
speed_pldi09_fig4_4.c below 1 PASS0.633
speed_pldi09_fig4_5.c below 1 PASS0.496
speed_pldi10_ex1.c below 1 PASS1.816
speed_pldi10_ex3.c below 1 PASS0.733
speed_pldi10_ex4.c below 1 PASS0.754
speed_popl10_fig2_1.c below 1 PASS0.644
speed_popl10_fig2_2.c below 1 FAIL0.432
speed_popl10_nested_multiple.c below 1 PASS0.58
speed_popl10_nested_single.c below 1 PASS0.545
speed_popl10_sequential_single.c below 1 PASS0.511
speed_popl10_simple_multiple.c below 1 PASS0.733
speed_popl10_simple_single_2.c below 1 PASS0.952
speed_popl10_simple_single.c below 1 PASS0.412
t07.c below 1 PASS0.546
t08.c below 1 PASS0.494
t09.c below 1 PASS0.462
t10.c below 1 PASS0.435
t11.c below 1 PASS0.648
t13.c below 1 FAIL0.542
t15.c below 1 PASS0.54
t16.c below 1 PASS0.484
t19.c below 1 PASS0.497
t20.c below 1 PASS0.463
t27.c below 1 PASS0.784
t28.c below 1 PASS0.739
t30.c below 1 FAIL0.488
t37.c below 2 PASS0.953
t39.c below 2 PASS0.806
t46.c below 1 PASS0.536
t47.c below 1 PASS0.705
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 23.768
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.5
qsort_full.c below 4 PASS12.531
rec1-param_safe.c below 2 PASS0.529
rec1-param_unsafe.c below 2 OKAY0.54
rec1_safe.c below 2 PASS0.479
rec1_unsafe.c below 2 OKAY0.477
rec2-param_safe.c below 2 PASS0.504
rec2-param_unsafe.c below 2 OKAY0.465
rec2_safe.c below 2 PASS0.483
rec2_unsafe.c below 2 OKAY0.481
rec-test.c below 2 PASS0.466
sas03_bothbranches.c below 7 PASS1.259
sas03.c below 2 PASS0.949
simulated_lese_recursive.c below 2 PASS0.658
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 20.321
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.4
count_up_down_unsafe.c below 1 OKAY0.402
divide.c below 1 PASS0.398
factor_unsafe.c below 1 OKAY0.369
for_infinite_loop_1_safe.c below 1 PASS0.375
for_infinite_loop_2_safe.c below 1 PASS0.356
interproc.c below 1 PASS0.319
mult.c below 1 PASS0.385
pointer_arith.c below 1 PASS0.328
quotient.c below 3 PASS0.729
subtract.c below 1 PASS0.372
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.372
sum01_bug02_unsafe.c below 1 OKAY0.738
sum01_real_safe.c below 1 PASS0.389
sum01_safe.c below 1 PASS0.404
sum01_unsafe.c below 1 OKAY0.586
sum02_safe.c below 1 PASS0.426
sum03_safe.c below 1 PASS0.482
sum03_unsafe.c below 1 OKAY0.603
sum04_safe.c below 1 PASS0.42
sum04_unsafe.c below 1 OKAY0.604
terminator_02_safe.c below 1 PASS0.363
terminator_02_unsafe.c below 1 OKAY0.418
terminator_03_safe.c below 1 PASS0.372
terminator_03_unsafe.c below 1 OKAY0.378
token_ring01_safe.c below 4 FAIL139.864
token_ring01_unsafe.c below 4 OKAY221.512
toy_safe.c below EXCEPTION 142.353
trex01_safe.c below 1 PASS0.814
trex01_unsafe.c below 1 OKAY0.449
trex02_safe2.c below 3 PASS0.546
trex02_safe.c below 3 PASS0.537
trex02_unsafe.c below 3 OKAY0.553
trex03_safe.c below 1 PASS0.518
trex03_unsafe.c below 1 OKAY0.506
trex04_safe.c below 1 PASS0.397
while_infinite_loop_1_safe.c below 1 PASS0.345
while_infinite_loop_2_safe.c below 1 PASS0.335
while_infinite_loop_3_safe.c below 1 PASS0.341
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 520.058
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.563
blogger_simplified1.c below 3 PASS1.747
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.532
mult-proc-params.c below 3 PASS0.541
popall.c below 1 PASS0.988
simulated_scc.c below 1 PASS0.878
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 305.253
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.422
degree2_binomial.c below 1 PASS0.935
degree2_monomial.c below 1 PASS0.509
degree3_binomial.c below 1 FAIL5.28
degree3_monomial.c below 1 PASS1.039
degree4_binomial.c below 1 FAIL5.591
degree4_monomial.c below 1 PASS1.812
degree5_binomial.c below 1 FAIL25.455
degree5_monomial.c below 1 PASS3.345
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 44.388
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.526
cubic_with_square_interproc.c below 2 FAIL0.747
cubic_with_square_nonlinear.c below 1 FAIL0.674
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.749
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.684
cubic_with_square_unsafe.c below 1 OKAY0.524
multi-input.c below 1 FAIL11.465
multi-input_unsafe.c below 1 OKAY11.128
nondet_loop_bound.c below 1 FAIL0.577
nondet_loop_bound_quartic.c below 1 FAIL0.808
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.8
nondet_loop_bound_unsafe.c below 1 OKAY0.573
nonlinear_stratified.c below 1 PASS132.503
nonlinear_stratified_unsafe.c below 1 OKAY74.568
quartic_with_cube.c below 1 FAIL0.737
quartic_with_cube_nonlinear.c below 1 FAIL1.061
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY1.053
quartic_with_cube_unsafe.c below 1 OKAY0.571
quintic_with_quartic.c below 1 PASS1.196
quintic_with_quartic_nonlinear.c below 1 PASS1.235
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY1.188
quintic_with_quartic_unsafe.c below 1 OKAY1.172
ICRA Assertions (True) = 3/12
ICRA Assertions (False) = 10/10
ICRA Time = 244.539
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS1.058
degree2_FD_AllAux_AllAssm.c below 1 PASS117.1
degree2_FD_AllAux_FewAssm.c below 1 PASS7.77
degree2_FD_FewAux_FewAssm.c below 1 PASS1.483
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.465
degree3.c below 1 PASS1.193
degree3_FD.c below 1 PASS1.318
degree4.c below 1 PASS2.036
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 133.423
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.536
loop_unsafe.c below 1 OKAY0.55
simulated_lese_parser.c below 1 PASS0.425
simulated_lese_sentinel.c below 1 PASS0.402
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.913
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.407
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.407
/bat0/stac/Code/Ark2-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/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.395
array_false-unreach-call2.c below 1 OKAY0.409
array_false-unreach-call3.c below 1 OKAY0.415
array_true-unreach-call1.c below 1 FAIL0.397
array_true-unreach-call2.c below 1 FAIL0.417
array_true-unreach-call3.c below 1 PASS0.403
array_true-unreach-call4.c below 1 FAIL0.379
const_false-unreach-call1.c below 1 OKAY0.406
const_true-unreach-call1.c below 1 PASS0.401
diamond_false-unreach-call1.c below 1 OKAY0.394
diamond_true-unreach-call1.c below 1 PASS0.391
diamond_true-unreach-call2.c below 1 PASS0.408
functions_false-unreach-call1.c below 3 OKAY0.522
functions_true-unreach-call1.c below 3 PASS0.518
multivar_false-unreach-call1.c below 1 OKAY0.422
multivar_true-unreach-call1.c below 1 PASS0.401
nested_false-unreach-call1.c below 1 OKAY0.466
nested_true-unreach-call1.c below 1 PASS0.471
overflow_true-unreach-call1.c below 1 PASS0.366
phases_false-unreach-call1.c below 1 OKAY0.5
phases_false-unreach-call2.c below 1 OKAY0.395
phases_true-unreach-call1.c below 1 PASS0.493
phases_true-unreach-call2.c below 1 PASS0.386
simple_false-unreach-call1.c below 1 OKAY0.363
simple_false-unreach-call2.c below 1 OKAY0.367
simple_false-unreach-call3.c below 1 OKAY0.361
simple_false-unreach-call4.c below 1 OKAY0.366
simple_true-unreach-call1.c below 1 PASS0.369
simple_true-unreach-call2.c below 1 PASS0.373
simple_true-unreach-call3.c below 1 PASS0.357
simple_true-unreach-call4.c below 1 PASS0.362
underapprox_false-unreach-call1.c below 1 OKAY0.41
underapprox_false-unreach-call2.c below 1 OKAY0.401
underapprox_true-unreach-call1.c below 1 FAIL0.402
underapprox_true-unreach-call2.c below 1 PASS0.398
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 14.284
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS1.638
apache-get-tag_true-unreach-call.c below 1 FAIL0.619
down_true-unreach-call.c below 1 PASS0.469
fragtest_simple_true-unreach-call.c below 1 PASS0.596
half_2_true-unreach-call.c below 1 PASS0.499
heapsort_true-unreach-call.c below 1 PASS2.447
id_build_true-unreach-call.c below 1 PASS0.433
id_trans_false-unreach-call.c below 1 OKAY0.371
id_trans_true-unreach-call.c below 1 PASS0.378
large_const_true-unreach-call.c below 1 PASS0.52
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.459
nested6_true-unreach-call.c below 1 FAIL0.626
nested9_true-unreach-call.c below 1 PASS0.745
nest-if3_true-unreach-call.c below 1 PASS0.563
NetBSD_loop_true-unreach-call.c below 1 PASS0.394
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.493
seq_true-unreach-call.c below 1 PASS0.559
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.68
string_concat-noarr_true-unreach-call.c below 1 PASS0.517
up_true-unreach-call.c below 1 PASS0.478
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 14.484
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.441
bhmr2007_true-unreach-call.c below 1 PASS0.446
cggmp2005b_true-unreach-call.c below 1 PASS0.675
cggmp2005_true-unreach-call.c below 1 PASS0.405
cggmp2005_variant_true-unreach-call.c below 1 PASS0.421
css2003_true-unreach-call.c below 1 PASS1.169
ddlm2013_true-unreach-call.c below 1 PASS0.627
gcnr2008_false-unreach-call.c below 1 OKAY1.161
gj2007b_true-unreach-call.c below 1 FAIL0.446
gj2007_true-unreach-call.c below 1 PASS0.586
gr2006_true-unreach-call.c below 1 PASS0.579
gsv2008_true-unreach-call.c below 1 PASS0.392
hhk2008_true-unreach-call.c below 1 PASS0.384
jm2006_true-unreach-call.c below 1 PASS0.527
jm2006_variant_true-unreach-call.c below 1 PASS0.63
mcmillan2006_true-unreach-call.c below 1 FAIL0.459
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 9.348
/bat0/stac/Code/Ark2-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.474
count_by_2_true-unreach-call.c below 1 PASS0.362
count_by_k_true-unreach-call.c below 1 PASS0.367
count_by_nondet_true-unreach-call.c below 1 PASS0.387
gauss_sum_true-unreach-call.c below 1 PASS0.426
half_true-unreach-call.c below 1 FAIL0.413
nested_true-unreach-call.c below 1 PASS0.538
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.337
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.446
array_true-unreach-call.c below 1 FAIL0.435
bubble_sort_false-unreach-call.c below 4 OKAY84.62
bubble_sort_true-unreach-call.c below 1 PASS5.528
compact_false-unreach-call.c below 1 OKAY0.467
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.396
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.4
eureka_01_false-unreach-call.c below 1 OKAY2.818
eureka_01_true-unreach-call.c below 1 FAIL1.706
eureka_05_true-unreach-call.c below 1 FAIL0.898
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.389
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.393
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.371
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.373
heavy_false-unreach-call.c below 1 OKAY0.603
heavy_true-unreach-call.c below 1 PASS0.591
insertion_sort_false-unreach-call.c below 1 OKAY1.621
insertion_sort_true-unreach-call.c below 1 FAIL0.665
invert_string_false-unreach-call.c below 1 OKAY0.607
invert_string_true-unreach-call.c below 1 FAIL0.652
linear_sea.ch_true-unreach-call.c below 1 FAIL0.427
linear_search_false-unreach-call.c below 1 OKAY0.443
lu.cmp_true-unreach-call.c below 3 PASS29.814
ludcmp_false-unreach-call.c below 3 OKAY29.745
matrix_false-unreach-call_true-termination.c below 1 OKAY1.471
matrix_true-unreach-call_true-termination.c below 1 FAIL0.524
n.c11_true-unreach-call.c below 3 FAIL0.592
n.c24_false-unreach-call.c below 3 OKAY5.625
n.c40_true-unreach-call.c below 1 FAIL0.408
nec11_false-unreach-call.c below 1 OKAY0.405
nec20_false-unreach-call.c below 1 OKAY0.452
nec40_true-unreach-call.c below 1 FAIL0.403
string_false-unreach-call.c below 1 OKAY0.789
string_true-unreach-call.c below 1 FAIL0.766
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.74
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.391
sum01_false-unreach-call_true-termination.c below 1 OKAY0.584
sum01_true-unreach-call_true-termination.c below 1 PASS0.404
sum03_false-unreach-call_true-termination.c below 1 OKAY0.649
sum03_true-unreach-call_false-termination.c below 1 PASS0.528
sum04_false-unreach-call_true-termination.c below 1 OKAY0.602
sum04_true-unreach-call_true-termination.c below 1 PASS0.414
sum_array_false-unreach-call.c below 1 OKAY0.662
sum_array_true-unreach-call.c below 1 FAIL0.703
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.357
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.628
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.455
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.377
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.381
trex01_false-unreach-call_true-termination.c below 3 OKAY0.639
trex01_true-unreach-call.c below 3 PASS0.964
trex02_false-unreach-call_true-termination.c below 3 OKAY0.554
trex02_true-unreach-call_true-termination.c below 3 PASS0.545
trex03_false-unreach-call_true-termination.c below 3 OKAY0.9
trex03_true-unreach-call.c below 3 PASS0.906
trex04_true-unreach-call_false-termination.c below 1 PASS0.44
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.403
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS10.189
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.402
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.419
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.559
vogal_false-unreach-call.c below 1 OKAY0.976
vogal_true-unreach-call.c below 1 FAIL0.987
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.334
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.354
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.347
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 209.969
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.685
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.639
Ackermann03_true-unreach-call.c below 7 FAIL1.743
Ackermann04_true-unreach-call.c below 7 FAIL1.71
Addition01_true-unreach-call_true-termination.c below 2 PASS0.835
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.858
Addition03_false-no-overflow.c below 2 PASS0.85
Addition03_true-unreach-call.c below 2 PASS0.859
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.633
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.574
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.581
Fibonacci01_true-unreach-call.c below TIMEOUT 300.005
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.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.006
gcd01_true-unreach-call_true-termination.c below 2 PASS0.757
gcd02_true-unreach-call.c below 2 FAIL1.489
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.308
McCarthy91_true-unreach-call.c below 7 FAIL1.319
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.781
Primes_true-unreach-call.c below 3 FAIL2.465
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL3.803
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.519
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.523
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1524.958
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.584
afterrec_2calls_true-unreach-call.c below 2 PASS0.567
afterrec_false-unreach-call.c below 2 OKAY0.491
afterrec_true-unreach-call.c below 2 PASS0.48
fibo_10_false-unreach-call.c below TIMEOUT 300.004
fibo_10_true-unreach-call.c below TIMEOUT 300.005
fibo_15_false-unreach-call.c below TIMEOUT 300.006
fibo_15_true-unreach-call.c below TIMEOUT 300.005
fibo_20_false-unreach-call.c below TIMEOUT 300.006
fibo_20_true-unreach-call.c below TIMEOUT 300.004
fibo_25_false-unreach-call.c below TIMEOUT 300.006
fibo_25_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.009
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.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.005
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.006
id2_b2_o3_true-unreach-call.c below 2 PASS1.013
id2_b3_o2_false-unreach-call.c below 2 OKAY1.025
id2_b3_o5_true-unreach-call.c below 2 PASS1.018
id2_b5_o10_true-unreach-call.c below 2 PASS0.995
id2_i5_o5_false-unreach-call.c below 2 OKAY0.571
id2_i5_o5_true-unreach-call.c below 2 PASS0.578
id_b2_o3_true-unreach-call.c below 2 PASS0.854
id_b3_o2_false-unreach-call.c below 2 OKAY0.869
id_b3_o5_true-unreach-call.c below 2 PASS0.861
id_b5_o10_true-unreach-call.c below 2 PASS0.843
id_i10_o10_false-unreach-call.c below 2 OKAY0.52
id_i10_o10_true-unreach-call.c below 2 PASS0.513
id_i15_o15_false-unreach-call.c below 2 OKAY0.516
id_i15_o15_true-unreach-call.c below 2 PASS0.507
id_i20_o20_false-unreach-call.c below 2 OKAY0.523
id_i20_o20_true-unreach-call.c below 2 PASS0.512
id_i25_o25_false-unreach-call.c below 2 OKAY0.515
id_i25_o25_true-unreach-call.c below 2 PASS0.511
id_i5_o5_false-unreach-call.c below 2 OKAY0.516
id_i5_o5_true-unreach-call.c below 2 PASS0.523
id_o1000_false-unreach-call.c below 2 OKAY0.515
id_o100_false-unreach-call.c below 2 OKAY0.515
id_o10_false-unreach-call.c below 2 OKAY0.519
id_o200_false-unreach-call.c below 2 OKAY0.501
id_o20_false-unreach-call.c below 2 OKAY0.514
id_o3_false-unreach-call.c below 2 OKAY0.522
sum_10x0_false-unreach-call.c below 2 OKAY0.58
sum_10x0_true-unreach-call.c below 2 PASS0.573
sum_15x0_false-unreach-call.c below 2 OKAY0.587
sum_15x0_true-unreach-call.c below 2 PASS0.569
sum_20x0_false-unreach-call.c below 2 OKAY0.594
sum_20x0_true-unreach-call.c below 2 PASS0.565
sum_25x0_false-unreach-call.c below 2 OKAY0.619
sum_25x0_true-unreach-call.c below 2 PASS0.569
sum_2x3_false-unreach-call.c below 2 OKAY0.594
sum_2x3_true-unreach-call.c below 2 PASS0.572
sum_non_eq_false-unreach-call.c below 2 OKAY0.585
sum_non_eq_true-unreach-call.c below 2 PASS0.558
sum_non_false-unreach-call.c below 2 OKAY0.577
sum_non_true-unreach-call.c below 2 PASS0.582
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9027.271
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-lit
rec-afnp2014_true-unreach-call.c below 2 PASS0.584
rec-bhmr2007_true-unreach-call.c below 2 PASS0.596
rec-cggmp2005b_true-unreach-call.c below 3 PASS1.16
rec-cggmp2005_true-unreach-call.c below 2 PASS0.537
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.561
rec-css2003_true-unreach-call.c below 2 PASS1.576
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.005
rec-gcnr2008_false-unreach-call.c below 2 OKAY1.148
rec-gj2007b_true-unreach-call.c below 2 FAIL0.531
rec-gj2007_true-unreach-call.c below 2 FAIL0.679
rec-gr2006_true-unreach-call.c below 2 FAIL0.688
rec-gsv2008_true-unreach-call.c below 2 PASS0.552
rec-hhk2008_true-unreach-call.c below 2 PASS0.521
rec-jm2006_true-unreach-call.c below 2 PASS0.676
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.765
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.644
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 311.223
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c below 2 PASS0.483
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.57
rec-count_by_2_true-unreach-call.c below 2 PASS0.472
rec-count_by_k_true-unreach-call.c below 2 PASS0.5
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.525
rec-gauss_sum_true-unreach-call.c below 2 PASS0.557
rec-half_true-unreach-call.c below 2 FAIL0.535
rec-nested_true-unreach-call.c below 3 FAIL0.893
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 4.535
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 FAIL0.656
cubic_polynomial_unsafe.c below 2 OKAY0.655
edit_distance_bottom_up.c below 3 FAIL203.515
edit_distance_top_down.c below 3 FAIL5.657
log_log_n_solution.c below 3 FAIL0.617
log_log_n_solution_unsafe.c below 3 OKAY0.609
log_n_solution.c below 2 FAIL0.629
log_n_solution_unsafe.c below 2 OKAY0.636
multivariate_1.c below TIMEOUT 300.103
multivariate_1_unsafe.c below TIMEOUT 300.007
multivariate_higher_order.c below 7 FAIL3.847
multivariate_higher_order_unsafe.c below 7 OKAY3.725
n_cubed_solution.c below EXCEPTION 109.201
n_cubed_solution_unsafe.c below EXCEPTION 0.028
n_log_n_solution.c below 8 FAIL1.76
n_log_n_solution_unsafe.c below 8 OKAY1.742
n_squared_two_base_case_even.c below 2 PASS0.716
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.713
n_squared_two_base_case_odd.c below 2 PASS0.781
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.77
pascals_dynamic.c below 3 FAIL2.855
pascals_dynamic_unsafe.c below 3 OKAY2.853
pascals_iterative.c below 1 FAIL5.344
pascals_iterative_unsafe.c below 1 OKAY5.331
pascals_recursive.c below 8 FAIL4.092
pascals_recursive_unsafe.c below 8 OKAY3.95
squared_solution.c below 8 FAIL3.358
squared_solution_unsafe.c below 8 OKAY3.346
two_n_even.c below 2 PASS0.541
two_n_even_unsafe.c below 2 OKAY0.551
two_n_odd.c below 2 PASS0.546
two_n_odd_unsafe.c below 2 OKAY0.547
two_to_n_over_two_even.c below 7 FAIL256.512
two_to_n_over_two_even_unsafe.c below 7 OKAY100.982
two_to_n_over_two_odd.c below 7 FAIL135.572
two_to_n_over_two_odd_unsafe.c below 7 OKAY162.646
two_to_n_squared.c below 5 FAIL22.231
two_to_n_squared_unsafe.c below 5 OKAY22.155
two_to_two_to_n.c below 7 FAIL1.525
two_to_two_to_n_unsafe.c below 7 OKAY1.531
ICRA Assertions (True) = 4/21
ICRA Assertions (False) = 17/19
ICRA Time = 1672.835
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.442
adding_and_mult_unsafe.c below 1 OKAY0.425
binary_search_array_tree.c below 1 FAIL0.841
exp_add_linear.c below 1 PASS0.562
exp_add_linear_unsafe.c below 1 OKAY0.562
exp_add_loop_rec.c below 1 FAIL0.416
exp_add_loop_rec_unsafe.c below 1 OKAY0.414
exp_add_loop_variable.c below 1 PASS0.509
exp_add_loop_variable_unsafe.c below 1 OKAY0.526
exp_with_linear_inner_loop.c below 1 FAIL0.637
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.632
halving_log1.c below 1 FAIL0.679
linear_two_to_n.c below 7 FAIL1.856
linear_two_to_n_unsafe.c below 7 OKAY1.877
loop_five_to_n.c below 1 PASS0.49
loop_five_to_n_unsafe.c below 1 OKAY0.482
non_loop_five_to_n.c below 7 FAIL58.53
non_loop_five_to_n_unsafe.c below 7 OKAY58.557
power_log.c below 1 PASS0.681
power_log_modified.c below 1 PASS0.687
simple_exponential.c below 1 PASS0.465
simple_exponential_for.c below 1 PASS0.49
simple_exponential_for_unsafe.c below 1 OKAY0.479
simple_exponential_unsafe.c below 1 OKAY0.471
two_to_n_minus_n.c below 7 FAIL2.541
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) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 736.87
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.722
02.c below 3 FAIL0.94
03.c below 1 PASS0.547
04.c below 1 PASS0.407
05.c below 3 PASS1.413
06.c below 3 FAIL11.038
07.c below 3 PASS0.721
08.c below 3 PASS1.731
09.c below 3 PASS1.162
10.c below 3 FAIL1.367
11.c below 1 PASS0.404
12.c below 3 PASS1.733
13.c below 3 PASS0.738
14.c below 3 PASS0.611
15.c below 1 PASS0.397
16.c below 1 PASS0.541
17.c below 1 PASS3.746
18.c below 1 PASS0.497
19.c below 1 PASS0.567
20.c below 3 FAIL0.843
21.c below 3 PASS0.715
22.c below 3 FAIL0.96
23.c below 1 PASS0.426
24.c below 1 PASS0.483
25.c below 3 FAIL1.831
26.c below TIMEOUT 300.004
27.c below 1 PASS0.559
28.c below 3 PASS0.718
29.c below 3 PASS1.298
30.c below 1 PASS0.427
31.c below 3 PASS1.422
32.c below 1 FAIL0.451
33.c below 3 PASS1.532
34.c below 1 FAIL0.488
35.c below 1 PASS0.384
36.c below 3 PASS3.18
37.c below 3 FAIL0.663
38.c below 1 FAIL0.469
39.c below 3 PASS0.597
40.c below 3 PASS1.087
41.c below 1 PASS0.511
42.c below 3 PASS1.322
43.c below 3 PASS0.833
44.c below 1 PASS0.585
45.c below 3 FAIL3.644
46.c below 3 FAIL2.429
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 357.143
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.617
AGHKTW2017_foo.c below 1 PASS0.561
AGHKTW2017_loginSafe.c below 1 PASS1.16
AGHKTW2017_loopAndBranch_safe.c below 1 PASS0.602
AGHKTW2017_loopAndBranch_unsafe.c below 1 OKAY0.659
BCK2011_gauss.c below 1 PASS0.584
BCK2011_strength_reduction.c below 1 PASS0.926
BCK2011_strength_reduction_linear.c below 1 PASS0.569
fibonacci_information_flow.c below 1 PASS0.725
loop_splitting_test_safe.c below 1 PASS0.73
TA2005_fib2.c below 1 PASS0.739
TA2005_fib.c below 1 PASS0.575
ICRA Assertions (True) = 11/11
ICRA Assertions (False) = 1/1
ICRA Time = 8.447