[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.383
kmp.c below 1 PASS1.169
qsort.c below 4 PASS0.973
speed_pldi09_fig1.c below 1 PASS0.523
speed_pldi09_fig4_2.c below 1 FAIL0.415
speed_pldi09_fig4_4.c below 1 PASS0.537
speed_pldi09_fig4_5.c below 1 PASS0.431
speed_pldi10_ex1.c below 1 PASS1.331
speed_pldi10_ex3.c below 1 PASS0.534
speed_pldi10_ex4.c below 1 PASS0.553
speed_popl10_fig2_1.c below 1 PASS0.49
speed_popl10_fig2_2.c below 1 FAIL0.387
speed_popl10_nested_multiple.c below 1 PASS0.483
speed_popl10_nested_single.c below 1 PASS0.454
speed_popl10_sequential_single.c below 1 PASS0.414
speed_popl10_simple_multiple.c below 1 PASS0.533
speed_popl10_simple_single_2.c below 1 PASS0.671
speed_popl10_simple_single.c below 1 PASS0.368
t07.c below 1 PASS0.446
t08.c below 1 PASS0.417
t09.c below 1 PASS0.412
t10.c below 1 PASS0.384
t11.c below 1 PASS0.501
t13.c below 1 FAIL0.436
t15.c below 1 PASS0.436
t16.c below 1 PASS0.412
t19.c below 1 PASS0.412
t20.c below 1 PASS0.404
t27.c below 1 PASS0.573
t28.c below 1 PASS0.494
t30.c below 1 FAIL0.426
t37.c below 2 PASS0.634
t39.c below 2 PASS0.564
t46.c below 1 PASS0.443
t47.c below 1 PASS0.552
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 18.595
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.402
qsort_full.c below 4 PASS10.33
rec1-param_safe.c below 2 PASS0.399
rec1-param_unsafe.c below 2 OKAY0.392
rec1_safe.c below 2 PASS0.371
rec1_unsafe.c below 2 OKAY0.401
rec2-param_safe.c below 2 PASS0.386
rec2-param_unsafe.c below 2 OKAY0.373
rec2_safe.c below 2 PASS0.381
rec2_unsafe.c below 2 OKAY0.374
rec-test.c below 2 PASS0.373
sas03_bothbranches.c below 7 PASS0.842
sas03.c below 2 PASS0.748
simulated_lese_recursive.c below 2 PASS0.554
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 16.326
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.339
count_up_down_unsafe.c below 1 OKAY0.352
divide.c below 1 PASS0.344
factor_unsafe.c below 1 OKAY0.337
for_infinite_loop_1_safe.c below 1 PASS0.328
for_infinite_loop_2_safe.c below 1 PASS0.335
interproc.c below 1 PASS0.326
mult.c below 1 PASS0.345
pointer_arith.c below 1 PASS0.316
quotient.c below 3 PASS0.51
subtract.c below 1 PASS0.338
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.353
sum01_bug02_unsafe.c below 1 OKAY0.6
sum01_real_safe.c below 1 PASS0.362
sum01_safe.c below 1 PASS0.359
sum01_unsafe.c below 1 OKAY0.47
sum02_safe.c below 1 PASS0.377
sum03_safe.c below 1 PASS0.43
sum03_unsafe.c below 1 OKAY0.466
sum04_safe.c below 1 PASS0.377
sum04_unsafe.c below 1 OKAY0.474
terminator_02_safe.c below 1 PASS0.337
terminator_02_unsafe.c below 1 OKAY0.367
terminator_03_safe.c below 1 PASS0.35
terminator_03_unsafe.c below 1 OKAY0.345
token_ring01_safe.c below 4 FAIL158.928
token_ring01_unsafe.c below 4 OKAY262.086
toy_safe.c below EXCEPTION 178.397
trex01_safe.c below 1 PASS0.747
trex01_unsafe.c below 1 OKAY0.387
trex02_safe2.c below 3 PASS0.417
trex02_safe.c below 3 PASS0.417
trex02_unsafe.c below 3 OKAY0.422
trex03_safe.c below 1 PASS0.452
trex03_unsafe.c below 1 OKAY0.449
trex04_safe.c below 1 PASS0.364
while_infinite_loop_1_safe.c below 1 PASS0.344
while_infinite_loop_2_safe.c below 1 PASS0.313
while_infinite_loop_3_safe.c below 1 PASS0.323
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 613.583
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.427
blogger_simplified1.c below 3 PASS1.164
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.397
mult-proc-params.c below 3 PASS0.412
popall.c below 1 PASS0.729
simulated_scc.c below 1 PASS0.68
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.813
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.388
degree2_binomial.c below 1 PASS0.738
degree2_monomial.c below 1 PASS0.426
degree3_binomial.c below 1 FAIL2.377
degree3_monomial.c below 1 PASS0.463
degree4_binomial.c below 1 FAIL7.785
degree4_monomial.c below 1 PASS0.556
degree5_binomial.c below 1 TIMEOUT300.019
degree5_monomial.c below 1 PASS0.65
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 313.402
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.477
cubic_with_square_interproc.c below 2 FAIL0.606
cubic_with_square_nonlinear.c below 1 FAIL0.392
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.454
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.397
cubic_with_square_unsafe.c below 1 OKAY0.468
multi-input.c below 1 FAIL0.493
multi-input_unsafe.c below 1 OKAY0.498
nondet_loop_bound.c below 1 FAIL0.365
nondet_loop_bound_quartic.c below 1 FAIL0.392
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.389
nondet_loop_bound_unsafe.c below 1 OKAY0.368
nonlinear_stratified.c below 1 TIMEOUT300.005
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.003
quartic_with_cube.c below 1 FAIL0.652
quartic_with_cube_nonlinear.c below 1 FAIL0.419
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.428
quartic_with_cube_unsafe.c below 1 OKAY0.52
quintic_with_quartic.c below 1 PASS1.135
quintic_with_quartic_nonlinear.c below 1 TIMEOUT300.005
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.564
quintic_with_quartic_unsafe.c below 1 OKAY1.131
ICRA Assertions (True) = 1/12
ICRA Assertions (False) = 9/10
ICRA Time = 910.161
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.745
degree2_FD_AllAux_AllAssm.c below 1 PASS117.285
degree2_FD_AllAux_FewAssm.c below 1 PASS7.289
degree2_FD_FewAux_FewAssm.c below 1 PASS1.088
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.104
degree3.c below 1 PASS0.801
degree3_FD.c below 1 PASS1.013
degree4.c below 1 PASS0.472
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 129.797
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.46
loop_unsafe.c below 1 OKAY0.463
simulated_lese_parser.c below 1 PASS0.366
simulated_lese_sentinel.c below 1 PASS0.371
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.66
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.366
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.366
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.007
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.007
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.374
array_false-unreach-call2.c below 1 OKAY0.386
array_false-unreach-call3.c below 1 OKAY0.373
array_true-unreach-call1.c below 1 FAIL0.366
array_true-unreach-call2.c below 1 FAIL0.386
array_true-unreach-call3.c below 1 PASS0.369
array_true-unreach-call4.c below 1 FAIL0.36
const_false-unreach-call1.c below 1 OKAY0.353
const_true-unreach-call1.c below 1 PASS0.355
diamond_false-unreach-call1.c below 1 OKAY0.358
diamond_true-unreach-call1.c below 1 PASS0.369
diamond_true-unreach-call2.c below 1 PASS0.383
functions_false-unreach-call1.c below 3 OKAY0.396
functions_true-unreach-call1.c below 3 PASS0.402
multivar_false-unreach-call1.c below 1 OKAY0.363
multivar_true-unreach-call1.c below 1 PASS0.362
nested_false-unreach-call1.c below 1 OKAY0.391
nested_true-unreach-call1.c below 1 PASS0.373
overflow_true-unreach-call1.c below 1 PASS0.332
phases_false-unreach-call1.c below 1 OKAY0.434
phases_false-unreach-call2.c below 1 OKAY0.358
phases_true-unreach-call1.c below 1 PASS0.414
phases_true-unreach-call2.c below 1 PASS0.357
simple_false-unreach-call1.c below 1 OKAY0.347
simple_false-unreach-call2.c below 1 OKAY0.337
simple_false-unreach-call3.c below 1 OKAY0.337
simple_false-unreach-call4.c below 1 OKAY0.348
simple_true-unreach-call1.c below 1 PASS0.333
simple_true-unreach-call2.c below 1 PASS0.334
simple_true-unreach-call3.c below 1 PASS0.352
simple_true-unreach-call4.c below 1 PASS0.34
underapprox_false-unreach-call1.c below 1 OKAY0.367
underapprox_false-unreach-call2.c below 1 OKAY0.357
underapprox_true-unreach-call1.c below 1 FAIL0.359
underapprox_true-unreach-call2.c below 1 PASS0.372
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.797
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.939
apache-get-tag_true-unreach-call.c below 1 FAIL0.451
down_true-unreach-call.c below 1 PASS0.386
fragtest_simple_true-unreach-call.c below 1 PASS0.466
half_2_true-unreach-call.c below 1 PASS0.411
heapsort_true-unreach-call.c below 1 PASS127.899
id_build_true-unreach-call.c below 1 PASS0.383
id_trans_false-unreach-call.c below 1 OKAY0.347
id_trans_true-unreach-call.c below 1 PASS0.357
large_const_true-unreach-call.c below 1 PASS0.447
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.394
nested6_true-unreach-call.c below 1 FAIL0.507
nested9_true-unreach-call.c below 1 PASS0.568
nest-if3_true-unreach-call.c below 1 PASS0.471
NetBSD_loop_true-unreach-call.c below 1 PASS0.356
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.408
seq_true-unreach-call.c below 1 PASS0.436
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.251
string_concat-noarr_true-unreach-call.c below 1 PASS0.408
up_true-unreach-call.c below 1 PASS0.394
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 137.279
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.38
bhmr2007_true-unreach-call.c below 1 PASS0.409
cggmp2005b_true-unreach-call.c below 1 PASS0.521
cggmp2005_true-unreach-call.c below 1 PASS0.371
cggmp2005_variant_true-unreach-call.c below 1 PASS0.366
css2003_true-unreach-call.c below 1 PASS0.837
ddlm2013_true-unreach-call.c below 1 PASS0.52
gcnr2008_false-unreach-call.c below 1 OKAY1.026
gj2007b_true-unreach-call.c below 1 FAIL0.389
gj2007_true-unreach-call.c below 1 PASS0.447
gr2006_true-unreach-call.c below 1 PASS0.444
gsv2008_true-unreach-call.c below 1 PASS0.364
hhk2008_true-unreach-call.c below 1 PASS0.351
jm2006_true-unreach-call.c below 1 PASS0.417
jm2006_variant_true-unreach-call.c below 1 PASS0.491
mcmillan2006_true-unreach-call.c below 1 FAIL0.402
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.735
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.336
count_by_1_variant_true-unreach-call.c below 1 PASS0.387
count_by_2_true-unreach-call.c below 1 PASS0.332
count_by_k_true-unreach-call.c below 1 PASS0.34
count_by_nondet_true-unreach-call.c below 1 PASS0.354
gauss_sum_true-unreach-call.c below 1 PASS0.384
half_true-unreach-call.c below 1 FAIL0.378
nested_true-unreach-call.c below 1 PASS0.437
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.948
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.404
array_true-unreach-call.c below 1 FAIL0.405
bubble_sort_false-unreach-call.c below 4 OKAY77.18
bubble_sort_true-unreach-call.c below 1 PASS4.65
compact_false-unreach-call.c below 1 OKAY0.415
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.366
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.356
eureka_01_false-unreach-call.c below 1 OKAY2.37
eureka_01_true-unreach-call.c below 1 FAIL1.512
eureka_05_true-unreach-call.c below 1 FAIL0.747
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.346
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.351
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.33
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.33
heavy_false-unreach-call.c below 1 OKAY0.51
heavy_true-unreach-call.c below 1 PASS0.484
insertion_sort_false-unreach-call.c below 1 OKAY1.512
insertion_sort_true-unreach-call.c below 1 FAIL0.603
invert_string_false-unreach-call.c below 1 OKAY0.502
invert_string_true-unreach-call.c below 1 FAIL0.53
linear_sea.ch_true-unreach-call.c below 1 FAIL0.402
linear_search_false-unreach-call.c below 1 OKAY0.403
lu.cmp_true-unreach-call.c below 3 PASS27.696
ludcmp_false-unreach-call.c below 3 OKAY27.659
matrix_false-unreach-call_true-termination.c below 1 OKAY1.233
matrix_true-unreach-call_true-termination.c below 1 FAIL0.462
n.c11_true-unreach-call.c below 3 FAIL0.47
n.c24_false-unreach-call.c below 3 OKAY6.635
n.c40_true-unreach-call.c below 1 FAIL0.384
nec11_false-unreach-call.c below 1 OKAY0.378
nec20_false-unreach-call.c below 1 OKAY0.399
nec40_true-unreach-call.c below 1 FAIL0.378
string_false-unreach-call.c below 1 OKAY0.615
string_true-unreach-call.c below 1 FAIL0.616
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.576
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.354
sum01_false-unreach-call_true-termination.c below 1 OKAY0.48
sum01_true-unreach-call_true-termination.c below 1 PASS0.367
sum03_false-unreach-call_true-termination.c below 1 OKAY0.52
sum03_true-unreach-call_false-termination.c below 1 PASS0.442
sum04_false-unreach-call_true-termination.c below 1 OKAY0.475
sum04_true-unreach-call_true-termination.c below 1 PASS0.366
sum_array_false-unreach-call.c below 1 OKAY0.556
sum_array_true-unreach-call.c below 1 FAIL0.589
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.345
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.467
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.379
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.346
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.357
trex01_false-unreach-call_true-termination.c below 3 OKAY0.463
trex01_true-unreach-call.c below 3 PASS0.807
trex02_false-unreach-call_true-termination.c below 3 OKAY0.415
trex02_true-unreach-call_true-termination.c below 3 PASS0.413
trex03_false-unreach-call_true-termination.c below 3 OKAY0.706
trex03_true-unreach-call.c below 3 PASS0.701
trex04_true-unreach-call_false-termination.c below 1 PASS0.412
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.369
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS8.022
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.392
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.373
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY7.802
vogal_false-unreach-call.c below 1 OKAY0.768
vogal_true-unreach-call.c below 1 FAIL0.746
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.316
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.318
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.321
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.326
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 191.922
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.3
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.217
Ackermann03_true-unreach-call.c below 7 FAIL1.303
Ackermann04_true-unreach-call.c below 7 FAIL1.284
Addition01_true-unreach-call_true-termination.c below 2 PASS0.608
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.612
Addition03_false-no-overflow.c below 2 PASS0.598
Addition03_true-unreach-call.c below 2 PASS0.604
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.515
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.421
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.442
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.006
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.614
gcd02_true-unreach-call.c below 2 FAIL1.151
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.984
McCarthy91_true-unreach-call.c below 7 FAIL0.975
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.596
Primes_true-unreach-call.c below 3 FAIL1.722
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL2.983
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.409
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.409
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1518.774
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.47
afterrec_2calls_true-unreach-call.c below 2 PASS0.415
afterrec_false-unreach-call.c below 2 OKAY0.396
afterrec_true-unreach-call.c below 2 PASS0.382
fibo_10_false-unreach-call.c below TIMEOUT 300.007
fibo_10_true-unreach-call.c below TIMEOUT 300.004
fibo_15_false-unreach-call.c below TIMEOUT 300.007
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.007
fibo_25_false-unreach-call.c below TIMEOUT 300.006
fibo_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.004
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.007
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.007
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.017
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.007
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.018
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.007
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.014
fibo_5_false-unreach-call.c below TIMEOUT 300.006
fibo_5_true-unreach-call.c below TIMEOUT 300.005
fibo_7_false-unreach-call.c below TIMEOUT 300.006
fibo_7_true-unreach-call.c below TIMEOUT 300.006
id2_b2_o3_true-unreach-call.c below 2 PASS0.725
id2_b3_o2_false-unreach-call.c below 2 OKAY0.751
id2_b3_o5_true-unreach-call.c below 2 PASS0.744
id2_b5_o10_true-unreach-call.c below 2 PASS0.741
id2_i5_o5_false-unreach-call.c below 2 OKAY0.458
id2_i5_o5_true-unreach-call.c below 2 PASS0.445
id_b2_o3_true-unreach-call.c below 2 PASS0.613
id_b3_o2_false-unreach-call.c below 2 OKAY0.619
id_b3_o5_true-unreach-call.c below 2 PASS0.621
id_b5_o10_true-unreach-call.c below 2 PASS0.621
id_i10_o10_false-unreach-call.c below 2 OKAY0.393
id_i10_o10_true-unreach-call.c below 2 PASS0.398
id_i15_o15_false-unreach-call.c below 2 OKAY0.407
id_i15_o15_true-unreach-call.c below 2 PASS0.392
id_i20_o20_false-unreach-call.c below 2 OKAY0.413
id_i20_o20_true-unreach-call.c below 2 PASS0.417
id_i25_o25_false-unreach-call.c below 2 OKAY0.405
id_i25_o25_true-unreach-call.c below 2 PASS0.408
id_i5_o5_false-unreach-call.c below 2 OKAY0.403
id_i5_o5_true-unreach-call.c below 2 PASS0.416
id_o1000_false-unreach-call.c below 2 OKAY0.403
id_o100_false-unreach-call.c below 2 OKAY0.417
id_o10_false-unreach-call.c below 2 OKAY0.416
id_o200_false-unreach-call.c below 2 OKAY0.416
id_o20_false-unreach-call.c below 2 OKAY0.397
id_o3_false-unreach-call.c below 2 OKAY0.411
sum_10x0_false-unreach-call.c below 2 OKAY0.447
sum_10x0_true-unreach-call.c below 2 PASS0.435
sum_15x0_false-unreach-call.c below 2 OKAY0.448
sum_15x0_true-unreach-call.c below 2 PASS0.437
sum_20x0_false-unreach-call.c below 2 OKAY0.454
sum_20x0_true-unreach-call.c below 2 PASS0.437
sum_25x0_false-unreach-call.c below 2 OKAY0.443
sum_25x0_true-unreach-call.c below 2 PASS0.448
sum_2x3_false-unreach-call.c below 2 OKAY0.443
sum_2x3_true-unreach-call.c below 2 PASS0.435
sum_non_eq_false-unreach-call.c below 2 OKAY0.449
sum_non_eq_true-unreach-call.c below 2 PASS0.447
sum_non_false-unreach-call.c below 2 OKAY0.449
sum_non_true-unreach-call.c below 2 PASS0.443
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9020.994
/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.454
rec-bhmr2007_true-unreach-call.c below 2 PASS0.439
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.68
rec-cggmp2005_true-unreach-call.c below 2 PASS0.399
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.426
rec-css2003_true-unreach-call.c below 2 PASS1.051
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.893
rec-gj2007b_true-unreach-call.c below 2 FAIL0.413
rec-gj2007_true-unreach-call.c below 2 FAIL0.482
rec-gr2006_true-unreach-call.c below 2 FAIL0.493
rec-gsv2008_true-unreach-call.c below 2 PASS0.425
rec-hhk2008_true-unreach-call.c below 2 PASS0.404
rec-jm2006_true-unreach-call.c below 2 PASS0.476
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.529
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.454
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 308.022
/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.373
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.42
rec-count_by_2_true-unreach-call.c below 2 PASS0.372
rec-count_by_k_true-unreach-call.c below 2 PASS0.41
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.413
rec-gauss_sum_true-unreach-call.c below 2 PASS0.449
rec-half_true-unreach-call.c below 2 FAIL0.426
rec-nested_true-unreach-call.c below 3 FAIL0.586
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.449
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.568
cubic_polynomial_unsafe.c below 2 OKAY0.566
edit_distance_bottom_up.c below 3 FAIL199.349
edit_distance_top_down.c below 3 FAIL4.634
log_log_n_solution.c below 3 FAIL0.463
log_log_n_solution_unsafe.c below 3 OKAY0.473
log_n_solution.c below 2 FAIL0.482
log_n_solution_unsafe.c below 2 OKAY0.477
multivariate_1.c below TIMEOUT 300.007
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL2.794
multivariate_higher_order_unsafe.c below 7 OKAY2.855
n_cubed_solution.c below EXCEPTION 81.547
n_cubed_solution_unsafe.c below EXCEPTION 0.029
n_log_n_solution.c below 8 FAIL1.242
n_log_n_solution_unsafe.c below 8 OKAY1.272
n_squared_two_base_case_even.c below 2 PASS0.6
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.611
n_squared_two_base_case_odd.c below 2 PASS0.6
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.601
pascals_dynamic.c below 3 FAIL2.529
pascals_dynamic_unsafe.c below 3 OKAY2.477
pascals_iterative.c below 1 FAIL4.788
pascals_iterative_unsafe.c below 1 OKAY4.836
pascals_recursive.c below 9 FAIL3.992
pascals_recursive_unsafe.c below 9 OKAY4.219
squared_solution.c below 8 FAIL3.278
squared_solution_unsafe.c below 8 OKAY2.94
two_n_even.c below 2 PASS0.433
two_n_even_unsafe.c below 2 OKAY0.435
two_n_odd.c below 2 PASS0.426
two_n_odd_unsafe.c below 2 OKAY0.437
two_to_n_over_two_even.c below 7 FAIL1.193
two_to_n_over_two_even_unsafe.c below 7 OKAY1.19
two_to_n_over_two_odd.c below 7 FAIL1.195
two_to_n_over_two_odd_unsafe.c below 7 OKAY1.175
two_to_n_squared.c below 5 FAIL18.97
two_to_n_squared_unsafe.c below 5 OKAY19.26
two_to_two_to_n.c below 7 FAIL1.127
two_to_two_to_n_unsafe.c below 7 OKAY1.168
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 17/19
ICRA Time = 975.243
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.379
adding_and_mult_unsafe.c below 1 OKAY0.383
binary_search_array_tree.c below 1 FAIL0.65
exp_add_linear.c below 1 PASS0.441
exp_add_linear_unsafe.c below 1 OKAY0.448
exp_add_loop_rec.c below 1 FAIL0.378
exp_add_loop_rec_unsafe.c below 1 OKAY0.369
exp_add_loop_variable.c below 1 PASS0.425
exp_add_loop_variable_unsafe.c below 1 OKAY0.439
exp_with_linear_inner_loop.c below 1 FAIL0.5
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.503
halving_log1.c below 1 FAIL0.513
linear_two_to_n.c below 7 FAIL22.309
linear_two_to_n_unsafe.c below 7 OKAY22.33
loop_five_to_n.c below 1 PASS0.398
loop_five_to_n_unsafe.c below 1 OKAY0.402
non_loop_five_to_n.c below 7 FAIL53.983
non_loop_five_to_n_unsafe.c below 7 OKAY54.049
power_log.c below 1 PASS0.507
power_log_modified.c below 1 PASS0.526
simple_exponential.c below 1 PASS0.407
simple_exponential_for.c below 1 PASS0.402
simple_exponential_for_unsafe.c below 1 OKAY0.406
simple_exponential_unsafe.c below 1 OKAY0.404
two_to_n_minus_n.c below 7 FAIL2.913
two_to_n_minus_n_loop.c below TIMEOUT 300.028
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.029
two_to_n_minus_n_unsafe.c below 7 OKAY2.889
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 767.41
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.568
02.c below 3 FAIL0.745
03.c below 1 PASS0.431
04.c below 1 PASS0.364
05.c below 3 PASS1.07
06.c below 3 FAIL7.528
07.c below 3 PASS0.554
08.c below 3 PASS1.27
09.c below 3 PASS0.694
10.c below 3 FAIL0.914
11.c below 1 PASS0.358
12.c below 3 PASS1.283
13.c below 3 PASS0.513
14.c below 3 PASS0.449
15.c below 1 PASS0.355
16.c below 1 PASS0.444
17.c below 1 PASS0.433
18.c below 1 PASS0.429
19.c below 1 PASS0.452
20.c below 3 FAIL0.615
21.c below 3 PASS0.516
22.c below 3 FAIL0.724
23.c below 1 PASS0.381
24.c below 1 PASS0.406
25.c below 3 FAIL1.341
26.c below TIMEOUT 300.005
27.c below 1 PASS0.447
28.c below 3 PASS0.497
29.c below 3 PASS0.904
30.c below 1 PASS0.38
31.c below 3 PASS0.867
32.c below 1 FAIL0.394
33.c below 3 PASS1.164
34.c below 1 FAIL0.395
35.c below 1 PASS0.343
36.c below 3 PASS2.588
37.c below 3 FAIL0.479
38.c below 1 FAIL0.397
39.c below 3 PASS0.435
40.c below 3 PASS0.679
41.c below 1 PASS0.397
42.c below 3 PASS0.801
43.c below 3 PASS0.465
44.c below 1 PASS0.382
45.c below 3 FAIL2.404
46.c below 3 FAIL1.467
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 338.727
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.412
AGHKTW2017_foo.c below 1 PASS0.406
AGHKTW2017_loginSafe.c below 1 PASS0.863
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.465
BCK2011_gauss.c below 1 PASS0.442
BCK2011_strength_reduction.c below 1 PASS0.417
BCK2011_strength_reduction_linear.c below 1 PASS0.452
fibonacci_information_flow.c below 1 PASS0.621
TA2005_fib2.c below 1 PASS0.567
TA2005_fib.c below 1 PASS0.481
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 5.126