[Version Information]
WALi-OpenNWA version: 539f35b837c29d4da7968b324f451666fd3447d8 (2017-07-03 16:54:01 -0500) "Adding several benchmarks to exponential"
duet version: 47a42e9090c5b4c10af414eb09f72f3b6089c3b6 (2017-07-03 19:57:17 -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.359
kmp.c below 1 PASS1.612
qsort.c below 2 PASS0.598
speed_pldi09_fig1.c below 1 PASS0.475
speed_pldi09_fig4_2.c below 1 FAIL0.392
speed_pldi09_fig4_4.c below 1 PASS20.71
speed_pldi09_fig4_5.c below 1 PASS0.399
speed_pldi10_ex1.c below 1 PASS1.155
speed_pldi10_ex3.c below 1 PASS0.508
speed_pldi10_ex4.c below 1 PASS0.527
speed_popl10_fig2_1.c below 1 PASS0.447
speed_popl10_fig2_2.c below 1 FAIL0.369
speed_popl10_nested_multiple.c below 1 PASS0.511
speed_popl10_nested_single.c below 1 PASS0.459
speed_popl10_sequential_single.c below 1 PASS0.409
speed_popl10_simple_multiple.c below 1 PASS0.532
speed_popl10_simple_single_2.c below 1 PASS0.678
speed_popl10_simple_single.c below 1 PASS0.359
t07.c below 1 PASS0.427
t08.c below 1 PASS0.39
t09.c below 1 PASS0.384
t10.c below 1 PASS0.347
t11.c below 1 PASS0.459
t13.c below 1 FAIL0.422
t15.c below 1 PASS0.416
t16.c below 1 PASS0.399
t19.c below 1 PASS0.387
t20.c below 1 PASS0.38
t27.c below 1 PASS0.553
t28.c below 1 PASS0.463
t30.c below 1 FAIL0.408
t37.c below 2 PASS0.608
t39.c below 2 PASS0.527
t46.c below 1 PASS0.41
t47.c below 1 FAIL0.54
ICRA Assertions (True) = 29/35
ICRA Assertions (False) = 0/0
ICRA Time = 38.019
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below 2 PASS0.362
qsort_full.c below 4 PASS5.329
rec1-param_safe.c below 2 PASS0.398
rec1-param_unsafe.c below 2 OKAY0.389
rec1_safe.c below 2 PASS0.363
rec1_unsafe.c below 2 OKAY0.37
rec2-param_safe.c below 2 PASS0.383
rec2-param_unsafe.c below 2 OKAY0.378
rec2_safe.c below 2 PASS0.379
rec2_unsafe.c below 2 OKAY0.359
rec-test.c below 2 PASS0.365
sas03_bothbranches.c below 2 PASS0.407
sas03.c below 2 PASS0.795
simulated_lese_recursive.c below 2 PASS0.429
ICRA Assertions (True) = 10/10
ICRA Assertions (False) = 4/4
ICRA Time = 10.706
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below 1 PASS0.338
count_up_down_unsafe.c below 1 OKAY0.35
divide.c below 1 PASS0.335
factor_unsafe.c below 1 OKAY0.324
for_infinite_loop_1_safe.c below 1 PASS0.338
for_infinite_loop_2_safe.c below 1 PASS0.321
interproc.c below 1 PASS0.3
mult.c below 1 PASS0.334
pointer_arith.c below 1 PASS0.307
quotient.c below 3 PASS0.478
subtract.c below 1 PASS0.329
sum01_bug02_sum01_bug02_base.case_unsafe.c below 1 OKAY0.347
sum01_bug02_unsafe.c below 1 OKAY0.584
sum01_real_safe.c below 1 PASS0.326
sum01_safe.c below 1 PASS0.337
sum01_unsafe.c below 1 OKAY0.462
sum02_safe.c below 1 PASS0.355
sum03_safe.c below 1 PASS0.395
sum03_unsafe.c below 1 OKAY0.472
sum04_safe.c below 1 PASS0.349
sum04_unsafe.c below 1 OKAY0.454
terminator_02_safe.c below 1 PASS0.308
terminator_02_unsafe.c below 1 OKAY0.365
terminator_03_safe.c below 1 PASS0.33
terminator_03_unsafe.c below 1 OKAY0.326
token_ring01_safe.c below 4 FAIL66.593
token_ring01_unsafe.c below 4 OKAY171.156
toy_safe.c below EXCEPTION 162.721
trex01_safe.c below 1 PASS0.736
trex01_unsafe.c below 1 OKAY0.365
trex02_safe2.c below 2 PASS0.348
trex02_safe.c below 2 PASS0.348
trex02_unsafe.c below 2 OKAY0.352
trex03_safe.c below 1 PASS0.427
trex03_unsafe.c below 1 OKAY0.417
trex04_safe.c below 1 PASS0.36
while_infinite_loop_1_safe.c below 1 PASS0.306
while_infinite_loop_2_safe.c below 1 PASS0.309
while_infinite_loop_3_safe.c below 1 PASS0.306
ICRA Assertions (True) = 24/26
ICRA Assertions (False) = 13/13
ICRA Time = 413.908
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below 3 PASS0.381
blogger_simplified1.c below 3 PASS1.059
divided_difference2.c below TIMEOUT 300.009
mult-proc.c below 3 PASS0.366
mult-proc-params.c below 3 PASS0.392
popall.c below 1 PASS0.667
simulated_scc.c below 1 PASS0.63
ICRA Assertions (True) = 6/7
ICRA Assertions (False) = 0/0
ICRA Time = 303.504
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below 1 PASS0.344
degree2_binomial.c below 1 PASS0.713
degree2_monomial.c below 1 PASS0.382
degree3_binomial.c below 1 PASS1.362
degree3_monomial.c below 1 PASS0.428
degree4_binomial.c below 1 PASS2.583
degree4_monomial.c below 1 PASS0.471
degree5_binomial.c below 1 PASS7.12
degree5_monomial.c below 1 PASS0.557
ICRA Assertions (True) = 9/9
ICRA Assertions (False) = 0/0
ICRA Time = 13.96
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below 1 PASS0.43
cubic_with_square_interproc.c below 2 PASS0.581
cubic_with_square_nonlinear.c below 1 PASS0.357
cubic_with_square_nonlinear_interproc.c below 2 PASS0.395
cubic_with_square_nonlinear_unsafe.c below 1 OKAY0.38
cubic_with_square_unsafe.c below 1 OKAY0.429
multi-input.c below 1 PASS213.216
multi-input_unsafe.c below 1 OKAY0.486
nondet_loop_bound.c below 1 PASS0.361
nondet_loop_bound_quartic.c below 1 PASS0.39
nondet_loop_bound_quartic_unsafe.c below 1 OKAY0.369
nondet_loop_bound_unsafe.c below 1 OKAY0.368
nonlinear_stratified.c below 1 PASS79.305
nonlinear_stratified_unsafe.c below 1 TIMEOUT300.004
quartic_with_cube.c below 1 PASS0.609
quartic_with_cube_nonlinear.c below 1 PASS0.384
quartic_with_cube_nonlinear_unsafe.c below 1 OKAY0.375
quartic_with_cube_unsafe.c below 1 OKAY0.479
quintic_with_quartic.c below 1 PASS1.013
quintic_with_quartic_nonlinear.c below 1 PASS0.434
quintic_with_quartic_nonlinear_unsafe.c below 1 OKAY0.441
quintic_with_quartic_unsafe.c below 1 OKAY1.006
ICRA Assertions (True) = 12/12
ICRA Assertions (False) = 9/10
ICRA Time = 601.812
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below 1 PASS0.675
degree2_FD_AllAux_AllAssm.c below 1 PASS156.046
degree2_FD_AllAux_FewAssm.c below 1 PASS4.825
degree2_FD_FewAux_FewAssm.c below 1 PASS0.87
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below 1 PASS0.894
degree3.c below 1 PASS0.596
degree3_FD.c below 1 PASS0.801
degree4.c below 1 PASS0.446
ICRA Assertions (True) = 8/8
ICRA Assertions (False) = 0/0
ICRA Time = 165.153
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below 1 PASS0.413
loop_unsafe.c below 1 OKAY0.434
simulated_lese_parser.c below 1 PASS0.341
simulated_lese_sentinel.c below 1 PASS0.354
ICRA Assertions (True) = 3/3
ICRA Assertions (False) = 1/1
ICRA Time = 1.542
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below 1 PASS0.344
ICRA Assertions (True) = 1/1
ICRA Assertions (False) = 0/0
ICRA Time = 0.344
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below TIMEOUT 300.004
ICRA Assertions (True) = 0/1
ICRA Assertions (False) = 0/0
ICRA Time = 300.004
/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.359
array_false-unreach-call3.c below 1 OKAY0.346
array_true-unreach-call1.c below 1 FAIL0.346
array_true-unreach-call2.c below 1 FAIL0.36
array_true-unreach-call3.c below 1 PASS0.343
array_true-unreach-call4.c below 1 FAIL0.342
const_false-unreach-call1.c below 1 OKAY0.343
const_true-unreach-call1.c below 1 PASS0.33
diamond_false-unreach-call1.c below 1 OKAY0.372
diamond_true-unreach-call1.c below 1 PASS0.366
diamond_true-unreach-call2.c below 1 PASS0.364
functions_false-unreach-call1.c below 3 OKAY0.384
functions_true-unreach-call1.c below 3 PASS0.366
multivar_false-unreach-call1.c below 1 OKAY0.353
multivar_true-unreach-call1.c below 1 PASS0.343
nested_false-unreach-call1.c below 1 OKAY0.365
nested_true-unreach-call1.c below 1 PASS0.373
overflow_true-unreach-call1.c below 1 PASS0.322
phases_false-unreach-call1.c below 1 OKAY0.408
phases_false-unreach-call2.c below 1 OKAY0.333
phases_true-unreach-call1.c below 1 PASS0.401
phases_true-unreach-call2.c below 1 PASS0.336
simple_false-unreach-call1.c below 1 OKAY0.318
simple_false-unreach-call2.c below 1 OKAY0.324
simple_false-unreach-call3.c below 1 OKAY0.315
simple_false-unreach-call4.c below 1 OKAY0.329
simple_true-unreach-call1.c below 1 PASS0.316
simple_true-unreach-call2.c below 1 PASS0.31
simple_true-unreach-call3.c below 1 PASS0.337
simple_true-unreach-call4.c below 1 PASS0.326
underapprox_false-unreach-call1.c below 1 OKAY0.331
underapprox_false-unreach-call2.c below 1 OKAY0.344
underapprox_true-unreach-call1.c below 1 FAIL0.344
underapprox_true-unreach-call2.c below 1 PASS0.342
ICRA Assertions (True) = 15/19
ICRA Assertions (False) = 16/16
ICRA Time = 12.142
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below 1 PASS0.813
apache-get-tag_true-unreach-call.c below 1 FAIL0.414
down_true-unreach-call.c below 1 PASS0.366
fragtest_simple_true-unreach-call.c below 1 PASS0.424
half_2_true-unreach-call.c below 1 PASS0.405
heapsort_true-unreach-call.c below 1 TIMEOUT300.196
id_build_true-unreach-call.c below 1 PASS0.466
id_trans_false-unreach-call.c below 1 OKAY0.335
large_const_true-unreach-call.c below 1 PASS0.419
MADWiFi-encode_ie_ok_true-unreach-call.c below 1 PASS0.383
nested6_true-unreach-call.c below 1 FAIL0.475
nested9_true-unreach-call.c below 1 PASS0.529
nest-if3_true-unreach-call.c below 1 PASS0.454
NetBSD_loop_true-unreach-call.c below 1 PASS0.342
sendmail-close-angle_true-unreach-call.c below 1 FAIL0.383
seq_true-unreach-call.c below 1 PASS0.423
SpamAssassin-loop_true-unreach-call.c below 1 PASS1.396
string_concat-noarr_true-unreach-call.c below 1 PASS0.381
up_true-unreach-call.c below 1 PASS0.377
ICRA Assertions (True) = 14/18
ICRA Assertions (False) = 1/1
ICRA Time = 308.981
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below 1 PASS0.376
bhmr2007_true-unreach-call.c below 1 PASS0.386
cggmp2005b_true-unreach-call.c below 1 PASS0.493
cggmp2005_true-unreach-call.c below 1 PASS0.333
cggmp2005_variant_true-unreach-call.c below 1 PASS0.351
css2003_true-unreach-call.c below 1 PASS0.778
ddlm2013_true-unreach-call.c below 1 PASS0.502
gcnr2008_false-unreach-call.c below 1 OKAY0.881
gj2007b_true-unreach-call.c below 1 FAIL0.371
gj2007_true-unreach-call.c below 1 PASS0.433
gr2006_true-unreach-call.c below 1 PASS0.426
gsv2008_true-unreach-call.c below 1 PASS0.332
hhk2008_true-unreach-call.c below 1 PASS0.333
jm2006_true-unreach-call.c below 1 PASS0.401
jm2006_variant_true-unreach-call.c below 1 PASS0.459
mcmillan2006_true-unreach-call.c below 1 FAIL0.391
ICRA Assertions (True) = 13/15
ICRA Assertions (False) = 1/1
ICRA Time = 7.246
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below 1 PASS0.32
count_by_1_variant_true-unreach-call.c below 1 PASS0.363
count_by_2_true-unreach-call.c below 1 PASS0.32
count_by_k_true-unreach-call.c below 1 PASS0.336
count_by_nondet_true-unreach-call.c below 1 FAIL0.355
gauss_sum_true-unreach-call.c below 1 PASS0.366
half_true-unreach-call.c below 1 FAIL0.357
nested_true-unreach-call.c below 1 PASS0.434
ICRA Assertions (True) = 6/8
ICRA Assertions (False) = 0/0
ICRA Time = 2.851
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below 1 OKAY0.366
array_true-unreach-call.c below 1 FAIL0.374
bubble_sort_false-unreach-call.c below 4 OKAY47.656
bubble_sort_true-unreach-call.c below 1 PASS3.625
compact_false-unreach-call.c below 1 OKAY0.397
count_up_down_false-unreach-call_true-termination.c below 1 OKAY0.339
count_up_down_true-unreach-call_true-termination.c below 1 PASS0.339
eureka_01_false-unreach-call.c below 1 OKAY2.131
eureka_01_true-unreach-call.c below 1 FAIL1.4
eureka_05_true-unreach-call.c below TIMEOUT 300.006
for_bounded_loop1_false-unreach-call_true-termination.c below 1 OKAY0.334
for_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.306
for_infinite_loop_2_true-unreach-call_false-termination.c below 1 PASS0.308
heavy_false-unreach-call.c below 1 OKAY0.456
heavy_true-unreach-call.c below 1 PASS0.435
insertion_sort_false-unreach-call.c below 1 OKAY1.51
insertion_sort_true-unreach-call.c below 1 FAIL0.532
invert_string_false-unreach-call.c below 1 OKAY0.49
invert_string_true-unreach-call.c below 1 FAIL0.508
linear_sea.ch_true-unreach-call.c below 1 FAIL0.382
linear_search_false-unreach-call.c below 1 OKAY0.377
lu.cmp_true-unreach-call.c below 3 PASS15.249
ludcmp_false-unreach-call.c below 3 OKAY15.343
matrix_false-unreach-call_true-termination.c below 1 OKAY1.012
matrix_true-unreach-call_true-termination.c below 1 FAIL0.395
n.c11_true-unreach-call.c below 3 FAIL0.42
n.c24_false-unreach-call.c below 3 OKAY2.582
n.c40_true-unreach-call.c below 1 FAIL0.351
nec11_false-unreach-call.c below 1 OKAY0.354
nec20_false-unreach-call.c below 1 OKAY0.373
nec40_true-unreach-call.c below 1 FAIL0.362
string_false-unreach-call.c below 1 OKAY0.593
string_true-unreach-call.c below 1 FAIL0.629
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.332
sum01_false-unreach-call_true-termination.c below 1 OKAY0.456
sum01_true-unreach-call_true-termination.c below 1 PASS0.357
sum03_false-unreach-call_true-termination.c below 1 OKAY0.472
sum03_true-unreach-call_false-termination.c below 1 PASS0.435
sum04_false-unreach-call_true-termination.c below 1 OKAY0.451
sum04_true-unreach-call_true-termination.c below 1 PASS0.342
sum_array_false-unreach-call.c below 1 OKAY0.565
sum_array_true-unreach-call.c below 1 FAIL0.646
terminator_01_false-unreach-call_false-termination.c below 1 OKAY0.327
terminator_02_false-unreach-call_true-termination.c below 2 OKAY0.421
terminator_02_true-unreach-call_true-termination.c below 2 PASS0.354
terminator_03_false-unreach-call_true-termination.c below 1 OKAY0.329
terminator_03_true-unreach-call_true-termination.c below 1 PASS0.325
trex01_false-unreach-call_true-termination.c below 3 OKAY0.431
trex01_true-unreach-call.c below 3 PASS0.689
trex02_false-unreach-call_true-termination.c below 2 OKAY0.373
trex02_true-unreach-call_true-termination.c below 2 PASS0.384
trex03_false-unreach-call_true-termination.c below 2 OKAY0.57
trex03_true-unreach-call.c below 2 PASS0.55
trex04_true-unreach-call_false-termination.c below 1 PASS0.377
veris.c_NetBSD-libc__loop_true-unreach-call.c below 1 PASS0.357
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below 3 PASS5.294
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below 1 PASS0.357
verisec_NetBSD-libc__loop_false-unreach-call.c below 1 OKAY0.357
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below 3 OKAY3.793
vogal_false-unreach-call.c below 1 OKAY0.735
vogal_true-unreach-call.c below 1 FAIL0.752
while_infinite_loop_1_true-unreach-call_false-termination.c below 1 PASS0.287
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.325
while_infinite_loop_4_false-unreach-call_true-termination.c below 1 OKAY0.304
ICRA Assertions (True) = 21/34
ICRA Assertions (False) = 32/32
ICRA Time = 422.593
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below 7 PASS0.93
Ackermann02_false-unreach-call_false-termination.c below 7 OKAY0.892
Ackermann03_true-unreach-call.c below 7 FAIL0.937
Ackermann04_true-unreach-call.c below 7 FAIL0.946
Addition01_true-unreach-call_true-termination.c below 2 PASS0.524
Addition02_false-unreach-call_false-termination.c below 2 OKAY0.526
Addition03_false-no-overflow.c below 2 PASS0.529
Addition03_true-unreach-call.c below 2 PASS0.532
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below 2 OKAY0.461
EvenOdd01_true-unreach-call_true-termination.c below 2 PASS0.408
EvenOdd03_false-unreach-call_false-termination.c below 2 OKAY0.409
Fibonacci01_true-unreach-call.c below 7 FAIL0.729
Fibonacci02_true-unreach-call_true-termination.c below 7 FAIL0.685
Fibonacci03_true-unreach-call_true-termination.c below 7 FAIL0.713
Fibonacci04_false-unreach-call_true-termination.c below 7 OKAY0.685
Fibonacci05_false-unreach-call_true-termination.c below 7 OKAY0.698
gcd01_true-unreach-call_true-termination.c below 2 PASS0.535
gcd02_true-unreach-call.c below 2 FAIL0.929
McCarthy91_false-unreach-call_false-termination.c below 4 OKAY0.568
McCarthy91_true-unreach-call.c below 4 PASS0.525
MultCommutative_true-unreach-call_true-termination.c below 2 FAIL0.547
Primes_true-unreach-call.c below 2 FAIL1.199
recHanoi01_true-unreach-call_true-termination.c below 8 FAIL1.621
recHanoi02_true-unreach-call_true-termination.c below 2 FAIL0.377
recHanoi03_true-unreach-call_true-termination.c below 2 FAIL0.382
ICRA Assertions (True) = 7/18
ICRA Assertions (False) = 7/7
ICRA Time = 17.287
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below 2 OKAY0.416
afterrec_2calls_true-unreach-call.c below 2 PASS0.39
afterrec_false-unreach-call.c below 2 OKAY0.374
afterrec_true-unreach-call.c below 2 PASS0.367
fibo_10_false-unreach-call.c below 7 OKAY0.726
fibo_10_true-unreach-call.c below 7 FAIL0.67
fibo_15_false-unreach-call.c below 7 OKAY0.705
fibo_15_true-unreach-call.c below 7 FAIL0.712
fibo_20_false-unreach-call.c below 7 OKAY0.691
fibo_20_true-unreach-call.c below 7 FAIL0.691
fibo_25_false-unreach-call.c below 7 OKAY0.705
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.009
fibo_2calls_15_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_15_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_20_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_20_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_25_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_25_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_2_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_2_true-unreach-call.c below TIMEOUT 300.014
fibo_2calls_4_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_4_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_5_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_5_true-unreach-call.c below TIMEOUT 300.013
fibo_2calls_6_false-unreach-call.c below TIMEOUT 300.012
fibo_2calls_6_true-unreach-call.c below TIMEOUT 300.012
fibo_2calls_8_false-unreach-call.c below TIMEOUT 300.013
fibo_2calls_8_true-unreach-call.c below TIMEOUT 300.013
fibo_5_false-unreach-call.c below 7 OKAY0.703
fibo_5_true-unreach-call.c below 7 FAIL0.682
fibo_7_false-unreach-call.c below 7 OKAY0.728
fibo_7_true-unreach-call.c below 7 FAIL0.707
id2_b2_o3_true-unreach-call.c below 2 PASS0.616
id2_b3_o2_false-unreach-call.c below 2 OKAY0.639
id2_b3_o5_true-unreach-call.c below 2 PASS0.593
id2_b5_o10_true-unreach-call.c below 2 PASS0.597
id2_i5_o5_false-unreach-call.c below 2 OKAY0.401
id2_i5_o5_true-unreach-call.c below 2 PASS0.399
id_b2_o3_true-unreach-call.c below 2 PASS0.546
id_b3_o2_false-unreach-call.c below 2 OKAY0.546
id_b3_o5_true-unreach-call.c below 2 PASS0.539
id_b5_o10_true-unreach-call.c below 2 PASS0.544
id_i10_o10_false-unreach-call.c below 2 OKAY0.377
id_i10_o10_true-unreach-call.c below 2 PASS0.379
id_i15_o15_false-unreach-call.c below 2 OKAY0.366
id_i15_o15_true-unreach-call.c below 2 PASS0.37
id_i20_o20_false-unreach-call.c below 2 OKAY0.367
id_i20_o20_true-unreach-call.c below 2 PASS0.373
id_i25_o25_false-unreach-call.c below 2 OKAY0.383
id_i25_o25_true-unreach-call.c below 2 PASS0.363
id_i5_o5_false-unreach-call.c below 2 OKAY0.374
id_i5_o5_true-unreach-call.c below 2 PASS0.37
id_o1000_false-unreach-call.c below 2 OKAY0.368
id_o100_false-unreach-call.c below 2 OKAY0.368
id_o10_false-unreach-call.c below 2 OKAY0.356
id_o200_false-unreach-call.c below 2 OKAY0.385
id_o20_false-unreach-call.c below 2 OKAY0.37
id_o3_false-unreach-call.c below 2 OKAY0.384
sum_10x0_false-unreach-call.c below 2 OKAY0.413
sum_10x0_true-unreach-call.c below 2 PASS0.405
sum_15x0_false-unreach-call.c below 2 OKAY0.403
sum_15x0_true-unreach-call.c below 2 PASS0.403
sum_20x0_false-unreach-call.c below 2 OKAY0.4
sum_20x0_true-unreach-call.c below 2 PASS0.425
sum_25x0_false-unreach-call.c below 2 OKAY0.412
sum_25x0_true-unreach-call.c below 2 PASS0.405
sum_2x3_false-unreach-call.c below 2 OKAY0.39
sum_2x3_true-unreach-call.c below 2 PASS0.396
sum_non_eq_false-unreach-call.c below 2 OKAY0.418
sum_non_eq_true-unreach-call.c below 2 PASS0.4
sum_non_false-unreach-call.c below 2 OKAY0.42
sum_non_true-unreach-call.c below 2 PASS0.398
ICRA Assertions (True) = 21/36
ICRA Assertions (False) = 29/38
ICRA Time = 5427.245
/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.426
rec-bhmr2007_true-unreach-call.c below 2 PASS0.409
rec-cggmp2005b_true-unreach-call.c below 2 PASS0.513
rec-cggmp2005_true-unreach-call.c below 2 PASS0.372
rec-cggmp2005_variant_true-unreach-call.c below 2 PASS0.401
rec-css2003_true-unreach-call.c below 2 PASS0.965
rec-ddlm2013_true-unreach-call.c below 2 FAIL1.071
rec-gcnr2008_false-unreach-call.c below 2 OKAY0.755
rec-gj2007b_true-unreach-call.c below 2 FAIL0.378
rec-gj2007_true-unreach-call.c below 2 FAIL0.461
rec-gr2006_true-unreach-call.c below 2 FAIL0.492
rec-gsv2008_true-unreach-call.c below 2 PASS0.439
rec-hhk2008_true-unreach-call.c below 2 PASS0.382
rec-jm2006_true-unreach-call.c below 2 PASS0.454
rec-jm2006_variant_true-unreach-call.c below 2 PASS0.482
rec-mcmillan2006_true-unreach-call.c below 2 FAIL0.421
ICRA Assertions (True) = 10/15
ICRA Assertions (False) = 1/1
ICRA Time = 8.421
/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.356
rec-count_by_1_variant_true-unreach-call.c below 2 PASS0.392
rec-count_by_2_true-unreach-call.c below 2 PASS0.359
rec-count_by_k_true-unreach-call.c below 2 PASS0.382
rec-count_by_nondet_true-unreach-call.c below 2 FAIL0.41
rec-gauss_sum_true-unreach-call.c below 2 PASS0.412
rec-half_true-unreach-call.c below 2 FAIL0.396
rec-nested_true-unreach-call.c below 3 FAIL0.524
ICRA Assertions (True) = 5/8
ICRA Assertions (False) = 0/0
ICRA Time = 3.231
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below 2 PASS0.483
cubic_polynomial_unsafe.c below 2 OKAY0.52
edit_distance_bottom_up.c below 3 FAIL116.458
edit_distance_top_down.c below 3 FAIL2.63
log_log_n_solution.c below 2 FAIL0.412
log_log_n_solution_unsafe.c below 2 OKAY0.389
log_n_solution.c below 2 FAIL0.436
log_n_solution_unsafe.c below 2 OKAY0.441
multivariate_1.c below TIMEOUT 300.004
multivariate_1_unsafe.c below TIMEOUT 300.005
multivariate_higher_order.c below 2 PASS0.783
multivariate_higher_order_unsafe.c below 2 UNSOUND0.784
n_cubed_solution.c below EXCEPTION 0.394
n_cubed_solution_unsafe.c below EXCEPTION 0.025
n_log_n_solution.c below 2 PASS0.511
n_log_n_solution_unsafe.c below 2 UNSOUND0.506
n_squared_two_base_case_even.c below 2 PASS0.478
n_squared_two_base_case_even_unsafe.c below 2 OKAY0.486
n_squared_two_base_case_odd.c below 2 PASS0.492
n_squared_two_base_case_odd_unsafe.c below 2 OKAY0.485
pascals_dynamic.c below 3 FAIL2.479
pascals_dynamic_unsafe.c below 3 OKAY2.462
pascals_iterative.c below 1 FAIL3.368
pascals_iterative_unsafe.c below 1 OKAY3.446
pascals_recursive.c below 8 FAIL8.047
pascals_recursive_unsafe.c below 8 OKAY8.096
squared_solution.c below 2 PASS0.537
squared_solution_unsafe.c below 2 UNSOUND0.536
two_n_even.c below 2 PASS0.386
two_n_even_unsafe.c below 2 OKAY0.396
two_n_odd.c below 2 PASS0.386
two_n_odd_unsafe.c below 2 OKAY0.392
two_to_n_over_two_even.c below 2 PASS0.415
two_to_n_over_two_even_unsafe.c below 2 UNSOUND0.427
two_to_n_over_two_odd.c below 2 PASS0.42
two_to_n_over_two_odd_unsafe.c below 2 UNSOUND0.43
two_to_n_squared.c below 8 FAIL16.914
two_to_n_squared_unsafe.c below 8 OKAY17.047
two_to_two_to_n.c below 2 PASS0.458
two_to_two_to_n_unsafe.c below 2 UNSOUND0.456
ICRA Assertions (True) = 11/21
ICRA Assertions (False) = 11/19
ICRA Time = 793.82
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below 1 PASS0.359
adding_and_mult_unsafe.c below 1 OKAY0.374
binary_search_array_tree.c below 1 FAIL0.601
exp_add_linear.c below 1 PASS0.411
exp_add_linear_unsafe.c below 1 OKAY0.422
exp_add_loop_rec.c below 1 FAIL0.352
exp_add_loop_rec_unsafe.c below 1 OKAY0.355
exp_add_loop_variable.c below 1 PASS0.396
exp_add_loop_variable_unsafe.c below 1 OKAY0.42
exp_with_linear_inner_loop.c below 1 FAIL0.479
exp_with_linear_inner_loop_unsafe.c below 1 OKAY0.488
halving_log1.c below 1 FAIL0.479
linear_two_to_n.c below 2 FAIL0.466
linear_two_to_n_unsafe.c below 2 OKAY0.451
loop_five_to_n.c below 1 PASS0.392
loop_five_to_n_unsafe.c below 1 OKAY0.394
non_loop_five_to_n.c below 2 FAIL0.658
non_loop_five_to_n_unsafe.c below 2 OKAY0.652
power_log.c below 1 PASS0.451
power_log_modified.c below 1 PASS0.493
simple_exponential.c below 1 PASS0.385
simple_exponential_for.c below 1 PASS0.382
simple_exponential_for_unsafe.c below 1 OKAY0.395
simple_exponential_unsafe.c below 1 OKAY0.402
two_to_n_minus_n.c below 2 FAIL0.494
two_to_n_minus_n_loop.c below 9 FAIL2.081
two_to_n_minus_n_loop_unsafe.c below 9 OKAY2.047
two_to_n_minus_n_unsafe.c below 2 OKAY0.492
ICRA Assertions (True) = 8/16
ICRA Assertions (False) = 12/12
ICRA Time = 15.771