[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.401
kmp.c below 1 PASS1.184
qsort.c below 4 PASS0.988
speed_pldi09_fig1.c below 1 PASS0.544
speed_pldi09_fig4_2.c below 1 FAIL0.426
speed_pldi09_fig4_4.c below 1 PASS0.554
speed_pldi09_fig4_5.c below 1 PASS0.443
speed_pldi10_ex1.c below 1 PASS1.393
speed_pldi10_ex3.c below 1 PASS0.547
speed_pldi10_ex4.c below 1 PASS0.582
speed_popl10_fig2_1.c below 1 PASS0.494
speed_popl10_fig2_2.c below 1 FAIL0.408
speed_popl10_nested_multiple.c below 1 PASS0.498
speed_popl10_nested_single.c below 1 PASS0.461
speed_popl10_sequential_single.c below 1 PASS0.43
speed_popl10_simple_multiple.c below 1 PASS0.555
speed_popl10_simple_single_2.c below 1 PASS0.716
speed_popl10_simple_single.c below 1 PASS0.379
t07.c below 1 PASS0.449
t08.c below 1 PASS0.42
t09.c below 1 PASS0.419
t10.c below 1 PASS0.395
t11.c below 1 PASS0.51
t13.c below 1 FAIL0.456
t15.c below 1 PASS0.453
t16.c below 1 PASS0.429
t19.c below 1 PASS0.426
t20.c below 1 PASS0.412
t27.c below 1 PASS0.589
t28.c below 1 PASS0.519
t30.c below 1 FAIL0.437
t37.c below 2 PASS0.667
t39.c below 2 PASS0.591
t46.c below 1 PASS0.446
t47.c below 1 PASS0.56
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 19.181
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.409
qsort_full.c below 4 PASS10.772
rec1-param_safe.c below 2 PASS0.401
rec1-param_unsafe.c below 2 OKAY0.4
rec1_safe.c below 2 PASS0.39
rec1_unsafe.c below 2 OKAY0.379
rec2-param_safe.c below 2 PASS0.393
rec2-param_unsafe.c below 2 OKAY0.382
rec2_safe.c below 2 PASS0.382
rec2_unsafe.c below 2 OKAY0.395
rec-test.c below 2 PASS0.376
sas03_bothbranches.c below 7 PASS0.862
sas03.c below 2 PASS0.783
simulated_lese_recursive.c below 2 PASS0.483
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 16.807
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.366
count_up_down_unsafe.c below 1 OKAY0.362
divide.c below 1 PASS0.354
factor_unsafe.c below 1 OKAY0.359
for_infinite_loop_1_safe.c below 1 PASS0.336
for_infinite_loop_2_safe.c below 1 PASS0.341
interproc.c below 1 PASS0.342
mult.c below 1 PASS0.347
pointer_arith.c below 1 PASS0.337
quotient.c below 3 PASS0.514
subtract.c below 1 PASS0.345
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.362
sum01_bug02_unsafe.c below 1 OKAY0.605
sum01_real_safe.c below 1 PASS0.342
sum01_safe.c below 1 PASS0.358
sum01_unsafe.c below 1 OKAY0.473
sum02_safe.c below 1 PASS0.39
sum03_safe.c below 1 PASS0.419
sum03_unsafe.c below 1 OKAY0.484
sum04_safe.c below 1 PASS0.374
sum04_unsafe.c below 1 OKAY0.496
terminator_02_safe.c below 1 PASS0.341
terminator_02_unsafe.c below 1 OKAY0.417
terminator_03_safe.c below 1 PASS0.357
terminator_03_unsafe.c below 1 OKAY0.357
token_ring01_safe.c below 4 FAIL163.729
token_ring01_unsafe.c below 4 OKAY261.689
toy_safe.c below EXCEPTION 214.246
trex01_safe.c below 1 PASS0.765
trex01_unsafe.c below 1 OKAY0.398
trex02_safe2.c below 3 PASS0.446
trex02_safe.c below 3 PASS0.432
trex02_unsafe.c below 3 OKAY0.446
trex03_safe.c below 1 PASS0.492
trex03_unsafe.c below 1 OKAY0.474
trex04_safe.c below 1 PASS0.384
while_infinite_loop_1_safe.c below 1 PASS0.34
while_infinite_loop_2_safe.c below 1 PASS0.348
while_infinite_loop_3_safe.c below 1 PASS0.344
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 654.311
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.441
blogger_simplified1.c below 3 PASS1.189
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.392
mult-proc-params.c below 3 PASS0.418
popall.c below 1 PASS0.726
simulated_scc.c below 1 PASS0.705
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.876
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.366
degree2_binomial.c below 1 PASS0.731
degree2_monomial.c below 1 PASS0.422
degree3_binomial.c below 1 FAIL2.371
degree3_monomial.c below 1 PASS0.48
degree4_binomial.c below 1 FAIL7.872
degree4_monomial.c below 1 PASS0.564
degree5_binomial.c below 1 TIMEOUT300.021
degree5_monomial.c below 1 PASS0.652
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 313.479
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.488
cubic_with_square_interproc.c below 2 FAIL0.617
cubic_with_square_nonlinear.c below 1 FAIL0.39
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.456
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.41
cubic_with_square_unsafe.c below 1 OKAY0.471
multi-input.c below 1 FAIL0.494
multi-input_unsafe.c below 1 OKAY0.502
nondet_loop_bound.c below 1 FAIL0.39
nondet_loop_bound_quartic.c below 1 FAIL0.399
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.4
nondet_loop_bound_unsafe.c below 1 OKAY0.371
nonlinear_stratified.c below 1 TIMEOUT300.005
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.005
quartic_with_cube.c below 1 FAIL0.652
quartic_with_cube_nonlinear.c below 1 FAIL0.418
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.422
quartic_with_cube_unsafe.c below 1 OKAY0.515
quintic_with_quartic.c below 1 PASS1.152
quintic_with_quartic_nonlinear.c below 1 TIMEOUT300.004
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.577
quintic_with_quartic_unsafe.c below 1 OKAY1.127
ICRA Assertions (True) = 1/12
ICRA Assertions (False) = 9/10
ICRA Time = 910.265
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.75
degree2_FD_AllAux_AllAssm.c below 1 PASS117.694
degree2_FD_AllAux_FewAssm.c below 1 PASS7.443
degree2_FD_FewAux_FewAssm.c below 1 PASS1.102
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.14
degree3.c below 1 PASS0.837
degree3_FD.c below 1 PASS1.007
degree4.c below 1 PASS0.469
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 130.442
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.443
loop_unsafe.c below 1 OKAY0.46
simulated_lese_parser.c below 1 PASS0.363
simulated_lese_sentinel.c below 1 PASS0.369
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.635
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.369
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.369
/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.354
array_false-unreach-call2.c below 1 OKAY0.375
array_false-unreach-call3.c below 1 OKAY0.356
array_true-unreach-call1.c below 1 FAIL0.358
array_true-unreach-call2.c below 1 FAIL0.386
array_true-unreach-call3.c below 1 PASS0.348
array_true-unreach-call4.c below 1 FAIL0.343
const_false-unreach-call1.c below 1 OKAY0.359
const_true-unreach-call1.c below 1 PASS0.364
diamond_false-unreach-call1.c below 1 OKAY0.362
diamond_true-unreach-call1.c below 1 PASS0.369
diamond_true-unreach-call2.c below 1 PASS0.395
functions_false-unreach-call1.c below 3 OKAY0.399
functions_true-unreach-call1.c below 3 PASS0.442
multivar_false-unreach-call1.c below 1 OKAY0.355
multivar_true-unreach-call1.c below 1 PASS0.381
nested_false-unreach-call1.c below 1 OKAY0.385
nested_true-unreach-call1.c below 1 PASS0.386
overflow_true-unreach-call1.c below 1 PASS0.339
phases_false-unreach-call1.c below 1 OKAY0.422
phases_false-unreach-call2.c below 1 OKAY0.371
phases_true-unreach-call1.c below 1 PASS0.417
phases_true-unreach-call2.c below 1 PASS0.369
simple_false-unreach-call1.c below 1 OKAY0.349
simple_false-unreach-call2.c below 1 OKAY0.343
simple_false-unreach-call3.c below 1 OKAY0.339
simple_false-unreach-call4.c below 1 OKAY0.342
simple_true-unreach-call1.c below 1 PASS0.347
simple_true-unreach-call2.c below 1 PASS0.331
simple_true-unreach-call3.c below 1 PASS0.347
simple_true-unreach-call4.c below 1 PASS0.37
underapprox_false-unreach-call1.c below 1 OKAY0.37
underapprox_false-unreach-call2.c below 1 OKAY0.371
underapprox_true-unreach-call1.c below 1 FAIL0.363
underapprox_true-unreach-call2.c below 1 PASS0.376
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.883
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.951
apache-get-tag_true-unreach-call.c below 1 FAIL0.469
down_true-unreach-call.c below 1 PASS0.391
fragtest_simple_true-unreach-call.c below 1 PASS0.482
half_2_true-unreach-call.c below 1 PASS0.409
heapsort_true-unreach-call.c below 1 PASS127.808
id_build_true-unreach-call.c below 1 PASS0.396
id_trans_false-unreach-call.c below 1 OKAY0.353
id_trans_true-unreach-call.c below 1 PASS0.358
large_const_true-unreach-call.c below 1 PASS0.434
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.401
nested6_true-unreach-call.c below 1 FAIL0.505
nested9_true-unreach-call.c below 1 PASS0.569
nest-if3_true-unreach-call.c below 1 PASS0.494
NetBSD_loop_true-unreach-call.c below 1 PASS0.369
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.416
seq_true-unreach-call.c below 1 PASS0.448
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.279
string_concat-noarr_true-unreach-call.c below 1 PASS0.43
up_true-unreach-call.c below 1 PASS0.393
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 137.355
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.395
bhmr2007_true-unreach-call.c below 1 PASS0.412
cggmp2005b_true-unreach-call.c below 1 PASS0.55
cggmp2005_true-unreach-call.c below 1 PASS0.372
cggmp2005_variant_true-unreach-call.c below 1 PASS0.37
css2003_true-unreach-call.c below 1 PASS0.848
ddlm2013_true-unreach-call.c below 1 PASS0.513
gcnr2008_false-unreach-call.c below 1 OKAY1.026
gj2007b_true-unreach-call.c below 1 FAIL0.407
gj2007_true-unreach-call.c below 1 PASS0.456
gr2006_true-unreach-call.c below 1 PASS0.453
gsv2008_true-unreach-call.c below 1 PASS0.373
hhk2008_true-unreach-call.c below 1 PASS0.367
jm2006_true-unreach-call.c below 1 PASS0.445
jm2006_variant_true-unreach-call.c below 1 PASS0.51
mcmillan2006_true-unreach-call.c below 1 FAIL0.397
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.894
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.353
count_by_1_variant_true-unreach-call.c below 1 PASS0.409
count_by_2_true-unreach-call.c below 1 PASS0.345
count_by_k_true-unreach-call.c below 1 PASS0.354
count_by_nondet_true-unreach-call.c below 1 PASS0.363
gauss_sum_true-unreach-call.c below 1 PASS0.395
half_true-unreach-call.c below 1 FAIL0.38
nested_true-unreach-call.c below 1 PASS0.444
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.043
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.412
array_true-unreach-call.c below 1 FAIL0.396
bubble_sort_false-unreach-call.c below 4 OKAY80.475
bubble_sort_true-unreach-call.c below 1 PASS4.951
compact_false-unreach-call.c below 1 OKAY0.407
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.361
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.369
eureka_01_false-unreach-call.c below 1 OKAY2.461
eureka_01_true-unreach-call.c below 1 FAIL1.576
eureka_05_true-unreach-call.c below 1 FAIL0.79
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.365
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.345
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.367
heavy_false-unreach-call.c below 1 OKAY0.506
heavy_true-unreach-call.c below 1 PASS0.491
insertion_sort_false-unreach-call.c below 1 OKAY1.505
insertion_sort_true-unreach-call.c below 1 FAIL0.598
invert_string_false-unreach-call.c below 1 OKAY0.483
invert_string_true-unreach-call.c below 1 FAIL0.53
linear_sea.ch_true-unreach-call.c below 1 FAIL0.41
linear_search_false-unreach-call.c below 1 OKAY0.409
lu.cmp_true-unreach-call.c below 3 PASS28.63
ludcmp_false-unreach-call.c below 3 OKAY28.815
matrix_false-unreach-call_true-termination.c below 1 OKAY1.253
matrix_true-unreach-call_true-termination.c below 1 FAIL0.474
n.c11_true-unreach-call.c below 3 FAIL0.469
n.c24_false-unreach-call.c below 3 OKAY6.637
n.c40_true-unreach-call.c below 1 FAIL0.375
nec11_false-unreach-call.c below 1 OKAY0.374
nec20_false-unreach-call.c below 1 OKAY0.421
nec40_true-unreach-call.c below 1 FAIL0.384
string_false-unreach-call.c below 1 OKAY0.61
string_true-unreach-call.c below 1 FAIL0.612
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.588
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.366
sum01_false-unreach-call_true-termination.c below 1 OKAY0.479
sum01_true-unreach-call_true-termination.c below 1 PASS0.367
sum03_false-unreach-call_true-termination.c below 1 OKAY0.515
sum03_true-unreach-call_false-termination.c below 1 PASS0.449
sum04_false-unreach-call_true-termination.c below 1 OKAY0.484
sum04_true-unreach-call_true-termination.c below 1 PASS0.373
sum_array_false-unreach-call.c below 1 OKAY0.561
sum_array_true-unreach-call.c below 1 FAIL0.599
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.327
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.468
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.375
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.359
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.358
trex01_false-unreach-call_true-termination.c below 3 OKAY0.475
trex01_true-unreach-call.c below 3 PASS0.812
trex02_false-unreach-call_true-termination.c below 3 OKAY0.411
trex02_true-unreach-call_true-termination.c below 3 PASS0.421
trex03_false-unreach-call_true-termination.c below 3 OKAY0.725
trex03_true-unreach-call.c below 3 PASS0.702
trex04_true-unreach-call_false-termination.c below 1 PASS0.401
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.371
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS8.307
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.38
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.376
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY8.048
vogal_false-unreach-call.c below 1 OKAY0.809
vogal_true-unreach-call.c below 1 FAIL0.755
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.325
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.328
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.333
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.333
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 198.592
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.35
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.261
Ackermann03_true-unreach-call.c below 7 FAIL1.311
Ackermann04_true-unreach-call.c below 7 FAIL1.317
Addition01_true-unreach-call_true-termination.c below 2 PASS0.598
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.621
Addition03_false-no-overflow.c below 2 PASS0.621
Addition03_true-unreach-call.c below 2 PASS0.615
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.537
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.452
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.444
Fibonacci01_true-unreach-call.c below TIMEOUT 300.007
Fibonacci02_true-unreach-call_true-termination.c below TIMEOUT 300.005
Fibonacci03_true-unreach-call_true-termination.c below TIMEOUT 300.007
Fibonacci04_false-unreach-call_true-termination.c below TIMEOUT 300.006
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.007
gcd01_true-unreach-call_true-termination.c below 2 PASS0.625
gcd02_true-unreach-call.c below 2 FAIL1.14
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY1.023
McCarthy91_true-unreach-call.c below 7 FAIL1.004
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.607
Primes_true-unreach-call.c below 3 FAIL1.734
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL2.989
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.416
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.419
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1519.116
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.465
afterrec_2calls_true-unreach-call.c below 2 PASS0.435
afterrec_false-unreach-call.c below 2 OKAY0.396
afterrec_true-unreach-call.c below 2 PASS0.393
fibo_10_false-unreach-call.c below TIMEOUT 300.004
fibo_10_true-unreach-call.c below TIMEOUT 300.009
fibo_15_false-unreach-call.c below TIMEOUT 300.008
fibo_15_true-unreach-call.c below TIMEOUT 300.007
fibo_20_false-unreach-call.c below TIMEOUT 300.005
fibo_20_true-unreach-call.c below TIMEOUT 300.006
fibo_25_false-unreach-call.c below TIMEOUT 300.006
fibo_25_true-unreach-call.c below TIMEOUT 300.008
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.006
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.005
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.005
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.019
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.019
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.005
fibo_5_false-unreach-call.c below TIMEOUT 300.006
fibo_5_true-unreach-call.c below TIMEOUT 300.006
fibo_7_false-unreach-call.c below TIMEOUT 300.006
fibo_7_true-unreach-call.c below TIMEOUT 300.007
id2_b2_o3_true-unreach-call.c below 2 PASS0.748
id2_b3_o2_false-unreach-call.c below 2 OKAY0.764
id2_b3_o5_true-unreach-call.c below 2 PASS0.771
id2_b5_o10_true-unreach-call.c below 2 PASS0.78
id2_i5_o5_false-unreach-call.c below 2 OKAY0.467
id2_i5_o5_true-unreach-call.c below 2 PASS0.45
id_b2_o3_true-unreach-call.c below 2 PASS0.641
id_b3_o2_false-unreach-call.c below 2 OKAY0.646
id_b3_o5_true-unreach-call.c below 2 PASS0.648
id_b5_o10_true-unreach-call.c below 2 PASS0.63
id_i10_o10_false-unreach-call.c below 2 OKAY0.403
id_i10_o10_true-unreach-call.c below 2 PASS0.415
id_i15_o15_false-unreach-call.c below 2 OKAY0.415
id_i15_o15_true-unreach-call.c below 2 PASS0.415
id_i20_o20_false-unreach-call.c below 2 OKAY0.423
id_i20_o20_true-unreach-call.c below 2 PASS0.437
id_i25_o25_false-unreach-call.c below 2 OKAY0.414
id_i25_o25_true-unreach-call.c below 2 PASS0.41
id_i5_o5_false-unreach-call.c below 2 OKAY0.404
id_i5_o5_true-unreach-call.c below 2 PASS0.414
id_o1000_false-unreach-call.c below 2 OKAY0.417
id_o100_false-unreach-call.c below 2 OKAY0.422
id_o10_false-unreach-call.c below 2 OKAY0.433
id_o200_false-unreach-call.c below 2 OKAY0.433
id_o20_false-unreach-call.c below 2 OKAY0.422
id_o3_false-unreach-call.c below 2 OKAY0.419
sum_10x0_false-unreach-call.c below 2 OKAY0.481
sum_10x0_true-unreach-call.c below 2 PASS0.458
sum_15x0_false-unreach-call.c below 2 OKAY0.47
sum_15x0_true-unreach-call.c below 2 PASS0.45
sum_20x0_false-unreach-call.c below 2 OKAY0.473
sum_20x0_true-unreach-call.c below 2 PASS0.445
sum_25x0_false-unreach-call.c below 2 OKAY0.463
sum_25x0_true-unreach-call.c below 2 PASS0.445
sum_2x3_false-unreach-call.c below 2 OKAY0.471
sum_2x3_true-unreach-call.c below 2 PASS0.443
sum_non_eq_false-unreach-call.c below 2 OKAY0.484
sum_non_eq_true-unreach-call.c below 2 PASS0.454
sum_non_false-unreach-call.c below 2 OKAY0.461
sum_non_true-unreach-call.c below 2 PASS0.454
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9021.684
/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.443
rec-bhmr2007_true-unreach-call.c below 2 PASS0.444
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.709
rec-cggmp2005_true-unreach-call.c below 2 PASS0.416
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.446
rec-css2003_true-unreach-call.c below 2 PASS1.065
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.915
rec-gj2007b_true-unreach-call.c below 2 FAIL0.425
rec-gj2007_true-unreach-call.c below 2 FAIL0.485
rec-gr2006_true-unreach-call.c below 2 FAIL0.505
rec-gsv2008_true-unreach-call.c below 2 PASS0.433
rec-hhk2008_true-unreach-call.c below 2 PASS0.422
rec-jm2006_true-unreach-call.c below 2 PASS0.491
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.569
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.453
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 308.225
/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.376
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.427
rec-count_by_2_true-unreach-call.c below 2 PASS0.385
rec-count_by_k_true-unreach-call.c below 2 PASS0.419
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.419
rec-gauss_sum_true-unreach-call.c below 2 PASS0.467
rec-half_true-unreach-call.c below 2 FAIL0.423
rec-nested_true-unreach-call.c below 3 FAIL0.581
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.497
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.581
cubic_polynomial_unsafe.c below 2 OKAY0.584
edit_distance_bottom_up.c below 3 FAIL198.76
edit_distance_top_down.c below 3 FAIL4.92
log_log_n_solution.c below 3 FAIL0.479
log_log_n_solution_unsafe.c below 3 OKAY0.468
log_n_solution.c below 2 FAIL0.497
log_n_solution_unsafe.c below 2 OKAY0.498
multivariate_1.c below TIMEOUT 300.006
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL2.954
multivariate_higher_order_unsafe.c below 7 OKAY2.946
n_cubed_solution.c below EXCEPTION 83.843
n_cubed_solution_unsafe.c below EXCEPTION 0.029
n_log_n_solution.c below 8 FAIL1.298
n_log_n_solution_unsafe.c below 8 OKAY1.292
n_squared_two_base_case_even.c below 2 PASS0.632
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.621
n_squared_two_base_case_odd.c below 2 PASS0.607
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.62
pascals_dynamic.c below 3 FAIL2.564
pascals_dynamic_unsafe.c below 3 OKAY2.62
pascals_iterative.c below 1 FAIL4.945
pascals_iterative_unsafe.c below 1 OKAY4.999
pascals_recursive.c below 9 FAIL4.138
pascals_recursive_unsafe.c below 9 OKAY4.072
squared_solution.c below 8 FAIL3.03
squared_solution_unsafe.c below 8 OKAY3.062
two_n_even.c below 2 PASS0.444
two_n_even_unsafe.c below 2 OKAY0.448
two_n_odd.c below 2 PASS0.431
two_n_odd_unsafe.c below 2 OKAY0.452
two_to_n_over_two_even.c below 7 FAIL1.227
two_to_n_over_two_even_unsafe.c below 7 OKAY1.226
two_to_n_over_two_odd.c below 7 FAIL1.219
two_to_n_over_two_odd_unsafe.c below 7 OKAY1.248
two_to_n_squared.c below 5 FAIL19.489
two_to_n_squared_unsafe.c below 5 OKAY19.443
two_to_two_to_n.c below 7 FAIL1.165
two_to_two_to_n_unsafe.c below 7 OKAY1.151
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 17/19
ICRA Time = 979.014
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.406
adding_and_mult_unsafe.c below 1 OKAY0.391
binary_search_array_tree.c below 1 FAIL0.658
exp_add_linear.c below 1 PASS0.464
exp_add_linear_unsafe.c below 1 OKAY0.477
exp_add_loop_rec.c below 1 FAIL0.383
exp_add_loop_rec_unsafe.c below 1 OKAY0.412
exp_add_loop_variable.c below 1 PASS0.441
exp_add_loop_variable_unsafe.c below 1 OKAY0.433
exp_with_linear_inner_loop.c below 1 FAIL0.523
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.524
halving_log1.c below 1 FAIL0.538
linear_two_to_n.c below 7 FAIL22.384
linear_two_to_n_unsafe.c below 7 OKAY22.46
loop_five_to_n.c below 1 PASS0.414
loop_five_to_n_unsafe.c below 1 OKAY0.423
non_loop_five_to_n.c below 7 FAIL54.051
non_loop_five_to_n_unsafe.c below 7 OKAY53.915
power_log.c below 1 PASS0.506
power_log_modified.c below 1 PASS0.536
simple_exponential.c below 1 PASS0.398
simple_exponential_for.c below 1 PASS0.42
simple_exponential_for_unsafe.c below 1 OKAY0.42
simple_exponential_unsafe.c below 1 OKAY0.401
two_to_n_minus_n.c below 7 FAIL2.982
two_to_n_minus_n_loop.c below TIMEOUT 300.027
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.029
two_to_n_minus_n_unsafe.c below 7 OKAY2.961
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 767.977
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.588
02.c below 3 FAIL0.754
03.c below 1 PASS0.454
04.c below 1 PASS0.383
05.c below 3 PASS1.118
06.c below 3 FAIL7.781
07.c below 3 PASS0.559
08.c below 3 PASS1.27
09.c below 3 PASS0.711
10.c below 3 FAIL0.948
11.c below 1 PASS0.391
12.c below 3 PASS1.287
13.c below 3 PASS0.521
14.c below 3 PASS0.468
15.c below 1 PASS0.361
16.c below 1 PASS0.444
17.c below 1 PASS0.436
18.c below 1 PASS0.413
19.c below 1 PASS0.468
20.c below 3 FAIL0.639
21.c below 3 PASS0.524
22.c below 3 FAIL0.741
23.c below 1 PASS0.386
24.c below 1 PASS0.408
25.c below 3 FAIL1.38
26.c below TIMEOUT 300.007
27.c below 1 PASS0.466
28.c below 3 PASS0.524
29.c below 3 PASS0.911
30.c below 1 PASS0.375
31.c below 3 PASS0.876
32.c below 1 FAIL0.389
33.c below 3 PASS1.211
34.c below 1 FAIL0.421
35.c below 1 PASS0.355
36.c below 3 PASS2.648
37.c below 3 FAIL0.516
38.c below 1 FAIL0.429
39.c below 3 PASS0.431
40.c below 3 PASS0.682
41.c below 1 PASS0.411
42.c below 3 PASS0.825
43.c below 3 PASS0.489
44.c below 1 PASS0.397
45.c below 3 FAIL2.468
46.c below 3 FAIL1.518
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 339.782
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.433
AGHKTW2017_foo.c below 1 PASS0.429
AGHKTW2017_loginSafe.c below 1 PASS0.867
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.49
BCK2011_gauss.c below 1 PASS0.461
BCK2011_strength_reduction.c below 1 PASS0.431
BCK2011_strength_reduction_linear.c below 1 PASS0.461
fibonacci_information_flow.c below 1 PASS0.617
TA2005_fib2.c below 1 PASS0.588
TA2005_fib.c below 1 PASS0.486
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 5.263