[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.373
kmp.c below 1 PASS1.049
qsort.c below 4 PASS0.899
speed_pldi09_fig1.c below 1 PASS0.515
speed_pldi09_fig4_2.c below 1 FAIL0.394
speed_pldi09_fig4_4.c below 1 PASS0.511
speed_pldi09_fig4_5.c below 1 PASS0.387
speed_pldi10_ex1.c below 1 PASS1.201
speed_pldi10_ex3.c below 1 PASS0.522
speed_pldi10_ex4.c below 1 PASS0.523
speed_popl10_fig2_1.c below 1 PASS0.473
speed_popl10_fig2_2.c below 1 FAIL0.382
speed_popl10_nested_multiple.c below 1 PASS0.47
speed_popl10_nested_single.c below 1 PASS0.448
speed_popl10_sequential_single.c below 1 PASS0.397
speed_popl10_simple_multiple.c below 1 PASS0.518
speed_popl10_simple_single_2.c below 1 PASS0.612
speed_popl10_simple_single.c below 1 PASS0.349
t07.c below 1 PASS0.422
t08.c below 1 PASS0.388
t09.c below 1 PASS0.389
t10.c below 1 PASS0.378
t11.c below 1 PASS0.469
t13.c below 1 FAIL0.42
t15.c below 1 PASS0.409
t16.c below 1 PASS0.393
t19.c below 1 PASS0.412
t20.c below 1 PASS0.393
t27.c below 1 PASS0.54
t28.c below 1 PASS0.483
t30.c below 1 FAIL0.408
t37.c below 2 PASS0.607
t39.c below 2 PASS0.547
t46.c below 1 PASS0.408
t47.c below 1 PASS0.516
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 17.605
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.394
qsort_full.c below 4 PASS9.44
rec1-param_safe.c below 2 PASS0.374
rec1-param_unsafe.c below 2 OKAY0.379
rec1_safe.c below 2 PASS0.367
rec1_unsafe.c below 2 OKAY0.369
rec2-param_safe.c below 2 PASS0.359
rec2-param_unsafe.c below 2 OKAY0.362
rec2_safe.c below 2 PASS0.367
rec2_unsafe.c below 2 OKAY0.379
rec-test.c below 2 PASS0.353
sas03_bothbranches.c below 7 PASS0.796
sas03.c below 2 PASS0.687
simulated_lese_recursive.c below 2 PASS0.474
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 15.1
/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.349
divide.c below 1 PASS0.342
factor_unsafe.c below 1 OKAY0.321
for_infinite_loop_1_safe.c below 1 PASS0.326
for_infinite_loop_2_safe.c below 1 PASS0.322
interproc.c below 1 PASS0.305
mult.c below 1 PASS0.33
pointer_arith.c below 1 PASS0.305
quotient.c below 3 PASS0.493
subtract.c below 1 PASS0.335
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.34
sum01_bug02_unsafe.c below 1 OKAY0.536
sum01_real_safe.c below 1 PASS0.334
sum01_safe.c below 1 PASS0.347
sum01_unsafe.c below 1 OKAY0.456
sum02_safe.c below 1 PASS0.359
sum03_safe.c below 1 PASS0.415
sum03_unsafe.c below 1 OKAY0.458
sum04_safe.c below 1 PASS0.338
sum04_unsafe.c below 1 OKAY0.47
terminator_02_safe.c below 1 PASS0.328
terminator_02_unsafe.c below 1 OKAY0.376
terminator_03_safe.c below 1 PASS0.345
terminator_03_unsafe.c below 1 OKAY0.338
token_ring01_safe.c below 4 FAIL141.538
token_ring01_unsafe.c below 4 OKAY238.492
toy_safe.c below EXCEPTION 165.351
trex01_safe.c below 1 PASS0.746
trex01_unsafe.c below 1 OKAY0.375
trex02_safe2.c below 3 PASS0.408
trex02_safe.c below 3 PASS0.407
trex02_unsafe.c below 3 OKAY0.403
trex03_safe.c below 1 PASS0.436
trex03_unsafe.c below 1 OKAY0.431
trex04_safe.c below 1 PASS0.347
while_infinite_loop_1_safe.c below 1 PASS0.315
while_infinite_loop_2_safe.c below 1 PASS0.311
while_infinite_loop_3_safe.c below 1 PASS0.304
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 559.068
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.399
blogger_simplified1.c below 3 PASS1.049
divided_difference2.c below TIMEOUT 300.004
mult-proc.c below 3 PASS0.379
mult-proc-params.c below 3 PASS0.406
popall.c below 1 PASS0.689
simulated_scc.c below 1 PASS0.64
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.566
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.347
degree2_binomial.c below 1 PASS0.68
degree2_monomial.c below 1 PASS0.389
degree3_binomial.c below 1 FAIL2.102
degree3_monomial.c below 1 PASS0.452
degree4_binomial.c below 1 FAIL6.954
degree4_monomial.c below 1 PASS0.532
degree5_binomial.c below 1 TIMEOUT300.019
degree5_monomial.c below 1 PASS0.621
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 312.096
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.441
cubic_with_square_interproc.c below 2 FAIL0.592
cubic_with_square_nonlinear.c below 1 FAIL0.382
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.429
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.382
cubic_with_square_unsafe.c below 1 OKAY0.456
multi-input.c below 1 FAIL0.486
multi-input_unsafe.c below 1 OKAY0.467
nondet_loop_bound.c below 1 FAIL0.348
nondet_loop_bound_quartic.c below 1 FAIL0.383
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.377
nondet_loop_bound_unsafe.c below 1 OKAY0.368
nonlinear_stratified.c below 1 TIMEOUT300.004
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube.c below 1 FAIL0.648
quartic_with_cube_nonlinear.c below 1 FAIL0.404
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.421
quartic_with_cube_unsafe.c below 1 OKAY0.507
quintic_with_quartic.c below 1 PASS1.089
quintic_with_quartic_nonlinear.c below 1 TIMEOUT300.005
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.545
quintic_with_quartic_unsafe.c below 1 OKAY1.047
ICRA Assertions (True) = 1/12
ICRA Assertions (False) = 9/10
ICRA Time = 909.785
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.689
degree2_FD_AllAux_AllAssm.c below 1 PASS101.656
degree2_FD_AllAux_FewAssm.c below 1 PASS6.497
degree2_FD_FewAux_FewAssm.c below 1 PASS1.026
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.039
degree3.c below 1 PASS0.738
degree3_FD.c below 1 PASS0.911
degree4.c below 1 PASS0.464
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 113.02
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.452
loop_unsafe.c below 1 OKAY0.446
simulated_lese_parser.c below 1 PASS0.351
simulated_lese_sentinel.c below 1 PASS0.351
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.6
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.348
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.348
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.005
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.005
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.351
array_false-unreach-call2.c below 1 OKAY0.375
array_false-unreach-call3.c below 1 OKAY0.36
array_true-unreach-call1.c below 1 FAIL0.374
array_true-unreach-call2.c below 1 FAIL0.365
array_true-unreach-call3.c below 1 PASS0.356
array_true-unreach-call4.c below 1 FAIL0.339
const_false-unreach-call1.c below 1 OKAY0.351
const_true-unreach-call1.c below 1 PASS0.342
diamond_false-unreach-call1.c below 1 OKAY0.353
diamond_true-unreach-call1.c below 1 PASS0.336
diamond_true-unreach-call2.c below 1 PASS0.375
functions_false-unreach-call1.c below 3 OKAY0.396
functions_true-unreach-call1.c below 3 PASS0.39
multivar_false-unreach-call1.c below 1 OKAY0.362
multivar_true-unreach-call1.c below 1 PASS0.353
nested_false-unreach-call1.c below 1 OKAY0.368
nested_true-unreach-call1.c below 1 PASS0.365
overflow_true-unreach-call1.c below 1 PASS0.325
phases_false-unreach-call1.c below 1 OKAY0.41
phases_false-unreach-call2.c below 1 OKAY0.356
phases_true-unreach-call1.c below 1 PASS0.376
phases_true-unreach-call2.c below 1 PASS0.345
simple_false-unreach-call1.c below 1 OKAY0.333
simple_false-unreach-call2.c below 1 OKAY0.324
simple_false-unreach-call3.c below 1 OKAY0.332
simple_false-unreach-call4.c below 1 OKAY0.333
simple_true-unreach-call1.c below 1 PASS0.326
simple_true-unreach-call2.c below 1 PASS0.364
simple_true-unreach-call3.c below 1 PASS0.366
simple_true-unreach-call4.c below 1 PASS0.351
underapprox_false-unreach-call1.c below 1 OKAY0.35
underapprox_false-unreach-call2.c below 1 OKAY0.392
underapprox_true-unreach-call1.c below 1 FAIL0.373
underapprox_true-unreach-call2.c below 1 PASS0.369
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.536
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.9
apache-get-tag_true-unreach-call.c below 1 FAIL0.428
down_true-unreach-call.c below 1 PASS0.398
fragtest_simple_true-unreach-call.c below 1 PASS0.471
half_2_true-unreach-call.c below 1 PASS0.4
heapsort_true-unreach-call.c below 1 PASS116.135
id_build_true-unreach-call.c below 1 PASS0.378
id_trans_false-unreach-call.c below 1 OKAY0.337
id_trans_true-unreach-call.c below 1 PASS0.341
large_const_true-unreach-call.c below 1 PASS0.427
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.391
nested6_true-unreach-call.c below 1 FAIL0.462
nested9_true-unreach-call.c below 1 PASS0.539
nest-if3_true-unreach-call.c below 1 PASS0.458
NetBSD_loop_true-unreach-call.c below 1 PASS0.338
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.397
seq_true-unreach-call.c below 1 PASS0.427
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.138
string_concat-noarr_true-unreach-call.c below 1 PASS0.397
up_true-unreach-call.c below 1 PASS0.361
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 125.123
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.364
bhmr2007_true-unreach-call.c below 1 PASS0.388
cggmp2005b_true-unreach-call.c below 1 PASS0.499
cggmp2005_true-unreach-call.c below 1 PASS0.356
cggmp2005_variant_true-unreach-call.c below 1 PASS0.356
css2003_true-unreach-call.c below 1 PASS0.814
ddlm2013_true-unreach-call.c below 1 PASS0.52
gcnr2008_false-unreach-call.c below 1 OKAY0.963
gj2007b_true-unreach-call.c below 1 FAIL0.377
gj2007_true-unreach-call.c below 1 PASS0.434
gr2006_true-unreach-call.c below 1 PASS0.447
gsv2008_true-unreach-call.c below 1 PASS0.362
hhk2008_true-unreach-call.c below 1 PASS0.343
jm2006_true-unreach-call.c below 1 PASS0.41
jm2006_variant_true-unreach-call.c below 1 PASS0.459
mcmillan2006_true-unreach-call.c below 1 FAIL0.37
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.462
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.326
count_by_1_variant_true-unreach-call.c below 1 PASS0.375
count_by_2_true-unreach-call.c below 1 PASS0.328
count_by_k_true-unreach-call.c below 1 PASS0.341
count_by_nondet_true-unreach-call.c below 1 PASS0.353
gauss_sum_true-unreach-call.c below 1 PASS0.379
half_true-unreach-call.c below 1 FAIL0.392
nested_true-unreach-call.c below 1 PASS0.43
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.924
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.408
array_true-unreach-call.c below 1 FAIL0.4
bubble_sort_false-unreach-call.c below 4 OKAY71.223
bubble_sort_true-unreach-call.c below 1 PASS4.527
compact_false-unreach-call.c below 1 OKAY0.401
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.341
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.343
eureka_01_false-unreach-call.c below 1 OKAY2.165
eureka_01_true-unreach-call.c below 1 FAIL1.43
eureka_05_true-unreach-call.c below 1 FAIL0.686
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.351
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.342
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.317
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.31
heavy_false-unreach-call.c below 1 OKAY0.489
heavy_true-unreach-call.c below 1 PASS0.468
insertion_sort_false-unreach-call.c below 1 OKAY1.418
insertion_sort_true-unreach-call.c below 1 FAIL0.573
invert_string_false-unreach-call.c below 1 OKAY0.472
invert_string_true-unreach-call.c below 1 FAIL0.509
linear_sea.ch_true-unreach-call.c below 1 FAIL0.382
linear_search_false-unreach-call.c below 1 OKAY0.398
lu.cmp_true-unreach-call.c below 3 PASS25.214
ludcmp_false-unreach-call.c below 3 OKAY25.769
matrix_false-unreach-call_true-termination.c below 1 OKAY1.142
matrix_true-unreach-call_true-termination.c below 1 FAIL0.458
n.c11_true-unreach-call.c below 3 FAIL0.454
n.c24_false-unreach-call.c below 3 OKAY6.117
n.c40_true-unreach-call.c below 1 FAIL0.363
nec11_false-unreach-call.c below 1 OKAY0.364
nec20_false-unreach-call.c below 1 OKAY0.381
nec40_true-unreach-call.c below 1 FAIL0.377
string_false-unreach-call.c below 1 OKAY0.577
string_true-unreach-call.c below 1 FAIL0.594
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.583
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.346
sum01_false-unreach-call_true-termination.c below 1 OKAY0.456
sum01_true-unreach-call_true-termination.c below 1 PASS0.359
sum03_false-unreach-call_true-termination.c below 1 OKAY0.499
sum03_true-unreach-call_false-termination.c below 1 PASS0.424
sum04_false-unreach-call_true-termination.c below 1 OKAY0.454
sum04_true-unreach-call_true-termination.c below 1 PASS0.366
sum_array_false-unreach-call.c below 1 OKAY0.534
sum_array_true-unreach-call.c below 1 FAIL0.578
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.332
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.465
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.354
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.332
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.326
trex01_false-unreach-call_true-termination.c below 3 OKAY0.451
trex01_true-unreach-call.c below 3 PASS0.736
trex02_false-unreach-call_true-termination.c below 3 OKAY0.409
trex02_true-unreach-call_true-termination.c below 3 PASS0.404
trex03_false-unreach-call_true-termination.c below 3 OKAY0.68
trex03_true-unreach-call.c below 3 PASS0.673
trex04_true-unreach-call_false-termination.c below 1 PASS0.396
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.348
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS7.238
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.374
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.363
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.983
vogal_false-unreach-call.c below 1 OKAY0.711
vogal_true-unreach-call.c below 1 FAIL0.738
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.298
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.304
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.327
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.318
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 177.922
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.208
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.151
Ackermann03_true-unreach-call.c below 7 FAIL1.188
Ackermann04_true-unreach-call.c below 7 FAIL1.186
Addition01_true-unreach-call_true-termination.c below 2 PASS0.565
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.575
Addition03_false-no-overflow.c below 2 PASS0.58
Addition03_true-unreach-call.c below 2 PASS0.579
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.503
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.437
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.442
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.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.584
gcd02_true-unreach-call.c below 2 FAIL1.039
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.891
McCarthy91_true-unreach-call.c below 7 FAIL0.9
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.583
Primes_true-unreach-call.c below 3 FAIL1.488
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL2.648
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.39
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.393
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1517.356
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.422
afterrec_2calls_true-unreach-call.c below 2 PASS0.401
afterrec_false-unreach-call.c below 2 OKAY0.372
afterrec_true-unreach-call.c below 2 PASS0.371
fibo_10_false-unreach-call.c below TIMEOUT 300.004
fibo_10_true-unreach-call.c below TIMEOUT 300.005
fibo_15_false-unreach-call.c below TIMEOUT 300.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.005
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.022
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.016
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.009
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.017
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.017
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.016
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.023
fibo_5_false-unreach-call.c below TIMEOUT 300.004
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.695
id2_b3_o2_false-unreach-call.c below 2 OKAY0.712
id2_b3_o5_true-unreach-call.c below 2 PASS0.7
id2_b5_o10_true-unreach-call.c below 2 PASS0.688
id2_i5_o5_false-unreach-call.c below 2 OKAY0.425
id2_i5_o5_true-unreach-call.c below 2 PASS0.423
id_b2_o3_true-unreach-call.c below 2 PASS0.617
id_b3_o2_false-unreach-call.c below 2 OKAY0.604
id_b3_o5_true-unreach-call.c below 2 PASS0.586
id_b5_o10_true-unreach-call.c below 2 PASS0.579
id_i10_o10_false-unreach-call.c below 2 OKAY0.376
id_i10_o10_true-unreach-call.c below 2 PASS0.381
id_i15_o15_false-unreach-call.c below 2 OKAY0.389
id_i15_o15_true-unreach-call.c below 2 PASS0.395
id_i20_o20_false-unreach-call.c below 2 OKAY0.391
id_i20_o20_true-unreach-call.c below 2 PASS0.399
id_i25_o25_false-unreach-call.c below 2 OKAY0.401
id_i25_o25_true-unreach-call.c below 2 PASS0.381
id_i5_o5_false-unreach-call.c below 2 OKAY0.38
id_i5_o5_true-unreach-call.c below 2 PASS0.384
id_o1000_false-unreach-call.c below 2 OKAY0.395
id_o100_false-unreach-call.c below 2 OKAY0.393
id_o10_false-unreach-call.c below 2 OKAY0.389
id_o200_false-unreach-call.c below 2 OKAY0.389
id_o20_false-unreach-call.c below 2 OKAY0.403
id_o3_false-unreach-call.c below 2 OKAY0.409
sum_10x0_false-unreach-call.c below 2 OKAY0.436
sum_10x0_true-unreach-call.c below 2 PASS0.408
sum_15x0_false-unreach-call.c below 2 OKAY0.424
sum_15x0_true-unreach-call.c below 2 PASS0.425
sum_20x0_false-unreach-call.c below 2 OKAY0.415
sum_20x0_true-unreach-call.c below 2 PASS0.415
sum_25x0_false-unreach-call.c below 2 OKAY0.422
sum_25x0_true-unreach-call.c below 2 PASS0.413
sum_2x3_false-unreach-call.c below 2 OKAY0.433
sum_2x3_true-unreach-call.c below 2 PASS0.42
sum_non_eq_false-unreach-call.c below 2 OKAY0.448
sum_non_eq_true-unreach-call.c below 2 PASS0.444
sum_non_false-unreach-call.c below 2 OKAY0.419
sum_non_true-unreach-call.c below 2 PASS0.421
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9020.161
/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.418
rec-bhmr2007_true-unreach-call.c below 2 PASS0.436
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.664
rec-cggmp2005_true-unreach-call.c below 2 PASS0.38
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.412
rec-css2003_true-unreach-call.c below 2 PASS0.984
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.834
rec-gj2007b_true-unreach-call.c below 2 FAIL0.393
rec-gj2007_true-unreach-call.c below 2 FAIL0.46
rec-gr2006_true-unreach-call.c below 2 FAIL0.499
rec-gsv2008_true-unreach-call.c below 2 PASS0.405
rec-hhk2008_true-unreach-call.c below 2 PASS0.396
rec-jm2006_true-unreach-call.c below 2 PASS0.488
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.522
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.426
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 307.721
/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.36
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.398
rec-count_by_2_true-unreach-call.c below 2 PASS0.371
rec-count_by_k_true-unreach-call.c below 2 PASS0.398
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.391
rec-gauss_sum_true-unreach-call.c below 2 PASS0.445
rec-half_true-unreach-call.c below 2 FAIL0.411
rec-nested_true-unreach-call.c below 3 FAIL0.544
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.318
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.54
cubic_polynomial_unsafe.c below 2 OKAY0.541
edit_distance_bottom_up.c below 3 FAIL173.029
edit_distance_top_down.c below 3 FAIL4.244
log_log_n_solution.c below 3 FAIL0.443
log_log_n_solution_unsafe.c below 3 OKAY0.435
log_n_solution.c below 2 FAIL0.455
log_n_solution_unsafe.c below 2 OKAY0.484
multivariate_1.c below TIMEOUT 300.005
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 7 FAIL2.515
multivariate_higher_order_unsafe.c below 7 OKAY2.592
n_cubed_solution.c below EXCEPTION 74.558
n_cubed_solution_unsafe.c below EXCEPTION 0.027
n_log_n_solution.c below 8 FAIL1.155
n_log_n_solution_unsafe.c below 8 OKAY1.18
n_squared_two_base_case_even.c below 2 PASS0.554
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.552
n_squared_two_base_case_odd.c below 2 PASS0.566
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.592
pascals_dynamic.c below 3 FAIL2.278
pascals_dynamic_unsafe.c below 3 OKAY2.537
pascals_iterative.c below 1 FAIL4.417
pascals_iterative_unsafe.c below 1 OKAY4.293
pascals_recursive.c below 9 FAIL3.529
pascals_recursive_unsafe.c below 9 OKAY3.457
squared_solution.c below 8 FAIL2.773
squared_solution_unsafe.c below 8 OKAY2.654
two_n_even.c below 2 PASS0.409
two_n_even_unsafe.c below 2 OKAY0.412
two_n_odd.c below 2 PASS0.412
two_n_odd_unsafe.c below 2 OKAY0.412
two_to_n_over_two_even.c below 7 FAIL1.093
two_to_n_over_two_even_unsafe.c below 7 OKAY1.108
two_to_n_over_two_odd.c below 7 FAIL1.098
two_to_n_over_two_odd_unsafe.c below 7 OKAY1.134
two_to_n_squared.c below 5 FAIL16.904
two_to_n_squared_unsafe.c below 5 OKAY16.603
two_to_two_to_n.c below 7 FAIL1.006
two_to_two_to_n_unsafe.c below 7 OKAY1.031
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 17/19
ICRA Time = 932.032
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.346
adding_and_mult_unsafe.c below 1 OKAY0.367
binary_search_array_tree.c below 1 FAIL0.62
exp_add_linear.c below 1 PASS0.421
exp_add_linear_unsafe.c below 1 OKAY0.422
exp_add_loop_rec.c below 1 FAIL0.37
exp_add_loop_rec_unsafe.c below 1 OKAY0.362
exp_add_loop_variable.c below 1 PASS0.407
exp_add_loop_variable_unsafe.c below 1 OKAY0.409
exp_with_linear_inner_loop.c below 1 FAIL0.477
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.468
halving_log1.c below 1 FAIL0.483
linear_two_to_n.c below 7 FAIL20.711
linear_two_to_n_unsafe.c below 7 OKAY20.673
loop_five_to_n.c below 1 PASS0.392
loop_five_to_n_unsafe.c below 1 OKAY0.39
non_loop_five_to_n.c below 7 FAIL49.643
non_loop_five_to_n_unsafe.c below 7 OKAY49.846
power_log.c below 1 PASS0.49
power_log_modified.c below 1 PASS0.484
simple_exponential.c below 1 PASS0.394
simple_exponential_for.c below 1 PASS0.386
simple_exponential_for_unsafe.c below 1 OKAY0.394
simple_exponential_unsafe.c below 1 OKAY0.373
two_to_n_minus_n.c below 7 FAIL2.586
two_to_n_minus_n_loop.c below TIMEOUT 300.026
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.029
two_to_n_minus_n_unsafe.c below 7 OKAY2.685
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 754.654
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.548
02.c below 3 FAIL0.714
03.c below 1 PASS0.441
04.c below 1 PASS0.36
05.c below 3 PASS1.013
06.c below 3 FAIL7.671
07.c below 3 PASS0.51
08.c below 3 PASS1.142
09.c below 3 PASS0.663
10.c below 3 FAIL0.895
11.c below 1 PASS0.347
12.c below 3 PASS1.216
13.c below 3 PASS0.477
14.c below 3 PASS0.422
15.c below 1 PASS0.353
16.c below 1 PASS0.437
17.c below 1 PASS0.43
18.c below 1 PASS0.407
19.c below 1 PASS0.449
20.c below 3 FAIL0.598
21.c below 3 PASS0.495
22.c below 3 FAIL0.674
23.c below 1 PASS0.36
24.c below 1 PASS0.414
25.c below 3 FAIL1.243
26.c below TIMEOUT 300.004
27.c below 1 PASS0.424
28.c below 3 PASS0.478
29.c below 3 PASS0.844
30.c below 1 PASS0.35
31.c below 3 PASS0.817
32.c below 1 FAIL0.367
33.c below 3 PASS1.078
34.c below 1 FAIL0.389
35.c below 1 PASS0.33
36.c below 3 PASS2.38
37.c below 3 FAIL0.496
38.c below 1 FAIL0.387
39.c below 3 PASS0.421
40.c below 3 PASS0.681
41.c below 1 PASS0.41
42.c below 3 PASS0.767
43.c below 3 PASS0.471
44.c below 1 PASS0.384
45.c below 3 FAIL2.255
46.c below 3 FAIL1.357
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 337.369
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.398
AGHKTW2017_foo.c below 1 PASS0.403
AGHKTW2017_loginSafe.c below 1 PASS0.807
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.457
BCK2011_gauss.c below 1 PASS0.428
BCK2011_strength_reduction.c below 1 PASS0.402
BCK2011_strength_reduction_linear.c below 1 PASS0.445
fibonacci_information_flow.c below 1 PASS0.543
TA2005_fib2.c below 1 PASS0.562
TA2005_fib.c below 1 PASS0.459
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.904