[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.369
kmp.c below 1 PASS1.067
qsort.c below 4 PASS0.919
speed_pldi09_fig1.c below 1 PASS0.508
speed_pldi09_fig4_2.c below 1 FAIL0.401
speed_pldi09_fig4_4.c below 1 PASS0.512
speed_pldi09_fig4_5.c below 1 PASS0.404
speed_pldi10_ex1.c below 1 PASS1.25
speed_pldi10_ex3.c below 1 PASS0.51
speed_pldi10_ex4.c below 1 PASS0.515
speed_popl10_fig2_1.c below 1 PASS0.462
speed_popl10_fig2_2.c below 1 FAIL0.375
speed_popl10_nested_multiple.c below 1 PASS0.476
speed_popl10_nested_single.c below 1 PASS0.443
speed_popl10_sequential_single.c below 1 PASS0.394
speed_popl10_simple_multiple.c below 1 PASS0.524
speed_popl10_simple_single_2.c below 1 PASS0.657
speed_popl10_simple_single.c below 1 PASS0.372
t07.c below 1 PASS0.441
t08.c below 1 PASS0.381
t09.c below 1 PASS0.402
t10.c below 1 PASS0.375
t11.c below 1 PASS0.476
t13.c below 1 FAIL0.429
t15.c below 1 PASS0.457
t16.c below 1 PASS0.395
t19.c below 1 PASS0.401
t20.c below 1 PASS0.383
t27.c below 1 PASS0.55
t28.c below 1 PASS0.48
t30.c below 1 FAIL0.421
t37.c below 2 PASS0.607
t39.c below 2 PASS0.555
t46.c below 1 PASS0.41
t47.c below 1 PASS0.501
ICRA Assertions (True) = 30/35
ICRA Assertions (False) = 0/0
ICRA Time = 17.822
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.378
qsort_full.c below 4 PASS9.364
rec1-param_safe.c below 2 PASS0.385
rec1-param_unsafe.c below 2 OKAY0.374
rec1_safe.c below 2 PASS0.37
rec1_unsafe.c below 2 OKAY0.355
rec2-param_safe.c below 2 PASS0.368
rec2-param_unsafe.c below 2 OKAY0.373
rec2_safe.c below 2 PASS0.361
rec2_unsafe.c below 2 OKAY0.371
rec-test.c below 2 PASS0.349
sas03_bothbranches.c below 7 PASS0.815
sas03.c below 2 PASS0.765
simulated_lese_recursive.c below 2 PASS0.443
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 15.071
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.345
count_up_down_unsafe.c below 1 OKAY0.339
divide.c below 1 PASS0.353
factor_unsafe.c below 1 OKAY0.332
for_infinite_loop_1_safe.c below 1 PASS0.321
for_infinite_loop_2_safe.c below 1 PASS0.32
interproc.c below 1 PASS0.308
mult.c below 1 PASS0.329
pointer_arith.c below 1 PASS0.324
quotient.c below 3 PASS0.475
subtract.c below 1 PASS0.329
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.361
sum01_bug02_unsafe.c below 1 OKAY0.579
sum01_real_safe.c below 1 PASS0.333
sum01_safe.c below 1 PASS0.351
sum01_unsafe.c below 1 OKAY0.443
sum02_safe.c below 1 PASS0.367
sum03_safe.c below 1 PASS0.414
sum03_unsafe.c below 1 OKAY0.461
sum04_safe.c below 1 PASS0.366
sum04_unsafe.c below 1 OKAY0.467
terminator_02_safe.c below 1 PASS0.332
terminator_02_unsafe.c below 1 OKAY0.354
terminator_03_safe.c below 1 PASS0.327
terminator_03_unsafe.c below 1 OKAY0.33
token_ring01_safe.c below 4 FAIL139.8
token_ring01_unsafe.c below 4 OKAY240.683
toy_safe.c below EXCEPTION 166.023
trex01_safe.c below 1 PASS0.715
trex01_unsafe.c below 1 OKAY0.383
trex02_safe2.c below 3 PASS0.398
trex02_safe.c below 3 PASS0.407
trex02_unsafe.c below 3 OKAY0.411
trex03_safe.c below 1 PASS0.439
trex03_unsafe.c below 1 OKAY0.438
trex04_safe.c below 1 PASS0.353
while_infinite_loop_1_safe.c below 1 PASS0.315
while_infinite_loop_2_safe.c below 1 PASS0.369
while_infinite_loop_3_safe.c below 1 PASS0.321
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 560.315
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.416
blogger_simplified1.c below 3 PASS1.041
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.376
mult-proc-params.c below 3 PASS0.397
popall.c below 1 PASS0.68
simulated_scc.c below 1 PASS0.634
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.549
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.365
degree2_binomial.c below 1 PASS0.716
degree2_monomial.c below 1 PASS0.403
degree3_binomial.c below 1 FAIL2.19
degree3_monomial.c below 1 PASS0.461
degree4_binomial.c below 1 FAIL6.976
degree4_monomial.c below 1 PASS0.533
degree5_binomial.c below 1 TIMEOUT300.018
degree5_monomial.c below 1 PASS0.652
ICRA Assertions (True) = 6/9
ICRA Assertions (False) = 0/0
ICRA Time = 312.314
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 FAIL0.475
cubic_with_square_interproc.c below 2 FAIL0.581
cubic_with_square_nonlinear.c below 1 FAIL0.388
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.433
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.397
cubic_with_square_unsafe.c below 1 OKAY0.458
multi-input.c below 1 FAIL0.487
multi-input_unsafe.c below 1 OKAY0.467
nondet_loop_bound.c below 1 FAIL0.359
nondet_loop_bound_quartic.c below 1 FAIL0.394
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.376
nondet_loop_bound_unsafe.c below 1 OKAY0.363
nonlinear_stratified.c below 1 TIMEOUT300.004
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube.c below 1 FAIL0.624
quartic_with_cube_nonlinear.c below 1 FAIL0.387
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.408
quartic_with_cube_unsafe.c below 1 OKAY0.498
quintic_with_quartic.c below 1 PASS1.023
quintic_with_quartic_nonlinear.c below 1 TIMEOUT300.005
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.551
quintic_with_quartic_unsafe.c below 1 OKAY1.048
ICRA Assertions (True) = 1/12
ICRA Assertions (False) = 9/10
ICRA Time = 909.73
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.693
degree2_FD_AllAux_AllAssm.c below 1 PASS103.991
degree2_FD_AllAux_FewAssm.c below 1 PASS6.675
degree2_FD_FewAux_FewAssm.c below 1 PASS1.005
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.993
degree3.c below 1 PASS0.766
degree3_FD.c below 1 PASS0.962
degree4.c below 1 PASS0.46
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 115.545
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.443
loop_unsafe.c below 1 OKAY0.447
simulated_lese_parser.c below 1 PASS0.357
simulated_lese_sentinel.c below 1 PASS0.357
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.604
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.361
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.361
/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.355
array_false-unreach-call2.c below 1 OKAY0.374
array_false-unreach-call3.c below 1 OKAY0.355
array_true-unreach-call1.c below 1 FAIL0.35
array_true-unreach-call2.c below 1 FAIL0.376
array_true-unreach-call3.c below 1 PASS0.345
array_true-unreach-call4.c below 1 FAIL0.338
const_false-unreach-call1.c below 1 OKAY0.351
const_true-unreach-call1.c below 1 PASS0.332
diamond_false-unreach-call1.c below 1 OKAY0.355
diamond_true-unreach-call1.c below 1 PASS0.345
diamond_true-unreach-call2.c below 1 PASS0.376
functions_false-unreach-call1.c below 3 OKAY0.376
functions_true-unreach-call1.c below 3 PASS0.377
multivar_false-unreach-call1.c below 1 OKAY0.355
multivar_true-unreach-call1.c below 1 PASS0.342
nested_false-unreach-call1.c below 1 OKAY0.375
nested_true-unreach-call1.c below 1 PASS0.375
overflow_true-unreach-call1.c below 1 PASS0.321
phases_false-unreach-call1.c below 1 OKAY0.426
phases_false-unreach-call2.c below 1 OKAY0.352
phases_true-unreach-call1.c below 1 PASS0.406
phases_true-unreach-call2.c below 1 PASS0.358
simple_false-unreach-call1.c below 1 OKAY0.316
simple_false-unreach-call2.c below 1 OKAY0.321
simple_false-unreach-call3.c below 1 OKAY0.322
simple_false-unreach-call4.c below 1 OKAY0.335
simple_true-unreach-call1.c below 1 PASS0.33
simple_true-unreach-call2.c below 1 PASS0.327
simple_true-unreach-call3.c below 1 PASS0.317
simple_true-unreach-call4.c below 1 PASS0.33
underapprox_false-unreach-call1.c below 1 OKAY0.347
underapprox_false-unreach-call2.c below 1 OKAY0.35
underapprox_true-unreach-call1.c below 1 FAIL0.358
underapprox_true-unreach-call2.c below 1 PASS0.365
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.333
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.902
apache-get-tag_true-unreach-call.c below 1 FAIL0.437
down_true-unreach-call.c below 1 PASS0.358
fragtest_simple_true-unreach-call.c below 1 PASS0.457
half_2_true-unreach-call.c below 1 PASS0.408
heapsort_true-unreach-call.c below 1 PASS115.672
id_build_true-unreach-call.c below 1 PASS0.362
id_trans_false-unreach-call.c below 1 OKAY0.333
id_trans_true-unreach-call.c below 1 PASS0.341
large_const_true-unreach-call.c below 1 PASS0.431
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.382
nested6_true-unreach-call.c below 1 FAIL0.49
nested9_true-unreach-call.c below 1 PASS0.538
nest-if3_true-unreach-call.c below 1 PASS0.454
NetBSD_loop_true-unreach-call.c below 1 PASS0.335
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.402
seq_true-unreach-call.c below 1 PASS0.448
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.205
string_concat-noarr_true-unreach-call.c below 1 PASS0.412
up_true-unreach-call.c below 1 PASS0.363
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 124.73
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.369
bhmr2007_true-unreach-call.c below 1 PASS0.396
cggmp2005b_true-unreach-call.c below 1 PASS0.51
cggmp2005_true-unreach-call.c below 1 PASS0.356
cggmp2005_variant_true-unreach-call.c below 1 PASS0.361
css2003_true-unreach-call.c below 1 PASS0.815
ddlm2013_true-unreach-call.c below 1 PASS0.494
gcnr2008_false-unreach-call.c below 1 OKAY0.946
gj2007b_true-unreach-call.c below 1 FAIL0.383
gj2007_true-unreach-call.c below 1 PASS0.453
gr2006_true-unreach-call.c below 1 PASS0.431
gsv2008_true-unreach-call.c below 1 PASS0.356
hhk2008_true-unreach-call.c below 1 PASS0.327
jm2006_true-unreach-call.c below 1 PASS0.422
jm2006_variant_true-unreach-call.c below 1 PASS0.468
mcmillan2006_true-unreach-call.c below 1 FAIL0.39
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.477
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.33
count_by_1_variant_true-unreach-call.c below 1 PASS0.373
count_by_2_true-unreach-call.c below 1 PASS0.332
count_by_k_true-unreach-call.c below 1 PASS0.324
count_by_nondet_true-unreach-call.c below 1 PASS0.352
gauss_sum_true-unreach-call.c below 1 PASS0.383
half_true-unreach-call.c below 1 FAIL0.357
nested_true-unreach-call.c below 1 PASS0.423
ICRA Assertions (True) = 7/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.874
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.397
array_true-unreach-call.c below 1 FAIL0.405
bubble_sort_false-unreach-call.c below 4 OKAY70.114
bubble_sort_true-unreach-call.c below 1 PASS4.258
compact_false-unreach-call.c below 1 OKAY0.389
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.356
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.34
eureka_01_false-unreach-call.c below 1 OKAY2.18
eureka_01_true-unreach-call.c below 1 FAIL1.408
eureka_05_true-unreach-call.c below 1 FAIL0.691
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.334
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.335
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.323
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.328
heavy_false-unreach-call.c below 1 OKAY0.476
heavy_true-unreach-call.c below 1 PASS0.483
insertion_sort_false-unreach-call.c below 1 OKAY1.424
insertion_sort_true-unreach-call.c below 1 FAIL0.578
invert_string_false-unreach-call.c below 1 OKAY0.478
invert_string_true-unreach-call.c below 1 FAIL0.503
linear_sea.ch_true-unreach-call.c below 1 FAIL0.397
linear_search_false-unreach-call.c below 1 OKAY0.401
lu.cmp_true-unreach-call.c below 3 PASS25.395
ludcmp_false-unreach-call.c below 3 OKAY25.365
matrix_false-unreach-call_true-termination.c below 1 OKAY1.131
matrix_true-unreach-call_true-termination.c below 1 FAIL0.439
n.c11_true-unreach-call.c below 3 FAIL0.435
n.c24_false-unreach-call.c below 3 OKAY5.918
n.c40_true-unreach-call.c below 1 FAIL0.365
nec11_false-unreach-call.c below 1 OKAY0.364
nec20_false-unreach-call.c below 1 OKAY0.401
nec40_true-unreach-call.c below 1 FAIL0.374
string_false-unreach-call.c below 1 OKAY0.592
string_true-unreach-call.c below 1 FAIL0.606
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.556
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.344
sum01_false-unreach-call_true-termination.c below 1 OKAY0.443
sum01_true-unreach-call_true-termination.c below 1 PASS0.358
sum03_false-unreach-call_true-termination.c below 1 OKAY0.51
sum03_true-unreach-call_false-termination.c below 1 PASS0.431
sum04_false-unreach-call_true-termination.c below 1 OKAY0.454
sum04_true-unreach-call_true-termination.c below 1 PASS0.363
sum_array_false-unreach-call.c below 1 OKAY0.519
sum_array_true-unreach-call.c below 1 FAIL0.571
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.323
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.459
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.358
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.335
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.325
trex01_false-unreach-call_true-termination.c below 3 OKAY0.451
trex01_true-unreach-call.c below 3 PASS0.734
trex02_false-unreach-call_true-termination.c below 3 OKAY0.399
trex02_true-unreach-call_true-termination.c below 3 PASS0.396
trex03_false-unreach-call_true-termination.c below 3 OKAY0.691
trex03_true-unreach-call.c below 3 PASS0.685
trex04_true-unreach-call_false-termination.c below 1 PASS0.383
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.1
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.359
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.365
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY6.958
vogal_false-unreach-call.c below 1 OKAY0.732
vogal_true-unreach-call.c below 1 FAIL0.739
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.302
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.299
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.312
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.317
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 175.902
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.236
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.114
Ackermann03_true-unreach-call.c below 7 FAIL1.161
Ackermann04_true-unreach-call.c below 7 FAIL1.188
Addition01_true-unreach-call_true-termination.c below 2 PASS0.572
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.583
Addition03_false-no-overflow.c below 2 PASS0.568
Addition03_true-unreach-call.c below 2 PASS0.565
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.509
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.416
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.42
Fibonacci01_true-unreach-call.c below TIMEOUT 300.006
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.005
Fibonacci05_false-unreach-call_true-termination.c below TIMEOUT 300.006
gcd01_true-unreach-call_true-termination.c below 2 PASS0.583
gcd02_true-unreach-call.c below 2 FAIL1.002
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.969
McCarthy91_true-unreach-call.c below 7 FAIL0.932
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.589
Primes_true-unreach-call.c below 3 FAIL1.556
recHanoi01_true-unreach-call_true-termination.c below 7 FAIL2.698
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.401
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.396
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 5/7
ICRA Time = 1517.487
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.417
afterrec_2calls_true-unreach-call.c below 2 PASS0.411
afterrec_false-unreach-call.c below 2 OKAY0.374
afterrec_true-unreach-call.c below 2 PASS0.374
fibo_10_false-unreach-call.c below TIMEOUT 300.004
fibo_10_true-unreach-call.c below TIMEOUT 300.004
fibo_15_false-unreach-call.c below TIMEOUT 300.006
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.006
fibo_25_false-unreach-call.c below TIMEOUT 300.005
fibo_25_true-unreach-call.c below TIMEOUT 300.007
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.016
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.022
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.023
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.016
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.024
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.015
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.017
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.017
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.022
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.007
fibo_7_false-unreach-call.c below TIMEOUT 300.005
fibo_7_true-unreach-call.c below TIMEOUT 300.005
id2_b2_o3_true-unreach-call.c below 2 PASS0.689
id2_b3_o2_false-unreach-call.c below 2 OKAY0.69
id2_b3_o5_true-unreach-call.c below 2 PASS0.717
id2_b5_o10_true-unreach-call.c below 2 PASS0.678
id2_i5_o5_false-unreach-call.c below 2 OKAY0.418
id2_i5_o5_true-unreach-call.c below 2 PASS0.425
id_b2_o3_true-unreach-call.c below 2 PASS0.599
id_b3_o2_false-unreach-call.c below 2 OKAY0.619
id_b3_o5_true-unreach-call.c below 2 PASS0.589
id_b5_o10_true-unreach-call.c below 2 PASS0.594
id_i10_o10_false-unreach-call.c below 2 OKAY0.364
id_i10_o10_true-unreach-call.c below 2 PASS0.387
id_i15_o15_false-unreach-call.c below 2 OKAY0.389
id_i15_o15_true-unreach-call.c below 2 PASS0.393
id_i20_o20_false-unreach-call.c below 2 OKAY0.398
id_i20_o20_true-unreach-call.c below 2 PASS0.375
id_i25_o25_false-unreach-call.c below 2 OKAY0.392
id_i25_o25_true-unreach-call.c below 2 PASS0.395
id_i5_o5_false-unreach-call.c below 2 OKAY0.397
id_i5_o5_true-unreach-call.c below 2 PASS0.375
id_o1000_false-unreach-call.c below 2 OKAY0.387
id_o100_false-unreach-call.c below 2 OKAY0.394
id_o10_false-unreach-call.c below 2 OKAY0.39
id_o200_false-unreach-call.c below 2 OKAY0.394
id_o20_false-unreach-call.c below 2 OKAY0.396
id_o3_false-unreach-call.c below 2 OKAY0.398
sum_10x0_false-unreach-call.c below 2 OKAY0.443
sum_10x0_true-unreach-call.c below 2 PASS0.422
sum_15x0_false-unreach-call.c below 2 OKAY0.441
sum_15x0_true-unreach-call.c below 2 PASS0.416
sum_20x0_false-unreach-call.c below 2 OKAY0.419
sum_20x0_true-unreach-call.c below 2 PASS0.425
sum_25x0_false-unreach-call.c below 2 OKAY0.427
sum_25x0_true-unreach-call.c below 2 PASS0.428
sum_2x3_false-unreach-call.c below 2 OKAY0.444
sum_2x3_true-unreach-call.c below 2 PASS0.433
sum_non_eq_false-unreach-call.c below 2 OKAY0.438
sum_non_eq_true-unreach-call.c below 2 PASS0.433
sum_non_false-unreach-call.c below 2 OKAY0.418
sum_non_true-unreach-call.c below 2 PASS0.413
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 23/38
ICRA Time = 9020.201
/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.444
rec-bhmr2007_true-unreach-call.c below 2 PASS0.416
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.657
rec-cggmp2005_true-unreach-call.c below 2 PASS0.384
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.411
rec-css2003_true-unreach-call.c below 2 PASS0.952
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.795
rec-gj2007b_true-unreach-call.c below 2 FAIL0.397
rec-gj2007_true-unreach-call.c below 2 FAIL0.471
rec-gr2006_true-unreach-call.c below 2 FAIL0.494
rec-gsv2008_true-unreach-call.c below 2 PASS0.409
rec-hhk2008_true-unreach-call.c below 2 PASS0.396
rec-jm2006_true-unreach-call.c below 2 PASS0.434
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.516
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.415
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 307.595
/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.363
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.406
rec-count_by_2_true-unreach-call.c below 2 PASS0.357
rec-count_by_k_true-unreach-call.c below 2 PASS0.397
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.393
rec-gauss_sum_true-unreach-call.c below 2 PASS0.443
rec-half_true-unreach-call.c below 2 FAIL0.397
rec-nested_true-unreach-call.c below 3 FAIL0.574
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.33
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.537
cubic_polynomial_unsafe.c below 2 OKAY0.531
edit_distance_bottom_up.c below 3 FAIL171.57
edit_distance_top_down.c below 3 FAIL4.221
log_log_n_solution.c below 3 FAIL0.437
log_log_n_solution_unsafe.c below 3 OKAY0.449
log_n_solution.c below 2 FAIL0.476
log_n_solution_unsafe.c below 2 OKAY0.445
multivariate_1.c below TIMEOUT 300.005
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL2.528
multivariate_higher_order_unsafe.c below 7 OKAY2.498
n_cubed_solution.c below EXCEPTION 75.02
n_cubed_solution_unsafe.c below EXCEPTION 0.025
n_log_n_solution.c below 8 FAIL1.145
n_log_n_solution_unsafe.c below 8 OKAY1.109
n_squared_two_base_case_even.c below 2 PASS0.564
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.563
n_squared_two_base_case_odd.c below 2 PASS0.573
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.577
pascals_dynamic.c below 3 FAIL2.26
pascals_dynamic_unsafe.c below 3 OKAY2.309
pascals_iterative.c below 1 FAIL4.296
pascals_iterative_unsafe.c below 1 OKAY4.241
pascals_recursive.c below 9 FAIL3.645
pascals_recursive_unsafe.c below 9 OKAY3.416
squared_solution.c below 8 FAIL2.683
squared_solution_unsafe.c below 8 OKAY2.662
two_n_even.c below 2 PASS0.423
two_n_even_unsafe.c below 2 OKAY0.41
two_n_odd.c below 2 PASS0.413
two_n_odd_unsafe.c below 2 OKAY0.417
two_to_n_over_two_even.c below 7 FAIL1.126
two_to_n_over_two_even_unsafe.c below 7 OKAY1.096
two_to_n_over_two_odd.c below 7 FAIL1.079
two_to_n_over_two_odd_unsafe.c below 7 OKAY1.03
two_to_n_squared.c below 5 FAIL16.634
two_to_n_squared_unsafe.c below 5 OKAY16.414
two_to_two_to_n.c below 7 FAIL1.015
two_to_two_to_n_unsafe.c below 7 OKAY1.034
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 17/19
ICRA Time = 929.882
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.358
adding_and_mult_unsafe.c below 1 OKAY0.36
binary_search_array_tree.c below 1 FAIL0.587
exp_add_linear.c below 1 PASS0.426
exp_add_linear_unsafe.c below 1 OKAY0.435
exp_add_loop_rec.c below 1 FAIL0.367
exp_add_loop_rec_unsafe.c below 1 OKAY0.348
exp_add_loop_variable.c below 1 PASS0.403
exp_add_loop_variable_unsafe.c below 1 OKAY0.418
exp_with_linear_inner_loop.c below 1 FAIL0.482
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.48
halving_log1.c below 1 FAIL0.479
linear_two_to_n.c below 7 FAIL20.528
linear_two_to_n_unsafe.c below 7 OKAY20.531
loop_five_to_n.c below 1 PASS0.375
loop_five_to_n_unsafe.c below 1 OKAY0.379
non_loop_five_to_n.c below 7 FAIL49.293
non_loop_five_to_n_unsafe.c below 7 OKAY49.942
power_log.c below 1 PASS0.473
power_log_modified.c below 1 PASS0.49
simple_exponential.c below 1 PASS0.39
simple_exponential_for.c below 1 PASS0.385
simple_exponential_for_unsafe.c below 1 OKAY0.393
simple_exponential_unsafe.c below 1 OKAY0.395
two_to_n_minus_n.c below 7 FAIL2.608
two_to_n_minus_n_loop.c below TIMEOUT 300.025
two_to_n_minus_n_loop_unsafe.c below TIMEOUT 300.028
two_to_n_minus_n_unsafe.c below 7 OKAY2.58
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 753.958
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.531
02.c below 3 FAIL0.679
03.c below 1 PASS0.42
04.c below 1 PASS0.348
05.c below 3 PASS1.004
06.c below 3 FAIL7.055
07.c below 3 PASS0.513
08.c below 3 PASS1.117
09.c below 3 PASS0.657
10.c below 3 FAIL0.843
11.c below 1 PASS0.336
12.c below 3 PASS1.155
13.c below 3 PASS0.497
14.c below 3 PASS0.42
15.c below 1 PASS0.333
16.c below 1 PASS0.413
17.c below 1 PASS0.409
18.c below 1 PASS0.415
19.c below 1 PASS0.441
20.c below 3 FAIL0.602
21.c below 3 PASS0.475
22.c below 3 FAIL0.654
23.c below 1 PASS0.367
24.c below 1 PASS0.393
25.c below 3 FAIL1.189
26.c below TIMEOUT 300.004
27.c below 1 PASS0.416
28.c below 3 PASS0.495
29.c below 3 PASS0.846
30.c below 1 PASS0.359
31.c below 3 PASS0.797
32.c below 1 FAIL0.361
33.c below 3 PASS1.048
34.c below 1 FAIL0.393
35.c below 1 PASS0.326
36.c below 3 PASS2.287
37.c below 3 FAIL0.471
38.c below 1 FAIL0.378
39.c below 3 PASS0.4
40.c below 3 PASS0.647
41.c below 1 PASS0.367
42.c below 3 PASS0.731
43.c below 3 PASS0.437
44.c below 1 PASS0.357
45.c below 3 FAIL2.184
46.c below 3 FAIL1.3
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 335.87
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.401
AGHKTW2017_foo.c below 1 PASS0.413
AGHKTW2017_loginSafe.c below 1 PASS0.805
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.427
BCK2011_gauss.c below 1 PASS0.427
BCK2011_strength_reduction.c below 1 PASS0.404
BCK2011_strength_reduction_linear.c below 1 PASS0.433
fibonacci_information_flow.c below 1 PASS0.576
TA2005_fib2.c below 1 PASS0.549
TA2005_fib.c below 1 PASS0.459
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.894