[Version Information]
WALi-OpenNWA version: 0f994ef6a5cbe02200899575605ae35f227d9ddb (2017-07-12 11:45:09 -0500) "Added programs and files used for POPL18"
duet version: 81b6696f6f312fabfa1611e9943c2a6ea2f1ed79 (2017-07-20 23:59:08 +0200) "Fixed build after merge"
# Installed packages for 4.02.1+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.5.3  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.4.1  Equivalent of the C preprocessor for OCaml programs
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170101  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.8  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.1  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             20170627v3  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.375
kmp.c below 1 PASS1.744
qsort.c below 5 PASS0.912
speed_pldi09_fig1.c below 1 PASS0.481
speed_pldi09_fig4_2.c below 1 FAIL0.405
speed_pldi09_fig4_4.c below 1 PASS4.742
speed_pldi09_fig4_5.c below 1 PASS0.417
speed_pldi10_ex1.c below 1 PASS1.239
speed_pldi10_ex3.c below 1 PASS0.513
speed_pldi10_ex4.c below 1 PASS0.549
speed_popl10_fig2_1.c below 1 PASS0.449
speed_popl10_fig2_2.c below 1 FAIL0.376
speed_popl10_nested_multiple.c below 1 PASS0.457
speed_popl10_nested_single.c below 1 PASS0.435
speed_popl10_sequential_single.c below 1 PASS0.387
speed_popl10_simple_multiple.c below 1 PASS0.533
speed_popl10_simple_single_2.c below 1 PASS0.621
speed_popl10_simple_single.c below 1 PASS0.359
t07.c below 1 PASS0.425
t08.c below 1 PASS0.392
t09.c below 1 PASS0.391
t10.c below 1 PASS0.38
t11.c below 1 PASS0.468
t13.c below 1 FAIL0.404
t15.c below 1 PASS0.423
t16.c below 1 PASS0.407
t19.c below 1 PASS0.395
t20.c below 1 PASS0.395
t27.c below 1 PASS0.556
t28.c below 1 PASS0.46
t30.c below 1 FAIL0.436
t37.c below 2 PASS0.613
t39.c below 2 PASS0.527
t46.c below 1 PASS0.422
t47.c below 1 FAIL0.577
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.665
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.351
qsort_full.c below 4 PASS6.305
rec1-param_safe.c below 2 PASS0.38
rec1-param_unsafe.c below 2 OKAY0.371
rec1_safe.c below 2 PASS0.347
rec1_unsafe.c below 2 OKAY0.359
rec2-param_safe.c below 2 PASS0.37
rec2-param_unsafe.c below 2 OKAY0.38
rec2_safe.c below 2 PASS0.37
rec2_unsafe.c below 2 OKAY0.364
rec-test.c below 2 PASS0.35
sas03_bothbranches.c below 7 PASS0.678
sas03.c below 2 PASS0.718
simulated_lese_recursive.c below 2 PASS0.455
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 11.798
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.352
count_up_down_unsafe.c below 1 OKAY0.35
divide.c below 1 PASS0.339
factor_unsafe.c below 1 OKAY0.327
for_infinite_loop_1_safe.c below 1 PASS0.319
for_infinite_loop_2_safe.c below 1 PASS0.326
interproc.c below 1 PASS0.33
mult.c below 1 PASS0.328
pointer_arith.c below 1 PASS0.293
quotient.c below 3 PASS0.477
subtract.c below 1 PASS0.327
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.366
sum01_bug02_unsafe.c below 1 OKAY0.589
sum01_real_safe.c below 1 PASS0.337
sum01_safe.c below 1 PASS0.352
sum01_unsafe.c below 1 OKAY0.47
sum02_safe.c below 1 PASS0.374
sum03_safe.c below 1 PASS0.385
sum03_unsafe.c below 1 OKAY0.483
sum04_safe.c below 1 PASS0.353
sum04_unsafe.c below 1 OKAY0.479
terminator_02_safe.c below 1 PASS0.332
terminator_02_unsafe.c below 1 OKAY0.358
terminator_03_safe.c below 1 PASS0.32
terminator_03_unsafe.c below 1 OKAY0.326
token_ring01_safe.c below 4 FAIL100.149
token_ring01_unsafe.c below 4 OKAY262.825
toy_safe.c below EXCEPTION 168.351
trex01_safe.c below 1 PASS0.552
trex01_unsafe.c below 1 OKAY0.363
trex02_safe2.c below 3 PASS0.392
trex02_safe.c below 3 PASS0.427
trex02_unsafe.c below 3 OKAY0.382
trex03_safe.c below 1 PASS0.438
trex03_unsafe.c below 1 OKAY0.427
trex04_safe.c below 1 PASS0.365
while_infinite_loop_1_safe.c below 1 PASS0.324
while_infinite_loop_2_safe.c below 1 PASS0.328
while_infinite_loop_3_safe.c below 1 PASS0.355
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 544.97
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.39
blogger_simplified1.c below 3 PASS1.11
divided_difference2.c below TIMEOUT 300.006
mult-proc.c below 3 PASS0.387
mult-proc-params.c below 3 PASS0.391
popall.c below 1 PASS0.711
simulated_scc.c below 1 PASS0.645
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.64
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.356
degree2_binomial.c below 1 FAIL0.836
degree2_monomial.c below 1 PASS0.382
degree3_binomial.c below 1 FAIL1.358
degree3_monomial.c below 1 PASS0.453
degree4_binomial.c below 1 FAIL3.151
degree4_monomial.c below 1 PASS0.727
degree5_binomial.c below 1 FAIL11.971
degree5_monomial.c below 1 PASS0.596
ICRA Assertions (True) = 5/9
ICRA Assertions (False) = 0/0
ICRA Time = 19.83
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.46
cubic_with_square_interproc.c below 2 FAIL0.59
cubic_with_square_nonlinear.c below 1 FAIL0.385
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.414
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.381
cubic_with_square_unsafe.c below 1 OKAY0.463
multi-input.c below 1 PASS214.096
multi-input_unsafe.c below 1 OKAY0.505
nondet_loop_bound.c below 1 FAIL0.351
nondet_loop_bound_quartic.c below 1 FAIL0.41
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.388
nondet_loop_bound_unsafe.c below 1 OKAY0.377
nonlinear_stratified.c below 1 PASS80.001
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.005
quartic_with_cube.c below 1 PASS0.636
quartic_with_cube_nonlinear.c below 1 FAIL0.391
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.408
quartic_with_cube_unsafe.c below 1 OKAY0.497
quintic_with_quartic.c below 1 PASS1.025
quintic_with_quartic_nonlinear.c below 1 PASS0.436
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.455
quintic_with_quartic_unsafe.c below 1 OKAY1.044
ICRA Assertions (True) = 6/12
ICRA Assertions (False) = 9/10
ICRA Time = 603.718
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.67
degree2_FD_AllAux_AllAssm.c below 1 PASS215.74
degree2_FD_AllAux_FewAssm.c below 1 PASS4.971
degree2_FD_FewAux_FewAssm.c below 1 PASS0.879
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.915
degree3.c below 1 PASS0.672
degree3_FD.c below 1 PASS0.838
degree4.c below 1 PASS0.439
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 225.124
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.446
loop_unsafe.c below 1 OKAY0.456
simulated_lese_parser.c below 1 PASS0.365
simulated_lese_sentinel.c below 1 PASS0.35
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.617
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.353
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.353
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.006
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.006
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below 1 OKAY0.352
array_false-unreach-call2.c below 1 OKAY0.377
array_false-unreach-call3.c below 1 OKAY0.356
array_true-unreach-call1.c below 1 FAIL0.354
array_true-unreach-call2.c below 1 FAIL0.373
array_true-unreach-call3.c below 1 PASS0.345
array_true-unreach-call4.c below 1 FAIL0.327
const_false-unreach-call1.c below 1 OKAY0.345
const_true-unreach-call1.c below 1 PASS0.348
diamond_false-unreach-call1.c below 1 OKAY0.378
diamond_true-unreach-call1.c below 1 PASS0.377
diamond_true-unreach-call2.c below 1 PASS0.385
functions_false-unreach-call1.c below 3 OKAY0.376
functions_true-unreach-call1.c below 3 PASS0.393
multivar_false-unreach-call1.c below 1 OKAY0.367
multivar_true-unreach-call1.c below 1 PASS0.358
nested_false-unreach-call1.c below 1 OKAY0.368
nested_true-unreach-call1.c below 1 PASS0.369
overflow_true-unreach-call1.c below 1 PASS0.328
phases_false-unreach-call1.c below 1 OKAY0.421
phases_false-unreach-call2.c below 1 OKAY0.356
phases_true-unreach-call1.c below 1 PASS0.389
phases_true-unreach-call2.c below 1 PASS0.34
simple_false-unreach-call1.c below 1 OKAY0.338
simple_false-unreach-call2.c below 1 OKAY0.324
simple_false-unreach-call3.c below 1 OKAY0.323
simple_false-unreach-call4.c below 1 OKAY0.326
simple_true-unreach-call1.c below 1 PASS0.323
simple_true-unreach-call2.c below 1 PASS0.329
simple_true-unreach-call3.c below 1 PASS0.339
simple_true-unreach-call4.c below 1 PASS0.327
underapprox_false-unreach-call1.c below 1 OKAY0.346
underapprox_false-unreach-call2.c below 1 OKAY0.35
underapprox_true-unreach-call1.c below 1 FAIL0.344
underapprox_true-unreach-call2.c below 1 PASS0.337
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.388
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.865
apache-get-tag_true-unreach-call.c below 1 FAIL0.437
down_true-unreach-call.c below 1 PASS0.366
fragtest_simple_true-unreach-call.c below 1 PASS0.445
half_2_true-unreach-call.c below 1 PASS0.389
heapsort_true-unreach-call.c below 1 PASS1.313
id_build_true-unreach-call.c below 1 PASS0.355
id_trans_false-unreach-call.c below 1 OKAY0.336
large_const_true-unreach-call.c below 1 PASS0.438
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.38
nested6_true-unreach-call.c below 1 FAIL0.515
nested9_true-unreach-call.c below 1 PASS0.521
nest-if3_true-unreach-call.c below 1 PASS0.471
NetBSD_loop_true-unreach-call.c below 1 PASS0.357
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.394
seq_true-unreach-call.c below 1 PASS0.43
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.394
string_concat-noarr_true-unreach-call.c below 1 PASS0.398
up_true-unreach-call.c below 1 PASS0.374
ICRA Assertions (True) = 15/18
ICRA Assertions (False) = 1/1
ICRA Time = 10.178
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.384
bhmr2007_true-unreach-call.c below 1 PASS0.391
cggmp2005b_true-unreach-call.c below 1 PASS0.506
cggmp2005_true-unreach-call.c below 1 PASS0.362
cggmp2005_variant_true-unreach-call.c below 1 PASS0.375
css2003_true-unreach-call.c below 1 PASS0.79
ddlm2013_true-unreach-call.c below 1 PASS0.504
gcnr2008_false-unreach-call.c below 1 OKAY0.91
gj2007b_true-unreach-call.c below 1 FAIL0.38
gj2007_true-unreach-call.c below 1 PASS0.448
gr2006_true-unreach-call.c below 1 PASS0.422
gsv2008_true-unreach-call.c below 1 PASS0.345
hhk2008_true-unreach-call.c below 1 PASS0.342
jm2006_true-unreach-call.c below 1 PASS0.399
jm2006_variant_true-unreach-call.c below 1 PASS0.473
mcmillan2006_true-unreach-call.c below 1 FAIL0.389
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.42
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.327
count_by_1_variant_true-unreach-call.c below 1 PASS0.388
count_by_2_true-unreach-call.c below 1 PASS0.345
count_by_k_true-unreach-call.c below 1 PASS0.353
count_by_nondet_true-unreach-call.c below 1 FAIL0.347
gauss_sum_true-unreach-call.c below 1 PASS0.375
half_true-unreach-call.c below 1 FAIL0.373
nested_true-unreach-call.c below 1 PASS0.424
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.932
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.383
array_true-unreach-call.c below 1 FAIL0.4
bubble_sort_false-unreach-call.c below 4 OKAY50.362
bubble_sort_true-unreach-call.c below 1 PASS3.785
compact_false-unreach-call.c below 1 OKAY0.394
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.35
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.345
eureka_01_false-unreach-call.c below 1 OKAY2.087
eureka_01_true-unreach-call.c below 1 FAIL1.469
eureka_05_true-unreach-call.c below 1 FAIL0.645
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.337
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.329
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.318
heavy_false-unreach-call.c below 1 OKAY0.457
heavy_true-unreach-call.c below 1 PASS0.458
insertion_sort_false-unreach-call.c below 1 OKAY1.761
insertion_sort_true-unreach-call.c below 1 FAIL0.594
invert_string_false-unreach-call.c below 1 OKAY0.515
invert_string_true-unreach-call.c below 1 FAIL0.529
linear_sea.ch_true-unreach-call.c below 1 FAIL0.388
linear_search_false-unreach-call.c below 1 OKAY0.414
lu.cmp_true-unreach-call.c below 3 PASS17.621
ludcmp_false-unreach-call.c below 3 OKAY17.843
matrix_false-unreach-call_true-termination.c below 1 OKAY1.127
matrix_true-unreach-call_true-termination.c below 1 FAIL0.43
n.c11_true-unreach-call.c below 3 FAIL0.442
n.c24_false-unreach-call.c below 3 OKAY2.839
n.c40_true-unreach-call.c below 1 FAIL0.363
nec11_false-unreach-call.c below 1 OKAY0.363
nec20_false-unreach-call.c below 1 OKAY0.393
nec40_true-unreach-call.c below 1 FAIL0.385
string_false-unreach-call.c below 1 OKAY0.61
string_true-unreach-call.c below 1 FAIL0.605
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.609
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.34
sum01_false-unreach-call_true-termination.c below 1 OKAY0.455
sum01_true-unreach-call_true-termination.c below 1 PASS0.362
sum03_false-unreach-call_true-termination.c below 1 OKAY0.498
sum03_true-unreach-call_false-termination.c below 1 PASS0.427
sum04_false-unreach-call_true-termination.c below 1 OKAY0.476
sum04_true-unreach-call_true-termination.c below 1 PASS0.355
sum_array_false-unreach-call.c below 1 OKAY0.589
sum_array_true-unreach-call.c below 1 FAIL0.677
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.33
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.442
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.358
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.333
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.337
trex01_false-unreach-call_true-termination.c below 3 OKAY0.436
trex01_true-unreach-call.c below 3 PASS0.685
trex02_false-unreach-call_true-termination.c below 3 OKAY0.406
trex02_true-unreach-call_true-termination.c below 3 PASS0.379
trex03_false-unreach-call_true-termination.c below 3 OKAY0.683
trex03_true-unreach-call.c below 3 PASS0.668
trex04_true-unreach-call_false-termination.c below 1 PASS0.395
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.363
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS6.221
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.377
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.358
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY4.59
vogal_false-unreach-call.c below 1 OKAY0.775
vogal_true-unreach-call.c below 1 FAIL0.762
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.303
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.315
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.312
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 134.255
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.981
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.94
Ackermann03_true-unreach-call.c below 7 FAIL0.973
Ackermann04_true-unreach-call.c below 7 FAIL0.98
Addition01_true-unreach-call_true-termination.c below 2 PASS0.548
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.535
Addition03_false-no-overflow.c below 2 PASS0.535
Addition03_true-unreach-call.c below 2 PASS0.564
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.462
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.419
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.432
Fibonacci01_true-unreach-call.c below 7 FAIL0.696
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.673
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.681
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.686
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.696
gcd01_true-unreach-call_true-termination.c below 2 PASS0.528
gcd02_true-unreach-call.c below 2 FAIL0.968
McCarthy91_false-unreach-call_false-termination.c below TIMEOUT 300.005
McCarthy91_true-unreach-call.c below TIMEOUT 300.007
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.548
Primes_true-unreach-call.c below 3 FAIL1.404
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.82
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.366
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.371
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 6/7
ICRA Time = 616.818
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.425
afterrec_2calls_true-unreach-call.c below 2 PASS0.416
afterrec_false-unreach-call.c below 2 OKAY0.386
afterrec_true-unreach-call.c below 2 PASS0.38
fibo_10_false-unreach-call.c below 7 OKAY0.683
fibo_10_true-unreach-call.c below 7 FAIL0.646
fibo_15_false-unreach-call.c below 7 OKAY0.662
fibo_15_true-unreach-call.c below 7 FAIL0.672
fibo_20_false-unreach-call.c below 7 OKAY0.674
fibo_20_true-unreach-call.c below 7 FAIL0.662
fibo_25_false-unreach-call.c below 7 OKAY0.674
fibo_25_true-unreach-call.c below 7 FAIL0.697
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.008
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.014
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.009
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.01
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.015
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.004
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.009
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.011
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.01
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.009
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.011
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.013
fibo_5_false-unreach-call.c below 7 OKAY0.683
fibo_5_true-unreach-call.c below 7 FAIL0.699
fibo_7_false-unreach-call.c below 7 OKAY0.66
fibo_7_true-unreach-call.c below 7 FAIL0.67
id2_b2_o3_true-unreach-call.c below 2 PASS0.646
id2_b3_o2_false-unreach-call.c below 2 OKAY0.655
id2_b3_o5_true-unreach-call.c below 2 PASS0.628
id2_b5_o10_true-unreach-call.c below 2 PASS0.605
id2_i5_o5_false-unreach-call.c below 2 OKAY0.405
id2_i5_o5_true-unreach-call.c below 2 PASS0.398
id_b2_o3_true-unreach-call.c below 2 PASS0.551
id_b3_o2_false-unreach-call.c below 2 OKAY0.53
id_b3_o5_true-unreach-call.c below 2 PASS0.555
id_b5_o10_true-unreach-call.c below 2 PASS0.558
id_i10_o10_false-unreach-call.c below 2 OKAY0.38
id_i10_o10_true-unreach-call.c below 2 PASS0.363
id_i15_o15_false-unreach-call.c below 2 OKAY0.375
id_i15_o15_true-unreach-call.c below 2 PASS0.373
id_i20_o20_false-unreach-call.c below 2 OKAY0.375
id_i20_o20_true-unreach-call.c below 2 PASS0.378
id_i25_o25_false-unreach-call.c below 2 OKAY0.38
id_i25_o25_true-unreach-call.c below 2 PASS0.388
id_i5_o5_false-unreach-call.c below 2 OKAY0.384
id_i5_o5_true-unreach-call.c below 2 PASS0.377
id_o1000_false-unreach-call.c below 2 OKAY0.384
id_o100_false-unreach-call.c below 2 OKAY0.385
id_o10_false-unreach-call.c below 2 OKAY0.387
id_o200_false-unreach-call.c below 2 OKAY0.376
id_o20_false-unreach-call.c below 2 OKAY0.374
id_o3_false-unreach-call.c below 2 OKAY0.385
sum_10x0_false-unreach-call.c below 2 OKAY0.412
sum_10x0_true-unreach-call.c below 2 PASS0.413
sum_15x0_false-unreach-call.c below 2 OKAY0.405
sum_15x0_true-unreach-call.c below 2 PASS0.414
sum_20x0_false-unreach-call.c below 2 OKAY0.424
sum_20x0_true-unreach-call.c below 2 PASS0.422
sum_25x0_false-unreach-call.c below 2 OKAY0.425
sum_25x0_true-unreach-call.c below 2 PASS0.409
sum_2x3_false-unreach-call.c below 2 OKAY0.424
sum_2x3_true-unreach-call.c below 2 PASS0.428
sum_non_eq_false-unreach-call.c below 2 OKAY0.429
sum_non_eq_true-unreach-call.c below 2 PASS0.411
sum_non_false-unreach-call.c below 2 OKAY0.411
sum_non_true-unreach-call.c below 2 PASS0.404
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5427.307
/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.439
rec-bhmr2007_true-unreach-call.c below 2 PASS0.433
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.617
rec-cggmp2005_true-unreach-call.c below 2 PASS0.375
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.429
rec-css2003_true-unreach-call.c below 2 PASS0.975
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.082
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.774
rec-gj2007b_true-unreach-call.c below 2 FAIL0.372
rec-gj2007_true-unreach-call.c below 2 FAIL0.467
rec-gr2006_true-unreach-call.c below 2 FAIL0.449
rec-gsv2008_true-unreach-call.c below 2 PASS0.448
rec-hhk2008_true-unreach-call.c below 2 PASS0.388
rec-jm2006_true-unreach-call.c below 2 PASS0.448
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.547
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.427
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.67
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c below 2 PASS0.373
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.412
rec-count_by_2_true-unreach-call.c below 2 PASS0.389
rec-count_by_k_true-unreach-call.c below 2 PASS0.423
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.407
rec-gauss_sum_true-unreach-call.c below 2 PASS0.427
rec-half_true-unreach-call.c below 2 PASS0.395
rec-nested_true-unreach-call.c below 3 FAIL0.558
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.384
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.528
cubic_polynomial_unsafe.c below 2 OKAY0.53
edit_distance_bottom_up.c below 3 FAIL131.997
edit_distance_top_down.c below 3 FAIL2.897
log_log_n_solution.c below 3 FAIL0.425
log_log_n_solution_unsafe.c below 3 OKAY0.438
log_n_solution.c below 2 FAIL0.442
log_n_solution_unsafe.c below 2 OKAY0.456
multivariate_1.c below TIMEOUT 300.105
multivariate_1_unsafe.c below TIMEOUT 300.006
multivariate_higher_order.c below 7 FAIL32.642
multivariate_higher_order_unsafe.c below 7 OKAY8.016
n_cubed_solution.c below EXCEPTION 46.086
n_cubed_solution_unsafe.c below EXCEPTION 0.023
n_log_n_solution.c below 10 FAIL4.473
n_log_n_solution_unsafe.c below 10 OKAY4.51
n_squared_two_base_case_even.c below 2 PASS0.478
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.471
n_squared_two_base_case_odd.c below 2 PASS0.502
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.486
pascals_dynamic.c below 3 FAIL2.649
pascals_dynamic_unsafe.c below 3 OKAY2.614
pascals_iterative.c below 1 FAIL3.653
pascals_iterative_unsafe.c below 1 OKAY3.684
pascals_recursive.c below 8 FAIL2.475
pascals_recursive_unsafe.c below 8 OKAY2.417
squared_solution.c below TIMEOUT 300.004
squared_solution_unsafe.c below TIMEOUT 300.009
two_n_even.c below 2 PASS0.401
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.422
two_to_n_over_two_even.c below TIMEOUT 300.004
two_to_n_over_two_even_unsafe.c below 8 OKAY299.296
two_to_n_over_two_odd.c below TIMEOUT 300.004
two_to_n_over_two_odd_unsafe.c below TIMEOUT 300.005
two_to_n_squared.c below 8 EXCEPTION 17.801
two_to_n_squared_unsafe.c below 8 EXCEPTION 17.471
two_to_two_to_n.c below 7 FAIL0.856
two_to_two_to_n_unsafe.c below 7 OKAY0.897
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 14/19
ICRA Time = 2690.997
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.374
adding_and_mult_unsafe.c below 1 OKAY0.372
binary_search_array_tree.c below 1 FAIL0.69
exp_add_linear.c below 1 PASS0.43
exp_add_linear_unsafe.c below 1 OKAY0.424
exp_add_loop_rec.c below 1 FAIL0.366
exp_add_loop_rec_unsafe.c below 1 OKAY0.367
exp_add_loop_variable.c below 1 PASS0.416
exp_add_loop_variable_unsafe.c below 1 OKAY0.411
exp_with_linear_inner_loop.c below 1 FAIL0.493
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.492
halving_log1.c below 1 FAIL0.514
linear_two_to_n.c below 8 FAIL1.126
linear_two_to_n_unsafe.c below 8 OKAY1.07
loop_five_to_n.c below 1 PASS0.359
loop_five_to_n_unsafe.c below 1 OKAY0.388
non_loop_five_to_n.c below TIMEOUT 300.045
non_loop_five_to_n_unsafe.c below TIMEOUT 300.036
power_log.c below 1 PASS0.477
power_log_modified.c below 1 PASS0.512
simple_exponential.c below 1 PASS0.389
simple_exponential_for.c below 1 PASS0.39
simple_exponential_for_unsafe.c below 1 OKAY0.388
simple_exponential_unsafe.c below 1 OKAY0.383
two_to_n_minus_n.c below 7 FAIL1.172
two_to_n_minus_n_loop.c below 7 FAIL1.652
two_to_n_minus_n_loop_unsafe.c below 7 OKAY1.675
two_to_n_minus_n_unsafe.c below 7 OKAY1.175
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 11/12
ICRA Time = 616.586
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.526
02.c below 3 FAIL0.672
03.c below 1 PASS0.412
04.c below 1 PASS0.353
05.c below 3 PASS0.948
06.c below 3 PASS11.612
07.c below 3 PASS0.506
08.c below 3 PASS1.01
09.c below 3 PASS0.649
10.c below 3 FAIL0.811
11.c below 1 PASS0.362
12.c below 3 PASS1.123
13.c below 3 PASS0.491
14.c below 3 PASS0.425
15.c below 1 PASS0.34
16.c below 1 PASS0.399
17.c below EXCEPTION 0.361
18.c below 1 PASS0.395
19.c below 1 PASS0.431
20.c below 3 FAIL0.581
21.c below 3 PASS0.476
22.c below 3 FAIL0.951
23.c below 1 PASS0.357
24.c below 1 PASS0.392
25.c below 3 FAIL1.149
26.c below TIMEOUT 300.004
27.c below 1 PASS0.411
28.c below 3 PASS0.464
29.c below EXCEPTION 0.394
30.c below 1 PASS0.366
31.c below 3 PASS0.742
32.c below 1 FAIL0.365
33.c below 3 PASS1.061
34.c below 1 FAIL0.385
35.c below 1 PASS0.325
36.c below 3 PASS2.247
37.c below 3 FAIL0.454
38.c below 1 FAIL0.379
39.c below 3 PASS0.41
40.c below 3 PASS0.69
41.c below 1 PASS0.373
42.c below 3 PASS0.775
43.c below 3 PASS0.436
44.c below 1 PASS0.356
45.c below 3 FAIL2.343
46.c below 3 FAIL1.882
ICRA Assertions (True) = 32/46
ICRA Assertions (False) = 0/0
ICRA Time = 340.594
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.385
AGHKTW2017_foo.c below 1 PASS0.402
AGHKTW2017_loginSafe.c below 1 PASS0.751
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.447
BCK2011_gauss.c below 1 PASS0.418
BCK2011_strength_reduction.c below 1 PASS0.393
BCK2011_strength_reduction_linear.c below 1 PASS0.423
fibonacci_information_flow.c below 1 PASS0.565
TA2005_fib2.c below 1 PASS0.535
TA2005_fib.c below 1 PASS0.449
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.768