[Version Information]
WALi-OpenNWA version: 088075c428c89531f84bc48ca70e4f182df9184b (2017-08-09 10:53:57 -0500) "the scripts used for POPL18 submission and fixed soundness errors for nightly run"
duet version: 7a637cd53ac9dd819b179b14263f4763715db4a5 (2017-08-21 16:13:10 -0400) "Merge remote-tracking branch 'origin/ark2' into Newton-ark2"
# 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.374
kmp.c below 1 PASS1.075
qsort.c below 4 PASS0.905
speed_pldi09_fig1.c below 1 PASS0.51
speed_pldi09_fig4_2.c below 1 FAIL0.397
speed_pldi09_fig4_4.c below 1 PASS0.523
speed_pldi09_fig4_5.c below 1 PASS0.406
speed_pldi10_ex1.c below 1 PASS1.225
speed_pldi10_ex3.c below 1 PASS0.508
speed_pldi10_ex4.c below 1 PASS0.522
speed_popl10_fig2_1.c below 1 PASS0.465
speed_popl10_fig2_2.c below 1 FAIL0.391
speed_popl10_nested_multiple.c below 1 PASS0.474
speed_popl10_nested_single.c below 1 PASS0.442
speed_popl10_sequential_single.c below 1 PASS0.411
speed_popl10_simple_multiple.c below 1 PASS0.509
speed_popl10_simple_single_2.c below 1 PASS0.654
speed_popl10_simple_single.c below 1 PASS0.336
t07.c below 1 PASS0.431
t08.c below 1 PASS0.382
t09.c below 1 PASS0.398
t10.c below 1 PASS0.367
t11.c below 1 PASS0.494
t13.c below 1 FAIL0.427
t15.c below 1 PASS0.413
t16.c below 1 PASS0.399
t19.c below 1 PASS0.385
t20.c below 1 PASS0.392
t27.c below 1 PASS0.558
t28.c below 1 PASS0.463
t30.c below 1 FAIL0.423
t37.c below 2 PASS0.595
t39.c below 2 PASS0.539
t46.c below 1 PASS0.417
t47.c below 1 PASS0.507
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 17.717
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.379
qsort_full.c below 4 PASS9.263
rec1-param_safe.c below 2 PASS0.384
rec1-param_unsafe.c below 2 OKAY0.375
rec1_safe.c below 2 PASS0.363
rec1_unsafe.c below 2 OKAY0.355
rec2-param_safe.c below 2 PASS0.388
rec2-param_unsafe.c below 2 OKAY0.365
rec2_safe.c below 2 PASS0.369
rec2_unsafe.c below 2 OKAY0.37
rec-test.c below 2 PASS0.373
sas03_bothbranches.c below 7 PASS0.804
sas03.c below 2 PASS0.71
simulated_lese_recursive.c below 2 PASS0.447
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 14.945
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.336
count_up_down_unsafe.c below 1 OKAY0.34
divide.c below 1 PASS0.342
factor_unsafe.c below 1 OKAY0.335
for_infinite_loop_1_safe.c below 1 PASS0.337
for_infinite_loop_2_safe.c below 1 PASS0.32
interproc.c below 1 PASS0.304
mult.c below 1 PASS0.335
pointer_arith.c below 1 PASS0.296
quotient.c below 3 PASS0.497
subtract.c below 1 PASS0.326
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.343
sum01_bug02_unsafe.c below 1 OKAY0.574
sum01_real_safe.c below 1 PASS0.336
sum01_safe.c below 1 PASS0.342
sum01_unsafe.c below 1 OKAY0.449
sum02_safe.c below 1 PASS0.358
sum03_safe.c below 1 PASS0.443
sum03_unsafe.c below 1 OKAY0.483
sum04_safe.c below 1 PASS0.351
sum04_unsafe.c below 1 OKAY0.455
terminator_02_safe.c below 1 PASS0.33
terminator_02_unsafe.c below 1 OKAY0.362
terminator_03_safe.c below 1 PASS0.33
terminator_03_unsafe.c below 1 OKAY0.341
token_ring01_safe.c below 4 FAIL140.712
token_ring01_unsafe.c below 4 OKAY240.04
toy_safe.c below EXCEPTION 166.528
trex01_safe.c below 1 PASS2.906
trex01_unsafe.c below 1 OKAY0.377
trex02_safe2.c below 3 PASS0.4
trex02_safe.c below 3 PASS0.394
trex02_unsafe.c below 3 OKAY0.397
trex03_safe.c below 1 PASS0.433
trex03_unsafe.c below 1 OKAY0.438
trex04_safe.c below 1 PASS0.351
while_infinite_loop_1_safe.c below 1 PASS0.297
while_infinite_loop_2_safe.c below 1 PASS0.3
while_infinite_loop_3_safe.c below 1 PASS0.327
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 563.165
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.417
blogger_simplified1.c below 3 PASS1.098
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.385
mult-proc-params.c below 3 PASS0.411
popall.c below 1 PASS0.659
simulated_scc.c below 1 PASS0.627
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.602
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.351
degree2_binomial.c below 1 PASS0.682
degree2_monomial.c below 1 PASS0.403
degree3_binomial.c below 1 FAIL2.172
degree3_monomial.c below 1 PASS0.45
degree4_binomial.c below 1 FAIL6.912
degree4_monomial.c below 1 PASS0.545
degree5_binomial.c below 1 TIMEOUT300.017
degree5_monomial.c below 1 PASS0.63
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 312.162
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.454
cubic_with_square_interproc.c below 2 FAIL0.584
cubic_with_square_nonlinear.c below 1 FAIL0.391
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.437
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.386
cubic_with_square_unsafe.c below 1 OKAY0.451
multi-input.c below 1 FAIL0.497
multi-input_unsafe.c below 1 OKAY0.479
nondet_loop_bound.c below 1 FAIL0.362
nondet_loop_bound_quartic.c below 1 FAIL0.38
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.38
nondet_loop_bound_unsafe.c below 1 OKAY0.35
nonlinear_stratified.c below 1 TIMEOUT300.004
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.005
quartic_with_cube.c below 1 FAIL0.599
quartic_with_cube_nonlinear.c below 1 FAIL0.391
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.391
quartic_with_cube_unsafe.c below 1 OKAY0.52
quintic_with_quartic.c below 1 PASS1.029
quintic_with_quartic_nonlinear.c below 1 TIMEOUT300.009
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.539
quintic_with_quartic_unsafe.c below 1 OKAY1.042
ICRA Assertions (True) = 1/12
ICRA Assertions (False) = 9/10
ICRA Time = 909.68
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.701
degree2_FD_AllAux_AllAssm.c below 1 PASS102.601
degree2_FD_AllAux_FewAssm.c below 1 PASS6.374
degree2_FD_FewAux_FewAssm.c below 1 PASS1.037
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.037
degree3.c below 1 PASS0.734
degree3_FD.c below 1 PASS0.938
degree4.c below 1 PASS0.459
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 113.881
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.431
loop_unsafe.c below 1 OKAY0.445
simulated_lese_parser.c below 1 PASS0.357
simulated_lese_sentinel.c below 1 PASS0.355
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.588
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.345
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.345
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.009
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.009
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.364
array_false-unreach-call2.c below 1 OKAY0.373
array_false-unreach-call3.c below 1 OKAY0.348
array_true-unreach-call1.c below 1 FAIL0.357
array_true-unreach-call2.c below 1 FAIL0.37
array_true-unreach-call3.c below 1 PASS0.348
array_true-unreach-call4.c below 1 FAIL0.341
const_false-unreach-call1.c below 1 OKAY0.342
const_true-unreach-call1.c below 1 PASS0.345
diamond_false-unreach-call1.c below 1 OKAY0.355
diamond_true-unreach-call1.c below 1 PASS0.363
diamond_true-unreach-call2.c below 1 PASS0.387
functions_false-unreach-call1.c below 3 OKAY0.383
functions_true-unreach-call1.c below 3 PASS0.382
multivar_false-unreach-call1.c below 1 OKAY0.354
multivar_true-unreach-call1.c below 1 PASS0.342
nested_false-unreach-call1.c below 1 OKAY0.373
nested_true-unreach-call1.c below 1 PASS0.368
overflow_true-unreach-call1.c below 1 PASS0.316
phases_false-unreach-call1.c below 1 OKAY0.406
phases_false-unreach-call2.c below 1 OKAY0.357
phases_true-unreach-call1.c below 1 PASS0.393
phases_true-unreach-call2.c below 1 PASS0.34
simple_false-unreach-call1.c below 1 OKAY0.32
simple_false-unreach-call2.c below 1 OKAY0.324
simple_false-unreach-call3.c below 1 OKAY0.327
simple_false-unreach-call4.c below 1 OKAY0.323
simple_true-unreach-call1.c below 1 PASS0.34
simple_true-unreach-call2.c below 1 PASS0.322
simple_true-unreach-call3.c below 1 PASS0.326
simple_true-unreach-call4.c below 1 PASS0.32
underapprox_false-unreach-call1.c below 1 OKAY0.357
underapprox_false-unreach-call2.c below 1 OKAY0.348
underapprox_true-unreach-call1.c below 1 FAIL0.357
underapprox_true-unreach-call2.c below 1 PASS0.382
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.353
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.991
apache-get-tag_true-unreach-call.c below 1 FAIL0.439
down_true-unreach-call.c below 1 PASS0.387
fragtest_simple_true-unreach-call.c below 1 PASS0.461
half_2_true-unreach-call.c below 1 PASS0.4
heapsort_true-unreach-call.c below 1 PASS115.62
id_build_true-unreach-call.c below 1 PASS0.357
id_trans_false-unreach-call.c below 1 OKAY0.331
id_trans_true-unreach-call.c below 1 PASS0.344
large_const_true-unreach-call.c below 1 PASS0.44
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.394
nested6_true-unreach-call.c below 1 FAIL0.464
nested9_true-unreach-call.c below 1 PASS0.539
nest-if3_true-unreach-call.c below 1 PASS0.444
NetBSD_loop_true-unreach-call.c below 1 PASS0.337
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.379
seq_true-unreach-call.c below 1 PASS0.422
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.145
string_concat-noarr_true-unreach-call.c below 1 PASS0.394
up_true-unreach-call.c below 1 PASS0.377
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 124.665
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.36
bhmr2007_true-unreach-call.c below 1 PASS0.386
cggmp2005b_true-unreach-call.c below 1 PASS0.512
cggmp2005_true-unreach-call.c below 1 PASS0.36
cggmp2005_variant_true-unreach-call.c below 1 PASS0.374
css2003_true-unreach-call.c below 1 PASS0.819
ddlm2013_true-unreach-call.c below 1 PASS0.507
gcnr2008_false-unreach-call.c below 1 OKAY0.94
gj2007b_true-unreach-call.c below 1 FAIL0.37
gj2007_true-unreach-call.c below 1 PASS0.448
gr2006_true-unreach-call.c below 1 PASS0.415
gsv2008_true-unreach-call.c below 1 PASS0.353
hhk2008_true-unreach-call.c below 1 PASS0.325
jm2006_true-unreach-call.c below 1 PASS0.415
jm2006_variant_true-unreach-call.c below 1 PASS0.47
mcmillan2006_true-unreach-call.c below 1 FAIL0.384
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.438
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.32
count_by_1_variant_true-unreach-call.c below 1 PASS0.393
count_by_2_true-unreach-call.c below 1 PASS0.326
count_by_k_true-unreach-call.c below 1 PASS0.339
count_by_nondet_true-unreach-call.c below 1 PASS0.343
gauss_sum_true-unreach-call.c below 1 PASS0.369
half_true-unreach-call.c below 1 FAIL0.379
nested_true-unreach-call.c below 1 PASS0.414
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.883
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.415
array_true-unreach-call.c below 1 FAIL0.386
bubble_sort_false-unreach-call.c below 4 OKAY70.967
bubble_sort_true-unreach-call.c below 1 PASS4.186
compact_false-unreach-call.c below 1 OKAY0.391
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.353
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.338
eureka_01_false-unreach-call.c below 1 OKAY2.148
eureka_01_true-unreach-call.c below 1 FAIL1.443
eureka_05_true-unreach-call.c below 1 FAIL0.688
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.327
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.34
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.321
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.321
heavy_false-unreach-call.c below 1 OKAY0.482
heavy_true-unreach-call.c below 1 PASS0.452
insertion_sort_false-unreach-call.c below 1 OKAY1.343
insertion_sort_true-unreach-call.c below 1 FAIL0.568
invert_string_false-unreach-call.c below 1 OKAY0.471
invert_string_true-unreach-call.c below 1 FAIL0.509
linear_sea.ch_true-unreach-call.c below 1 FAIL0.394
linear_search_false-unreach-call.c below 1 OKAY0.393
lu.cmp_true-unreach-call.c below 3 PASS25.196
ludcmp_false-unreach-call.c below 3 OKAY25.495
matrix_false-unreach-call_true-termination.c below 1 OKAY1.157
matrix_true-unreach-call_true-termination.c below 1 FAIL0.445
n.c11_true-unreach-call.c below 3 FAIL0.441
n.c24_false-unreach-call.c below 3 OKAY5.925
n.c40_true-unreach-call.c below 1 FAIL0.362
nec11_false-unreach-call.c below 1 OKAY0.368
nec20_false-unreach-call.c below 1 OKAY0.382
nec40_true-unreach-call.c below 1 FAIL0.359
string_false-unreach-call.c below 1 OKAY0.583
string_true-unreach-call.c below 1 FAIL0.594
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.558
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.351
sum01_false-unreach-call_true-termination.c below 1 OKAY0.441
sum01_true-unreach-call_true-termination.c below 1 PASS0.364
sum03_false-unreach-call_true-termination.c below 1 OKAY0.479
sum03_true-unreach-call_false-termination.c below 1 PASS0.432
sum04_false-unreach-call_true-termination.c below 1 OKAY0.455
sum04_true-unreach-call_true-termination.c below 1 PASS0.351
sum_array_false-unreach-call.c below 1 OKAY0.544
sum_array_true-unreach-call.c below 1 FAIL0.57
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.327
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.464
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.366
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.328
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.327
trex01_false-unreach-call_true-termination.c below 3 OKAY0.474
trex01_true-unreach-call.c below 3 PASS0.781
trex02_false-unreach-call_true-termination.c below 3 OKAY0.395
trex02_true-unreach-call_true-termination.c below 3 PASS0.397
trex03_false-unreach-call_true-termination.c below 3 OKAY0.692
trex03_true-unreach-call.c below 3 PASS0.699
trex04_true-unreach-call_false-termination.c below 1 PASS0.368
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.346
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS7.129
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.37
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.361
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY7.004
vogal_false-unreach-call.c below 1 OKAY0.713
vogal_true-unreach-call.c below 1 FAIL0.721
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.287
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.306
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.31
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.306
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 176.559
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.212
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.136
Ackermann03_true-unreach-call.c below 7 FAIL1.193
Ackermann04_true-unreach-call.c below 7 FAIL1.175
Addition01_true-unreach-call_true-termination.c below 2 PASS0.565
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.581
Addition03_false-no-overflow.c below 2 PASS0.569
Addition03_true-unreach-call.c below 2 PASS0.588
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.538
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.438
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.438
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.004
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.006
gcd01_true-unreach-call_true-termination.c below 2 PASS0.56
gcd02_true-unreach-call.c below 2 FAIL1.019
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.885
McCarthy91_true-unreach-call.c below 7 FAIL0.937
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.569
Primes_true-unreach-call.c below 3 FAIL1.564
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL2.689
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.395
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.393
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1517.468
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.425
afterrec_2calls_true-unreach-call.c below 2 PASS0.399
afterrec_false-unreach-call.c below 2 OKAY0.365
afterrec_true-unreach-call.c below 2 PASS0.365
fibo_10_false-unreach-call.c below TIMEOUT 300.004
fibo_10_true-unreach-call.c below TIMEOUT 300.006
fibo_15_false-unreach-call.c below TIMEOUT 300.007
fibo_15_true-unreach-call.c below TIMEOUT 300.004
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.004
fibo_25_true-unreach-call.c below TIMEOUT 300.007
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.018
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.022
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.022
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.022
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.022
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.019
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.016
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.022
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.005
id2_b2_o3_true-unreach-call.c below 2 PASS0.684
id2_b3_o2_false-unreach-call.c below 2 OKAY0.689
id2_b3_o5_true-unreach-call.c below 2 PASS0.698
id2_b5_o10_true-unreach-call.c below 2 PASS0.695
id2_i5_o5_false-unreach-call.c below 2 OKAY0.42
id2_i5_o5_true-unreach-call.c below 2 PASS0.422
id_b2_o3_true-unreach-call.c below 2 PASS0.6
id_b3_o2_false-unreach-call.c below 2 OKAY0.607
id_b3_o5_true-unreach-call.c below 2 PASS0.585
id_b5_o10_true-unreach-call.c below 2 PASS0.598
id_i10_o10_false-unreach-call.c below 2 OKAY0.384
id_i10_o10_true-unreach-call.c below 2 PASS0.388
id_i15_o15_false-unreach-call.c below 2 OKAY0.384
id_i15_o15_true-unreach-call.c below 2 PASS0.386
id_i20_o20_false-unreach-call.c below 2 OKAY0.372
id_i20_o20_true-unreach-call.c below 2 PASS0.392
id_i25_o25_false-unreach-call.c below 2 OKAY0.38
id_i25_o25_true-unreach-call.c below 2 PASS0.375
id_i5_o5_false-unreach-call.c below 2 OKAY0.391
id_i5_o5_true-unreach-call.c below 2 PASS0.384
id_o1000_false-unreach-call.c below 2 OKAY0.384
id_o100_false-unreach-call.c below 2 OKAY0.395
id_o10_false-unreach-call.c below 2 OKAY0.382
id_o200_false-unreach-call.c below 2 OKAY0.409
id_o20_false-unreach-call.c below 2 OKAY0.389
id_o3_false-unreach-call.c below 2 OKAY0.395
sum_10x0_false-unreach-call.c below 2 OKAY0.431
sum_10x0_true-unreach-call.c below 2 PASS0.421
sum_15x0_false-unreach-call.c below 2 OKAY0.434
sum_15x0_true-unreach-call.c below 2 PASS0.418
sum_20x0_false-unreach-call.c below 2 OKAY0.432
sum_20x0_true-unreach-call.c below 2 PASS0.423
sum_25x0_false-unreach-call.c below 2 OKAY0.435
sum_25x0_true-unreach-call.c below 2 PASS0.426
sum_2x3_false-unreach-call.c below 2 OKAY0.419
sum_2x3_true-unreach-call.c below 2 PASS0.435
sum_non_eq_false-unreach-call.c below 2 OKAY0.422
sum_non_eq_true-unreach-call.c below 2 PASS0.422
sum_non_false-unreach-call.c below 2 OKAY0.43
sum_non_true-unreach-call.c below 2 PASS0.435
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9020.086
/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.452
rec-bhmr2007_true-unreach-call.c below 2 PASS0.408
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.654
rec-cggmp2005_true-unreach-call.c below 2 PASS0.365
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.403
rec-css2003_true-unreach-call.c below 2 PASS0.973
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.824
rec-gj2007b_true-unreach-call.c below 2 FAIL0.377
rec-gj2007_true-unreach-call.c below 2 FAIL0.455
rec-gr2006_true-unreach-call.c below 2 FAIL0.499
rec-gsv2008_true-unreach-call.c below 2 PASS0.392
rec-hhk2008_true-unreach-call.c below 2 PASS0.399
rec-jm2006_true-unreach-call.c below 2 PASS0.432
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.513
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.441
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 307.591
/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.374
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.405
rec-count_by_2_true-unreach-call.c below 2 PASS0.37
rec-count_by_k_true-unreach-call.c below 2 PASS0.395
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.401
rec-gauss_sum_true-unreach-call.c below 2 PASS0.437
rec-half_true-unreach-call.c below 2 FAIL0.41
rec-nested_true-unreach-call.c below 3 FAIL0.564
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.356
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.548
cubic_polynomial_unsafe.c below 2 OKAY0.529
edit_distance_bottom_up.c below 3 FAIL171.944
edit_distance_top_down.c below 3 FAIL4.143
log_log_n_solution.c below 3 FAIL0.439
log_log_n_solution_unsafe.c below 3 OKAY0.442
log_n_solution.c below 2 FAIL0.453
log_n_solution_unsafe.c below 2 OKAY0.46
multivariate_1.c below TIMEOUT 300.005
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL2.475
multivariate_higher_order_unsafe.c below 7 OKAY2.581
n_cubed_solution.c below EXCEPTION 74.885
n_cubed_solution_unsafe.c below EXCEPTION 0.025
n_log_n_solution.c below 8 FAIL1.204
n_log_n_solution_unsafe.c below 8 OKAY1.129
n_squared_two_base_case_even.c below 2 PASS0.575
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.571
n_squared_two_base_case_odd.c below 2 PASS0.597
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.557
pascals_dynamic.c below 3 FAIL2.311
pascals_dynamic_unsafe.c below 3 OKAY2.245
pascals_iterative.c below 1 FAIL4.252
pascals_iterative_unsafe.c below 1 OKAY4.365
pascals_recursive.c below 9 FAIL3.427
pascals_recursive_unsafe.c below 9 OKAY3.535
squared_solution.c below 8 FAIL2.76
squared_solution_unsafe.c below 8 OKAY2.702
two_n_even.c below 2 PASS0.405
two_n_even_unsafe.c below 2 OKAY0.43
two_n_odd.c below 2 PASS0.406
two_n_odd_unsafe.c below 2 OKAY0.411
two_to_n_over_two_even.c below 7 FAIL1.074
two_to_n_over_two_even_unsafe.c below 7 OKAY1.073
two_to_n_over_two_odd.c below 7 FAIL1.062
two_to_n_over_two_odd_unsafe.c below 7 OKAY1.131
two_to_n_squared.c below 5 FAIL16.697
two_to_n_squared_unsafe.c below 5 OKAY16.698
two_to_two_to_n.c below 7 FAIL1.017
two_to_two_to_n_unsafe.c below 7 OKAY1.014
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 17/19
ICRA Time = 930.582
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.36
adding_and_mult_unsafe.c below 1 OKAY0.365
binary_search_array_tree.c below 1 FAIL0.618
exp_add_linear.c below 1 PASS0.43
exp_add_linear_unsafe.c below 1 OKAY0.447
exp_add_loop_rec.c below 1 FAIL0.36
exp_add_loop_rec_unsafe.c below 1 OKAY0.362
exp_add_loop_variable.c below 1 PASS0.43
exp_add_loop_variable_unsafe.c below 1 OKAY0.41
exp_with_linear_inner_loop.c below 1 FAIL0.481
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.464
halving_log1.c below 1 FAIL0.525
linear_two_to_n.c below 7 FAIL20.657
linear_two_to_n_unsafe.c below 7 OKAY20.603
loop_five_to_n.c below 1 PASS0.383
loop_five_to_n_unsafe.c below 1 OKAY0.395
non_loop_five_to_n.c below 7 FAIL49.666
non_loop_five_to_n_unsafe.c below 7 OKAY49.529
power_log.c below 1 PASS0.481
power_log_modified.c below 1 PASS0.506
simple_exponential.c below 1 PASS0.408
simple_exponential_for.c below 1 PASS0.401
simple_exponential_for_unsafe.c below 1 OKAY0.383
simple_exponential_unsafe.c below 1 OKAY0.378
two_to_n_minus_n.c below 7 FAIL2.643
two_to_n_minus_n_loop.c below TIMEOUT 300.024
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.026
two_to_n_minus_n_unsafe.c below 7 OKAY2.65
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 754.385
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.549
02.c below 3 FAIL0.704
03.c below 1 PASS0.429
04.c below 1 PASS0.347
05.c below 3 PASS0.985
06.c below 3 FAIL7.012
07.c below 3 PASS0.542
08.c below 3 PASS1.158
09.c below 3 PASS0.724
10.c below 3 FAIL0.884
11.c below 1 PASS0.345
12.c below 3 PASS1.293
13.c below 3 PASS0.543
14.c below 3 PASS0.449
15.c below 1 PASS0.358
16.c below 1 PASS0.425
17.c below 1 PASS0.431
18.c below 1 PASS0.409
19.c below 1 PASS0.439
20.c below 3 FAIL0.602
21.c below 3 PASS0.482
22.c below 3 FAIL0.67
23.c below 1 PASS0.397
24.c below 1 PASS0.445
25.c below 3 FAIL1.313
26.c below TIMEOUT 300.005
27.c below 1 PASS0.442
28.c below 3 PASS0.476
29.c below 3 PASS0.879
30.c below 1 PASS0.354
31.c below 3 PASS0.801
32.c below 1 FAIL0.373
33.c below 3 PASS1.049
34.c below 1 FAIL0.381
35.c below 1 PASS0.336
36.c below 3 PASS2.327
37.c below 3 FAIL0.476
38.c below 1 FAIL0.374
39.c below 3 PASS0.41
40.c below 3 PASS0.651
41.c below 1 PASS0.385
42.c below 3 PASS0.771
43.c below 3 PASS0.44
44.c below 1 PASS0.368
45.c below 3 FAIL2.169
46.c below 3 FAIL1.38
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 336.782
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.39
AGHKTW2017_foo.c below 1 PASS0.392
AGHKTW2017_loginSafe.c below 1 PASS0.797
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.461
BCK2011_gauss.c below 1 PASS0.43
BCK2011_strength_reduction.c below 1 PASS0.4
BCK2011_strength_reduction_linear.c below 1 PASS0.44
fibonacci_information_flow.c below 1 PASS0.584
TA2005_fib2.c below 1 PASS0.578
TA2005_fib.c below 1 PASS0.473
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.945