[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: 0bb65ddfee3d65b76cb927b278e492b410b1c720 (2017-08-06 18:12:28 -0400) "Merge remote-tracking branch 'origin/ark2' into Newton-ark2"
# 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.39
kmp.c below 1 PASS1.137
qsort.c below 4 PASS0.959
speed_pldi09_fig1.c below 1 PASS0.503
speed_pldi09_fig4_2.c below 1 FAIL0.392
speed_pldi09_fig4_4.c below 1 PASS4.797
speed_pldi09_fig4_5.c below 1 PASS0.381
speed_pldi10_ex1.c below 1 PASS1.761
speed_pldi10_ex3.c below 1 PASS0.526
speed_pldi10_ex4.c below 1 PASS0.552
speed_popl10_fig2_1.c below 1 PASS0.457
speed_popl10_fig2_2.c below 1 FAIL0.386
speed_popl10_nested_multiple.c below 1 PASS0.463
speed_popl10_nested_single.c below 1 PASS0.453
speed_popl10_sequential_single.c below 1 PASS0.408
speed_popl10_simple_multiple.c below 1 PASS0.514
speed_popl10_simple_single_2.c below 1 PASS0.619
speed_popl10_simple_single.c below 1 PASS0.35
t07.c below 1 PASS0.43
t08.c below 1 PASS0.396
t09.c below 1 PASS0.404
t10.c below 1 PASS0.357
t11.c below 1 PASS0.482
t13.c below 1 FAIL0.442
t15.c below 1 PASS0.421
t16.c below 1 PASS0.495
t19.c below 1 PASS0.421
t20.c below 1 PASS0.418
t27.c below 1 PASS0.566
t28.c below 1 PASS0.497
t30.c below 1 FAIL0.429
t37.c below 2 PASS0.612
t39.c below 2 PASS0.539
t46.c below 1 PASS0.433
t47.c below 1 FAIL0.569
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 22.959
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.391
qsort_full.c below 4 PASS11.033
rec1-param_safe.c below 2 PASS0.37
rec1-param_unsafe.c below 2 OKAY0.407
rec1_safe.c below 2 PASS0.37
rec1_unsafe.c below 2 OKAY0.379
rec2-param_safe.c below 2 PASS0.375
rec2-param_unsafe.c below 2 OKAY0.372
rec2_safe.c below 2 PASS0.357
rec2_unsafe.c below 2 OKAY0.368
rec-test.c below 2 PASS0.364
sas03_bothbranches.c below 7 PASS0.824
sas03.c below 2 PASS0.734
simulated_lese_recursive.c below 2 PASS0.456
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 16.8
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.35
count_up_down_unsafe.c below 1 OKAY0.339
divide.c below 1 PASS0.341
factor_unsafe.c below 1 OKAY0.332
for_infinite_loop_1_safe.c below 1 PASS0.327
for_infinite_loop_2_safe.c below 1 PASS0.316
interproc.c below 1 PASS0.304
mult.c below 1 PASS0.325
pointer_arith.c below 1 PASS0.309
quotient.c below 3 PASS0.489
subtract.c below 1 PASS0.324
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.344
sum01_bug02_unsafe.c below 1 OKAY0.591
sum01_real_safe.c below 1 PASS0.345
sum01_safe.c below 1 PASS0.337
sum01_unsafe.c below 1 OKAY0.466
sum02_safe.c below 1 PASS0.364
sum03_safe.c below 1 PASS0.404
sum03_unsafe.c below 1 OKAY0.487
sum04_safe.c below 1 PASS0.34
sum04_unsafe.c below 1 OKAY0.458
terminator_02_safe.c below 1 PASS0.333
terminator_02_unsafe.c below 1 OKAY0.363
terminator_03_safe.c below 1 PASS0.326
terminator_03_unsafe.c below 1 OKAY0.342
token_ring01_safe.c below 4 FAIL196.013
token_ring01_unsafe.c below 4 TIMEOUT 300.007
toy_safe.c below EXCEPTION 170.858
trex01_safe.c below 1 PASS0.75
trex01_unsafe.c below 1 OKAY0.38
trex02_safe2.c below 3 PASS0.398
trex02_safe.c below 3 PASS0.386
trex02_unsafe.c below 3 OKAY0.412
trex03_safe.c below 1 PASS0.429
trex03_unsafe.c below 1 OKAY0.429
trex04_safe.c below 1 PASS0.352
while_infinite_loop_1_safe.c below 1 PASS0.309
while_infinite_loop_2_safe.c below 1 PASS0.306
while_infinite_loop_3_safe.c below 1 PASS0.318
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 12/13
ICRA Time = 680.603
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.416
blogger_simplified1.c below 3 PASS1.143
divided_difference2.c below TIMEOUT 300.005
mult-proc.c below 3 PASS0.363
mult-proc-params.c below 3 PASS0.401
popall.c below 1 PASS0.659
simulated_scc.c below 1 PASS0.652
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.639
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.386
degree2_binomial.c below 1 FAIL0.871
degree2_monomial.c below 1 PASS0.403
degree3_binomial.c below 1 FAIL1.985
degree3_monomial.c below 1 PASS0.476
degree4_binomial.c below 1 FAIL8.014
degree4_monomial.c below 1 PASS0.561
degree5_binomial.c below 1 FAIL189.912
degree5_monomial.c below 1 PASS0.665
ICRA Assertions (True) = 5/9
ICRA Assertions (False) = 0/0
ICRA Time = 203.273
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.452
cubic_with_square_interproc.c below 2 PASS0.614
cubic_with_square_nonlinear.c below 1 FAIL0.382
cubic_with_square_nonlinear_interproc.c below 2 FAIL0.428
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.394
cubic_with_square_unsafe.c below 1 OKAY0.466
multi-input.c below 1 PASS0.485
multi-input_unsafe.c below 1 OKAY0.548
nondet_loop_bound.c below 1 FAIL0.356
nondet_loop_bound_quartic.c below 1 FAIL0.399
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.39
nondet_loop_bound_unsafe.c below 1 OKAY0.363
nonlinear_stratified.c below 1 TIMEOUT300.005
nonlinear_stratified_unsafe.c below 1 OKAY0.703
quartic_with_cube.c below 1 PASS0.632
quartic_with_cube_nonlinear.c below 1 FAIL0.403
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.414
quartic_with_cube_unsafe.c below 1 OKAY0.501
quintic_with_quartic.c below 1 PASS1.026
quintic_with_quartic_nonlinear.c below 1 PASS2.96
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.562
quintic_with_quartic_unsafe.c below 1 OKAY1.032
ICRA Assertions (True) = 6/12
ICRA Assertions (False) = 10/10
ICRA Time = 313.515
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.712
degree2_FD_AllAux_AllAssm.c below 1 PASS106.04
degree2_FD_AllAux_FewAssm.c below 1 PASS7.02
degree2_FD_FewAux_FewAssm.c below 1 PASS0.999
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS1.04
degree3.c below 1 PASS0.739
degree3_FD.c below 1 PASS0.937
degree4.c below 1 PASS0.461
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 117.948
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.442
loop_unsafe.c below 1 OKAY0.458
simulated_lese_parser.c below 1 PASS0.339
simulated_lese_sentinel.c below 1 PASS0.357
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.596
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.351
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.351
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below EXCEPTION 107.032
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 107.032
/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.372
array_false-unreach-call3.c below 1 OKAY0.354
array_true-unreach-call1.c below 1 FAIL0.359
array_true-unreach-call2.c below 1 FAIL0.37
array_true-unreach-call3.c below 1 PASS0.345
array_true-unreach-call4.c below 1 FAIL0.345
const_false-unreach-call1.c below 1 OKAY0.342
const_true-unreach-call1.c below 1 PASS0.348
diamond_false-unreach-call1.c below 1 OKAY0.351
diamond_true-unreach-call1.c below 1 PASS0.339
diamond_true-unreach-call2.c below 1 PASS0.372
functions_false-unreach-call1.c below 3 OKAY0.388
functions_true-unreach-call1.c below 3 PASS0.368
multivar_false-unreach-call1.c below 1 OKAY0.369
multivar_true-unreach-call1.c below 1 PASS0.355
nested_false-unreach-call1.c below 1 OKAY0.376
nested_true-unreach-call1.c below 1 PASS0.375
overflow_true-unreach-call1.c below 1 PASS0.319
phases_false-unreach-call1.c below 1 OKAY0.413
phases_false-unreach-call2.c below 1 OKAY0.336
phases_true-unreach-call1.c below 1 PASS0.399
phases_true-unreach-call2.c below 1 PASS0.346
simple_false-unreach-call1.c below 1 OKAY0.314
simple_false-unreach-call2.c below 1 OKAY0.332
simple_false-unreach-call3.c below 1 OKAY0.332
simple_false-unreach-call4.c below 1 OKAY0.325
simple_true-unreach-call1.c below 1 PASS0.335
simple_true-unreach-call2.c below 1 PASS0.331
simple_true-unreach-call3.c below 1 PASS0.326
simple_true-unreach-call4.c below 1 PASS0.321
underapprox_false-unreach-call1.c below 1 OKAY0.35
underapprox_false-unreach-call2.c below 1 OKAY0.349
underapprox_true-unreach-call1.c below 1 FAIL0.346
underapprox_true-unreach-call2.c below 1 PASS0.346
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.3
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.871
apache-get-tag_true-unreach-call.c below 1 FAIL0.452
down_true-unreach-call.c below 1 PASS0.392
fragtest_simple_true-unreach-call.c below 1 PASS0.435
half_2_true-unreach-call.c below 1 PASS0.382
heapsort_true-unreach-call.c below 1 PASS3.292
id_build_true-unreach-call.c below 1 PASS0.355
id_trans_false-unreach-call.c below 1 OKAY0.338
id_trans_true-unreach-call.c below 1 PASS0.364
large_const_true-unreach-call.c below 1 PASS0.435
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.391
nested6_true-unreach-call.c below 1 FAIL0.512
nested9_true-unreach-call.c below 1 PASS0.554
nest-if3_true-unreach-call.c below 1 PASS0.486
NetBSD_loop_true-unreach-call.c below 1 PASS0.341
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.41
seq_true-unreach-call.c below 1 PASS0.444
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.456
string_concat-noarr_true-unreach-call.c below 1 PASS0.389
up_true-unreach-call.c below 1 PASS0.369
ICRA Assertions (True) = 16/19
ICRA Assertions (False) = 1/1
ICRA Time = 12.668
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.375
bhmr2007_true-unreach-call.c below 1 PASS0.402
cggmp2005b_true-unreach-call.c below 1 PASS0.527
cggmp2005_true-unreach-call.c below 1 PASS0.345
cggmp2005_variant_true-unreach-call.c below 1 PASS0.378
css2003_true-unreach-call.c below 1 PASS0.757
ddlm2013_true-unreach-call.c below 1 PASS0.513
gcnr2008_false-unreach-call.c below 1 OKAY0.987
gj2007b_true-unreach-call.c below 1 FAIL0.391
gj2007_true-unreach-call.c below 1 PASS0.437
gr2006_true-unreach-call.c below 1 PASS0.414
gsv2008_true-unreach-call.c below 1 PASS0.353
hhk2008_true-unreach-call.c below 1 PASS0.352
jm2006_true-unreach-call.c below 1 PASS0.412
jm2006_variant_true-unreach-call.c below 1 PASS0.483
mcmillan2006_true-unreach-call.c below 1 FAIL0.387
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.513
/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.378
count_by_2_true-unreach-call.c below 1 PASS0.33
count_by_k_true-unreach-call.c below 1 PASS0.341
count_by_nondet_true-unreach-call.c below 1 FAIL0.348
gauss_sum_true-unreach-call.c below 1 PASS0.392
half_true-unreach-call.c below 1 FAIL0.373
nested_true-unreach-call.c below 1 PASS0.419
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.908
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.401
array_true-unreach-call.c below 1 FAIL0.392
bubble_sort_false-unreach-call.c below 4 OKAY72.506
bubble_sort_true-unreach-call.c below 1 PASS5.228
compact_false-unreach-call.c below 1 OKAY0.387
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.351
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.326
eureka_01_false-unreach-call.c below 1 OKAY2.261
eureka_01_true-unreach-call.c below 1 FAIL1.562
eureka_05_true-unreach-call.c below 1 FAIL0.766
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.325
for_bounded_loop1_true-unreach-call_true-termination.c below 1 PASS0.338
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.314
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.32
heavy_false-unreach-call.c below 1 OKAY0.509
heavy_true-unreach-call.c below 1 PASS0.498
insertion_sort_false-unreach-call.c below 1 OKAY2.443
insertion_sort_true-unreach-call.c below 1 FAIL0.594
invert_string_false-unreach-call.c below 1 OKAY0.517
invert_string_true-unreach-call.c below 1 FAIL0.548
linear_sea.ch_true-unreach-call.c below 1 FAIL0.375
linear_search_false-unreach-call.c below 1 OKAY0.404
lu.cmp_true-unreach-call.c below 3 PASS65.381
ludcmp_false-unreach-call.c below 3 OKAY66.147
matrix_false-unreach-call_true-termination.c below 1 OKAY1.135
matrix_true-unreach-call_true-termination.c below 1 FAIL0.455
n.c11_true-unreach-call.c below 3 FAIL0.452
n.c24_false-unreach-call.c below 3 OKAY5.43
n.c40_true-unreach-call.c below 1 FAIL0.369
nec11_false-unreach-call.c below 1 OKAY0.383
nec20_false-unreach-call.c below 1 OKAY0.396
nec40_true-unreach-call.c below 1 FAIL0.369
string_false-unreach-call.c below 1 OKAY0.654
string_true-unreach-call.c below 1 FAIL0.618
sum01_bug02_false-unreach-call_true-termination.c below 1 OKAY0.59
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below 1 OKAY0.334
sum01_false-unreach-call_true-termination.c below 1 OKAY0.449
sum01_true-unreach-call_true-termination.c below 1 PASS0.349
sum03_false-unreach-call_true-termination.c below 1 OKAY0.51
sum03_true-unreach-call_false-termination.c below 1 PASS0.446
sum04_false-unreach-call_true-termination.c below 1 OKAY0.519
sum04_true-unreach-call_true-termination.c below 1 PASS0.352
sum_array_false-unreach-call.c below 1 OKAY0.615
sum_array_true-unreach-call.c below 1 FAIL0.685
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.324
terminator_02_false-unreach-call_true-termination.c below 3 OKAY0.461
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.357
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.333
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.339
trex01_false-unreach-call_true-termination.c below 3 OKAY0.464
trex01_true-unreach-call.c below 3 PASS0.713
trex02_false-unreach-call_true-termination.c below 3 OKAY0.411
trex02_true-unreach-call_true-termination.c below 3 PASS0.393
trex03_false-unreach-call_true-termination.c below 3 OKAY0.685
trex03_true-unreach-call.c below 3 PASS0.669
trex04_true-unreach-call_false-termination.c below 1 PASS0.387
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.36
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS11.832
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.36
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.36
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY7.774
vogal_false-unreach-call.c below 1 OKAY0.793
vogal_true-unreach-call.c below 1 FAIL0.829
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.308
while_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.31
while_infinite_loop_3_true-unreach-call_false-termination.c below 1 PASS0.32
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.32
ICRA Assertions (True) = 22/35
ICRA Assertions (False) = 32/32
ICRA Time = 267.105
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS1.305
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY1.244
Ackermann03_true-unreach-call.c below 7 FAIL1.316
Ackermann04_true-unreach-call.c below 7 FAIL1.313
Addition01_true-unreach-call_true-termination.c below 2 PASS0.57
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.589
Addition03_false-no-overflow.c below 2 PASS0.591
Addition03_true-unreach-call.c below 2 PASS0.603
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.495
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.435
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.436
Fibonacci01_true-unreach-call.c below 7 FAIL0.829
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.852
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.831
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.851
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.825
gcd01_true-unreach-call_true-termination.c below 2 PASS0.572
gcd02_true-unreach-call.c below 2 FAIL1.111
McCarthy91_false-unreach-call_false-termination.c below 7 OKAY0.978
McCarthy91_true-unreach-call.c below 7 FAIL0.945
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.599
Primes_true-unreach-call.c below 3 FAIL1.648
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL46.455
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.394
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.414
ICRA Assertions (True) = 6/18
ICRA Assertions (False) = 7/7
ICRA Time = 66.201
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.419
afterrec_2calls_true-unreach-call.c below 2 PASS0.402
afterrec_false-unreach-call.c below 2 OKAY0.386
afterrec_true-unreach-call.c below 2 PASS0.371
fibo_10_false-unreach-call.c below 7 OKAY0.843
fibo_10_true-unreach-call.c below 7 FAIL0.828
fibo_15_false-unreach-call.c below 7 OKAY0.832
fibo_15_true-unreach-call.c below 7 FAIL0.829
fibo_20_false-unreach-call.c below 7 OKAY0.824
fibo_20_true-unreach-call.c below 7 FAIL0.828
fibo_25_false-unreach-call.c below 7 OKAY0.83
fibo_25_true-unreach-call.c below 7 FAIL0.866
fibo_2calls_10_false-unreach-call.c below TIMEOUT 300.022
fibo_2calls_10_true-unreach-call.c below TIMEOUT 300.022
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.019
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.024
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.021
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.024
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.022
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.024
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.021
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.024
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.023
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.021
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.024
fibo_5_false-unreach-call.c below 7 OKAY0.85
fibo_5_true-unreach-call.c below 7 FAIL0.813
fibo_7_false-unreach-call.c below 7 OKAY0.856
fibo_7_true-unreach-call.c below 7 FAIL0.856
id2_b2_o3_true-unreach-call.c below 2 PASS0.727
id2_b3_o2_false-unreach-call.c below 2 OKAY0.77
id2_b3_o5_true-unreach-call.c below 2 PASS0.733
id2_b5_o10_true-unreach-call.c below 2 PASS0.73
id2_i5_o5_false-unreach-call.c below 2 OKAY0.439
id2_i5_o5_true-unreach-call.c below 2 PASS0.422
id_b2_o3_true-unreach-call.c below 2 PASS0.626
id_b3_o2_false-unreach-call.c below 2 OKAY0.606
id_b3_o5_true-unreach-call.c below 2 PASS0.59
id_b5_o10_true-unreach-call.c below 2 PASS0.577
id_i10_o10_false-unreach-call.c below 2 OKAY0.403
id_i10_o10_true-unreach-call.c below 2 PASS0.385
id_i15_o15_false-unreach-call.c below 2 OKAY0.392
id_i15_o15_true-unreach-call.c below 2 PASS0.395
id_i20_o20_false-unreach-call.c below 2 OKAY0.407
id_i20_o20_true-unreach-call.c below 2 PASS0.386
id_i25_o25_false-unreach-call.c below 2 OKAY0.394
id_i25_o25_true-unreach-call.c below 2 PASS0.389
id_i5_o5_false-unreach-call.c below 2 OKAY0.384
id_i5_o5_true-unreach-call.c below 2 PASS0.388
id_o1000_false-unreach-call.c below 2 OKAY0.401
id_o100_false-unreach-call.c below 2 OKAY0.392
id_o10_false-unreach-call.c below 2 OKAY0.403
id_o200_false-unreach-call.c below 2 OKAY0.397
id_o20_false-unreach-call.c below 2 OKAY0.389
id_o3_false-unreach-call.c below 2 OKAY0.388
sum_10x0_false-unreach-call.c below 2 OKAY0.431
sum_10x0_true-unreach-call.c below 2 PASS0.41
sum_15x0_false-unreach-call.c below 2 OKAY0.437
sum_15x0_true-unreach-call.c below 2 PASS0.412
sum_20x0_false-unreach-call.c below 2 OKAY0.417
sum_20x0_true-unreach-call.c below 2 PASS0.424
sum_25x0_false-unreach-call.c below 2 OKAY0.435
sum_25x0_true-unreach-call.c below 2 PASS0.433
sum_2x3_false-unreach-call.c below 2 OKAY0.418
sum_2x3_true-unreach-call.c below 2 PASS0.443
sum_non_eq_false-unreach-call.c below 2 OKAY0.46
sum_non_eq_true-unreach-call.c below 2 PASS0.429
sum_non_false-unreach-call.c below 2 OKAY0.432
sum_non_true-unreach-call.c below 2 PASS0.416
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5430.553
/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.432
rec-cggmp2005b_true-unreach-call.c below 3 PASS0.705
rec-cggmp2005_true-unreach-call.c below 2 PASS0.375
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.428
rec-css2003_true-unreach-call.c below 2 PASS0.96
rec-ddlm2013_true-unreach-call.c below TIMEOUT 300.004
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.845
rec-gj2007b_true-unreach-call.c below 2 FAIL0.394
rec-gj2007_true-unreach-call.c below 2 FAIL0.476
rec-gr2006_true-unreach-call.c below 2 FAIL0.486
rec-gsv2008_true-unreach-call.c below 2 PASS0.41
rec-hhk2008_true-unreach-call.c below 2 PASS0.393
rec-jm2006_true-unreach-call.c below 2 PASS0.454
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.505
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.422
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 307.728
/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.369
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.419
rec-count_by_2_true-unreach-call.c below 2 PASS0.37
rec-count_by_k_true-unreach-call.c below 2 PASS0.39
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.416
rec-gauss_sum_true-unreach-call.c below 2 PASS0.446
rec-half_true-unreach-call.c below 2 FAIL0.414
rec-nested_true-unreach-call.c below 3 FAIL0.541
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.365
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.548
cubic_polynomial_unsafe.c below 2 OKAY0.596
edit_distance_bottom_up.c below 3 FAIL205.074
edit_distance_top_down.c below 3 FAIL4.446
log_log_n_solution.c below 3 FAIL0.437
log_log_n_solution_unsafe.c below 3 OKAY0.446
log_n_solution.c below 2 FAIL0.468
log_n_solution_unsafe.c below 2 OKAY0.453
multivariate_1.c below TIMEOUT 300.006
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below TIMEOUT 300.014
multivariate_higher_order_unsafe.c below TIMEOUT 300.014
n_cubed_solution.c below EXCEPTION 105.494
n_cubed_solution_unsafe.c below EXCEPTION 0.026
n_log_n_solution.c below 9 FAIL1.466
n_log_n_solution_unsafe.c below 9 OKAY1.402
n_squared_two_base_case_even.c below 2 PASS0.558
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.573
n_squared_two_base_case_odd.c below 2 PASS0.563
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.606
pascals_dynamic.c below 3 FAIL3.02
pascals_dynamic_unsafe.c below 3 OKAY3.085
pascals_iterative.c below 1 FAIL5.077
pascals_iterative_unsafe.c below 1 OKAY5.157
pascals_recursive.c below 8 FAIL5.282
pascals_recursive_unsafe.c below 8 OKAY5.413
squared_solution.c below 8 FAIL11.211
squared_solution_unsafe.c below 8 OKAY11.329
two_n_even.c below 2 PASS0.403
two_n_even_unsafe.c below 2 OKAY0.42
two_n_odd.c below 2 PASS0.409
two_n_odd_unsafe.c below 2 OKAY0.425
two_to_n_over_two_even.c below 7 FAIL1.07
two_to_n_over_two_even_unsafe.c below 7 OKAY1.03
two_to_n_over_two_odd.c below 7 FAIL1.028
two_to_n_over_two_odd_unsafe.c below 7 OKAY1.026
two_to_n_squared.c below 5 FAIL24.295
two_to_n_squared_unsafe.c below 5 OKAY24.264
two_to_two_to_n.c below 7 FAIL1.062
two_to_two_to_n_unsafe.c below 7 OKAY1.061
ICRA Assertions (True) = 5/21
ICRA Assertions (False) = 16/19
ICRA Time = 1629.262
/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.368
binary_search_array_tree.c below 1 FAIL0.693
exp_add_linear.c below 1 PASS0.417
exp_add_linear_unsafe.c below 1 OKAY0.427
exp_add_loop_rec.c below 1 FAIL0.377
exp_add_loop_rec_unsafe.c below 1 OKAY0.375
exp_add_loop_variable.c below 1 PASS0.394
exp_add_loop_variable_unsafe.c below 1 OKAY0.416
exp_with_linear_inner_loop.c below 1 FAIL0.489
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.46
halving_log1.c below 1 FAIL0.511
linear_two_to_n.c below TIMEOUT 300.007
linear_two_to_n_unsafe.c below TIMEOUT 300.012
loop_five_to_n.c below 1 PASS0.387
loop_five_to_n_unsafe.c below 1 OKAY0.404
non_loop_five_to_n.c below TIMEOUT 300.04
non_loop_five_to_n_unsafe.c below TIMEOUT 300.031
power_log.c below 1 PASS0.483
power_log_modified.c below 1 PASS0.499
simple_exponential.c below 1 PASS0.4
simple_exponential_for.c below 1 PASS0.388
simple_exponential_for_unsafe.c below 1 OKAY0.376
simple_exponential_unsafe.c below 1 OKAY0.39
two_to_n_minus_n.c below 8 FAIL2.986
two_to_n_minus_n_loop.c below 8 FAIL4.864
two_to_n_minus_n_loop_unsafe.c below 8 OKAY4.65
two_to_n_minus_n_unsafe.c below 8 OKAY3.023
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 10/12
ICRA Time = 1224.241
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below 3 PASS0.556
02.c below 3 FAIL0.708
03.c below 1 PASS0.41
04.c below 1 PASS0.34
05.c below 3 PASS0.977
06.c below 3 PASS7.488
07.c below 3 PASS0.546
08.c below 3 PASS1.11
09.c below 3 PASS0.628
10.c below 3 FAIL0.886
11.c below 1 PASS0.362
12.c below 3 PASS1.201
13.c below 3 PASS0.499
14.c below 3 PASS0.426
15.c below 1 PASS0.336
16.c below 1 PASS0.416
17.c below 1 PASS0.473
18.c below 1 PASS0.383
19.c below 1 PASS0.435
20.c below 3 FAIL0.602
21.c below 3 PASS0.481
22.c below 3 FAIL0.686
23.c below 1 PASS0.352
24.c below 1 PASS0.38
25.c below 3 FAIL1.36
26.c below 3 PASS113.158
27.c below 1 PASS0.417
28.c below 3 PASS0.485
29.c below EXCEPTION 0.39
30.c below 1 PASS0.363
31.c below 3 PASS0.799
32.c below 1 FAIL0.376
33.c below 3 PASS1.268
34.c below 1 FAIL0.377
35.c below 1 PASS0.345
36.c below 3 PASS2.194
37.c below 3 FAIL0.479
38.c below 1 FAIL0.386
39.c below 3 PASS0.404
40.c below 3 PASS0.661
41.c below 1 PASS0.386
42.c below EXCEPTION 0.342
43.c below 3 PASS0.472
44.c below 1 PASS0.362
45.c below 3 FAIL3.151
46.c below 3 FAIL1.758
ICRA Assertions (True) = 33/46
ICRA Assertions (False) = 0/0
ICRA Time = 150.614
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below 1 PASS0.393
AGHKTW2017_foo.c below 1 PASS0.384
AGHKTW2017_loginSafe.c below 1 PASS0.788
AGHKTW2017_loopAndBranch_safe.c below 1 FAIL0.44
BCK2011_gauss.c below 1 PASS0.426
BCK2011_strength_reduction.c below 1 PASS0.41
BCK2011_strength_reduction_linear.c below 1 PASS0.421
fibonacci_information_flow.c below 1 PASS0.571
TA2005_fib2.c below 1 PASS0.556
TA2005_fib.c below 1 PASS0.457
ICRA Assertions (True) = 9/10
ICRA Assertions (False) = 0/0
ICRA Time = 4.846