[Version Information]
Phase2 (IST-Java-ICRA) WALi-OpenNWA version: cb66c5d81a7461250a11c7d2e8f839a3ac4b693b (2017-06-01 11:48:21 -0500) "Allow full_icra_rebuild.sh to work with both NewtonICRA duet and Newton-ark2 duet."
Phase2 (IST-Java-ICRA) duet version: 393b2fa15ae67d4cf44b9a72bd4e0c54307ef649 (2017-05-16 13:07:27 -0400) "Updated the costs for thread.sleep from 10 to 1000"

Phase3 WALi-OpenNWA version: cb66c5d81a7461250a11c7d2e8f839a3ac4b693b (2017-06-01 11:48:21 -0500) "Allow full_icra_rebuild.sh to work with both NewtonICRA duet and Newton-ark2 duet."
Phase3 duet version: 3f3626cb91d25fac166f7330b2ef6994712067de (2017-06-14 18:23:52 -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
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 Time (Prev.)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c [OCRS][without] 1 FAIL
0.391
kmp.c [OCRS][without] 1 PASS
1.421 (1.183)
qsort.c [OCRS][without] 5 PASS
3.73 (2.145)
speed_pldi09_fig1.c [OCRS][without] 1 PASS
0.39
speed_pldi09_fig4_2.c [OCRS][without] 1 FAIL
0.41
speed_pldi09_fig4_4.c [OCRS][without] 1 PASS
0.484
speed_pldi09_fig4_5.c [OCRS][without] 1 PASS
0.404
speed_pldi10_ex1.c [OCRS][without] 1 PASS
4.019 (0.863)
speed_pldi10_ex3.c [OCRS][without] 1 PASS
0.485
speed_pldi10_ex4.c [OCRS][without] EXCEPTION
0.442
speed_popl10_fig2_1.c [OCRS][without] 1 PASS
0.405
speed_popl10_fig2_2.c [OCRS][without] 1 FAIL
0.381
speed_popl10_nested_multiple.c [OCRS][without] 1 PASS
0.461
speed_popl10_nested_single.c [OCRS][without] 1 PASS
0.404
speed_popl10_sequential_single.c [OCRS][without] 1 PASS
0.356
speed_popl10_simple_multiple.c [OCRS][without] 1 PASS
0.407
speed_popl10_simple_single_2.c [OCRS][without] 1 PASS
0.42
speed_popl10_simple_single.c [OCRS][without] 1 PASS
0.345
t07.c [OCRS][without] 1 PASS
0.37
t08.c [OCRS][without] 1 PASS
0.363
t09.c [OCRS][without] 1 PASS
0.386
t10.c [OCRS][without] 1 PASS
0.376
t11.c [OCRS][without] 1 PASS
0.412
t13.c [OCRS][without] 1 FAIL
0.432
t15.c [OCRS][without] 1 PASS
0.406
t16.c [OCRS][without] 1 PASS
0.399
t19.c [OCRS][without] 1 PASS
0.386
t20.c [OCRS][without] 1 PASS
0.363
t27.c [OCRS][without] 1 PASS
0.438
t28.c [OCRS][without] 1 PASS
0.433
t30.c [OCRS][without] 1 FAIL
0.367
t37.c [OCRS][without] 2 PASS
0.526
t39.c [OCRS][without] 2 PASS
0.497
t46.c [OCRS][without] 1 PASS
0.385
t47.c [OCRS][without] 1 PASS
0.4
Total Below Time = 22.294 (was 16.899)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c [OCRS][without] 2 PASS
PASS
0.39
qsort_full.c [OCRS][without] 5 TIMEOUT
300.006 (43.516)
rec1-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.371
rec1-param_unsafe.c [OCRS][without] 2 PASS
0.379
rec1_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.362
rec1_unsafe.c [OCRS][without] 2 PASS
0.353
rec2-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.35
rec2-param_unsafe.c [OCRS][without] 2 PASS
0.359
rec2_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.359
rec2_unsafe.c [OCRS][without] 2 PASS
0.345
rec-test.c [OCRS][without] 2 PASS
0.363
sas03_bothbranches.c [OCRS][without] 7 PASS
1.323
sas03.c [OCRS][without] 2 PASS
0.849
simulated_lese_recursive.c [OCRS][without] 2 PASS
0.417
Total Below Time = 306.226 (was 49.643)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c [OCRS][without] 1 PASS
0.347
count_up_down_unsafe.c [OCRS][without] 1 PASS
0.338
divide.c [OCRS][without] 1 PASS
0.345
factor_unsafe.c [OCRS][without] 1 PASS
0.355
for_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.329
for_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.321
interproc.c [OCRS][without] 1 PASS
0.34
mult.c [OCRS][without] 1 PASS
PASS
0.348
pointer_arith.c [OCRS][without] 1 PASS
PASS
PASS
PASS
0.325
quotient.c [OCRS][without] 3 PASS
0.44
subtract.c [OCRS][without] 1 PASS
0.342
sum01_bug02_sum01_bug02_base.case_unsafe.c [OCRS][without] 1 PASS
0.357
sum01_bug02_unsafe.c [OCRS][without] 1 PASS
0.391
sum01_real_safe.c [OCRS][without] 1 PASS
0.338
sum01_safe.c [OCRS][without] 1 PASS
0.349
sum01_unsafe.c [OCRS][without] 1 PASS
0.384
sum02_safe.c [OCRS][without] 1 PASS
0.329
sum03_safe.c [OCRS][without] 1 PASS
0.353
sum03_unsafe.c [OCRS][without] 1 PASS
0.417
sum04_safe.c [OCRS][without] 1 PASS
0.333
sum04_unsafe.c [OCRS][without] 1 PASS
0.389
terminator_02_safe.c [OCRS][without] 1 PASS
0.351
terminator_02_unsafe.c [OCRS][without] 1 PASS
0.363
terminator_03_safe.c [OCRS][without] 1 PASS
0.351
terminator_03_unsafe.c [OCRS][without] 1 PASS
0.354
token_ring01_safe.c [OCRS][without] TIMEOUT
300.008
token_ring01_unsafe.c [OCRS][without] TIMEOUT
300.008
toy_safe.c [OCRS][without] EXCEPTION
209.077
trex01_safe.c [OCRS][without] 1 PASS
0.58
trex01_unsafe.c [OCRS][without] 1 PASS
0.372
trex02_safe2.c [OCRS][without] 3 PASS
0.415
trex02_safe.c [OCRS][without] 3 PASS
0.411
trex02_unsafe.c [OCRS][without] 3 PASS
0.408
trex03_safe.c [OCRS][without] 1 PASS
0.493
trex03_unsafe.c [OCRS][without] 1 PASS
0.479 (0.428)
trex04_safe.c [OCRS][without] 1 PASS
0.371
while_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.34
while_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.343
while_infinite_loop_3_safe.c [OCRS][without] 1 PASS
0.328
Total Below Time = 822.522 (was 810.402)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c [OCRS][without] 3 PASS
0.474
blogger_simplified1.c [OCRS][without] 3 PASS
0.988
divided_difference2.c [OCRS][without] TIMEOUT
300.006
mult-proc.c [OCRS][without] 3 PASS
PASS
0.39
mult-proc-params.c [OCRS][without] 3 PASS
PASS
0.441
popall.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
0.437
simulated_scc.c [OCRS][without] 1 PASS
PASS
0.575 (0.497)
Total Below Time = 303.311 (was 303.193)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c [OCRS][without] 1 PASS
0.368
degree2_binomial.c [OCRS][without] 1 PASS
0.501
degree2_monomial.c [OCRS][without] 1 PASS
0.37 (0.416)
degree3_binomial.c [OCRS][without] 1 PASS
0.909
degree3_monomial.c [OCRS][without] 1 PASS
0.446
degree4_binomial.c [OCRS][without] 1 PASS
1.249 (1.121)
degree4_monomial.c [OCRS][without] 1 PASS
0.522
degree5_binomial.c [OCRS][without] 1 PASS
1.887
degree5_monomial.c [OCRS][without] 1 PASS
0.569
Total Below Time = 6.821 (was 6.872)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c [OCRS][without] 1 PASS
0.365
cubic_with_square_interproc.c [OCRS][without] 2 PASS
0.385
cubic_with_square_nonlinear.c [OCRS][without] 1 PASS
0.38
cubic_with_square_nonlinear_interproc.c [OCRS][without] 2 PASS
0.389
cubic_with_square_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.369
cubic_with_square_unsafe.c [OCRS][without] 1 PASS
0.368
multi-input.c [OCRS][without] 1 PASS
0.415
multi-input_unsafe.c [OCRS][without] 1 PASS
0.466 (0.529)
nondet_loop_bound.c [OCRS][without] 1 PASS
0.383
nondet_loop_bound_quartic.c [OCRS][without] 1 PASS
0.392 (0.351)
nondet_loop_bound_quartic_unsafe.c [OCRS][without] 1 PASS
0.379
nondet_loop_bound_unsafe.c [OCRS][without] 1 PASS
0.388
nonlinear_stratified.c [OCRS][without] 1 FAIL
0.387
nonlinear_stratified_unsafe.c [OCRS][without] 1 PASS
0.383
quartic_with_cube.c [OCRS][without] 1 PASS
0.361
quartic_with_cube_nonlinear.c [OCRS][without] 1 PASS
0.377
quartic_with_cube_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.357
quartic_with_cube_unsafe.c [OCRS][without] 1 PASS
0.386
quintic_with_quartic.c [OCRS][without] 1 PASS
0.377
quintic_with_quartic_nonlinear.c [OCRS][without] 1 PASS
0.392
quintic_with_quartic_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.398 (0.476)
quintic_with_quartic_unsafe.c [OCRS][without] 1 PASS
0.389
Total Below Time = 8.486 (was 8.54)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c [OCRS][without] 1 PASS
0.541
degree2_FD_AllAux_AllAssm.c [OCRS][without] 1 PASS
3.774 (3.279)
degree2_FD_AllAux_FewAssm.c [OCRS][without] 1 PASS
5.708 (3.314)
degree2_FD_FewAux_FewAssm.c [OCRS][without] 1 PASS
0.722
degree2_FD_FewAux_FewAssm_NonLinAsrt.c [OCRS][without] 1 PASS
0.75
degree3.c [OCRS][without] 1 PASS
0.565
degree3_FD.c [OCRS][without] 1 PASS
0.752
degree4.c [OCRS][without] 1 PASS
0.413
Total Below Time = 13.225 (was 10.325)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c [OCRS][without] 1 PASS
0.393
loop_unsafe.c [OCRS][without] 1 PASS
0.419
simulated_lese_parser.c [OCRS][without] 1 PASS
0.351
simulated_lese_sentinel.c [OCRS][without] 1 PASS
0.366
Total Below Time = 1.529 (was 1.504)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c [OCRS][without] 1 PASS
PASS
PASS
0.375
Total Below Time = 0.375 (was 0.368)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c [OCRS][without] TIMEOUT
300.016
Total Below Time = 300.016 (was 300.008)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c [OCRS][without] 1 PASS
0.357
array_false-unreach-call2.c [OCRS][without] 1 PASS
0.38
array_false-unreach-call3.c [OCRS][without] 1 PASS
0.362 (0.328)
array_true-unreach-call1.c [OCRS][without] 1 FAIL
0.366
array_true-unreach-call2.c [OCRS][without] 1 FAIL
0.37
array_true-unreach-call3.c [OCRS][without] 1 PASS
0.355
array_true-unreach-call4.c [OCRS][without] 1 FAIL
0.35
const_false-unreach-call1.c [OCRS][without] 1 PASS
0.33
const_true-unreach-call1.c [OCRS][without] 1 PASS
0.322
diamond_false-unreach-call1.c [OCRS][without] 1 PASS
0.357
diamond_true-unreach-call1.c [OCRS][without] 1 PASS
0.346
diamond_true-unreach-call2.c [OCRS][without] 1 PASS
0.387
functions_false-unreach-call1.c [OCRS][without] 3 PASS
0.399
functions_true-unreach-call1.c [OCRS][without] 3 PASS
0.386
multivar_false-unreach-call1.c [OCRS][without] 1 PASS
0.329
multivar_true-unreach-call1.c [OCRS][without] 1 PASS
0.331
nested_false-unreach-call1.c [OCRS][without] 1 PASS
0.335
nested_true-unreach-call1.c [OCRS][without] 1 PASS
0.346
overflow_true-unreach-call1.c [OCRS][without] 1 PASS
0.329
phases_false-unreach-call1.c [OCRS][without] 1 PASS
0.35
phases_false-unreach-call2.c [OCRS][without] 1 PASS
0.359
phases_true-unreach-call1.c [OCRS][without] 1 PASS
0.343
phases_true-unreach-call2.c [OCRS][without] 1 PASS
0.356
simple_false-unreach-call1.c [OCRS][without] 1 PASS
0.327
simple_false-unreach-call2.c [OCRS][without] 1 PASS
0.328
simple_false-unreach-call3.c [OCRS][without] 1 PASS
0.344
simple_false-unreach-call4.c [OCRS][without] 1 PASS
0.338
simple_true-unreach-call1.c [OCRS][without] 1 PASS
0.334
simple_true-unreach-call2.c [OCRS][without] 1 PASS
0.342
simple_true-unreach-call3.c [OCRS][without] 1 PASS
0.344
simple_true-unreach-call4.c [OCRS][without] 1 PASS
0.344
underapprox_false-unreach-call1.c [OCRS][without] 1 PASS
0.331
underapprox_false-unreach-call2.c [OCRS][without] 1 PASS
0.345
underapprox_true-unreach-call1.c [OCRS][without] 1 FAIL
0.355
underapprox_true-unreach-call2.c [OCRS][without] 1 PASS
0.336
Total Below Time = 12.213 (was 12.404)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
0.909
apache-get-tag_true-unreach-call.c [OCRS][without] 1 PASS
PASS
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
0.466
down_true-unreach-call.c [OCRS][without] 1 PASS
0.353
fragtest_simple_true-unreach-call.c [OCRS][without] 1 PASS
0.393
half_2_true-unreach-call.c [OCRS][without] 1 PASS
0.37
heapsort_true-unreach-call.c [OCRS][without] 1 TIMEOUT
300.138 (2.522)
id_build_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.356
id_trans_false-unreach-call.c [OCRS][without] 1 FAIL
FAIL
FAIL
PASS
0.366
large_const_true-unreach-call.c [OCRS][without] 1 PASS
0.442
MADWiFi-encode_ie_ok_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.381
nested6_true-unreach-call.c [OCRS][without] 1 FAIL
FAIL
PASS
0.42
nested9_true-unreach-call.c [OCRS][without] 1 PASS
0.457
nest-if3_true-unreach-call.c [OCRS][without] 1 PASS
0.443
NetBSD_loop_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.361
sendmail-close-angle_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.397
seq_true-unreach-call.c [OCRS][without] 1 PASS
0.394
SpamAssassin-loop_true-unreach-call.c [OCRS][without] TIMEOUT
300.123 (1.288)
string_concat-noarr_true-unreach-call.c [OCRS][without] 1 PASS
0.384
up_true-unreach-call.c [OCRS][without] 1 PASS
0.374
Total Below Time = 607.527 (was 11.014)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c [OCRS][without] 1 PASS
0.367
bhmr2007_true-unreach-call.c [OCRS][without] 1 PASS
0.381
cggmp2005b_true-unreach-call.c [OCRS][without] 1 PASS
0.428 (0.381)
cggmp2005_true-unreach-call.c [OCRS][without] 1 PASS
0.342
cggmp2005_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.351
css2003_true-unreach-call.c [OCRS][without] 1 PASS
0.502
ddlm2013_true-unreach-call.c [OCRS][without] 1 PASS
0.396
gcnr2008_false-unreach-call.c [OCRS][without] 1 TIMEOUT
300.181 (0.908)
gj2007b_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
0.392
gj2007_true-unreach-call.c [OCRS][without] 1 PASS
0.375
gr2006_true-unreach-call.c [OCRS][without] 1 PASS
0.373
gsv2008_true-unreach-call.c [OCRS][without] 1 PASS
0.347
hhk2008_true-unreach-call.c [OCRS][without] 1 PASS
0.36
jm2006_true-unreach-call.c [OCRS][without] 1 PASS
0.389
jm2006_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.404
mcmillan2006_true-unreach-call.c [OCRS][without] 1 FAIL
0.401
Total Below Time = 305.989 (was 6.573)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c [OCRS][without] 1 PASS
0.346
count_by_1_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.347
count_by_2_true-unreach-call.c [OCRS][without] 1 PASS
0.312
count_by_k_true-unreach-call.c [OCRS][without] 1 PASS
0.335
count_by_nondet_true-unreach-call.c [OCRS][without] 1 FAIL
0.372
gauss_sum_true-unreach-call.c [OCRS][without] 1 PASS
0.376
half_true-unreach-call.c [OCRS][without] EXCEPTION
0.368
nested_true-unreach-call.c [OCRS][without] 1 PASS
0.422
Total Below Time = 2.878 (was 2.789)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c [OCRS][without] 1 PASS
0.437
array_true-unreach-call.c [OCRS][without] 1 FAIL
0.453
bubble_sort_false-unreach-call.c [OCRS][without] 4 PASS
PASS
199.077
bubble_sort_true-unreach-call.c [OCRS][without] 1 4.094
compact_false-unreach-call.c [OCRS][without] 1 PASS
0.359
count_up_down_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.341
count_up_down_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.355
eureka_01_false-unreach-call.c [OCRS][without] 1 PASS
2.387
eureka_01_true-unreach-call.c [OCRS][without] 1 FAIL
2.168
eureka_05_true-unreach-call.c [OCRS][without] 1 FAIL
1.099 (0.781)
for_bounded_loop1_false-unreach-call_true-termination.c [OCRS][without] 1 FAIL
FAIL
PASS
0.348
for_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.326
for_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.343
heavy_false-unreach-call.c [OCRS][without] 1 PASS
0.555
heavy_true-unreach-call.c [OCRS][without] 1 PASS
0.566
insertion_sort_false-unreach-call.c [OCRS][without] 1 PASS
2.393
insertion_sort_true-unreach-call.c [OCRS][without] 1 FAIL
0.796
invert_string_false-unreach-call.c [OCRS][without] 1 PASS
0.543
invert_string_true-unreach-call.c [OCRS][without] 1 FAIL
0.534
linear_sea.ch_true-unreach-call.c [OCRS][without] 1 FAIL
0.387
linear_search_false-unreach-call.c [OCRS][without] 1 EXCEPTION
0.41
lu.cmp_true-unreach-call.c [OCRS][without] TIMEOUT
300.261 (134.177)
ludcmp_false-unreach-call.c [OCRS][without] TIMEOUT
300.251 (133.385)
matrix_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
1.042 (0.851)
matrix_true-unreach-call_true-termination.c [OCRS][without] 1 FAIL
0.489
n.c11_true-unreach-call.c [OCRS][without] 3 FAIL
0.452
n.c24_false-unreach-call.c [OCRS][without] 3 PASS
25.401
n.c40_true-unreach-call.c [OCRS][without] 1 FAIL
0.395
nec11_false-unreach-call.c [OCRS][without] 1 PASS
0.407
nec20_false-unreach-call.c [OCRS][without] 1 PASS
0.401
nec40_true-unreach-call.c [OCRS][without] 1 FAIL
0.393
string_false-unreach-call.c [OCRS][without] 1 PASS
0.639
string_true-unreach-call.c [OCRS][without] 1 FAIL
0.645
sum01_bug02_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.413
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.341
sum01_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.381
sum01_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.348
sum03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.506
sum03_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.396
sum04_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.363
sum04_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.34
sum_array_false-unreach-call.c [OCRS][without] 1 PASS
0.656
sum_array_true-unreach-call.c [OCRS][without] 1 FAIL
0.731
terminator_01_false-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.342
terminator_02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.447
terminator_02_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.341
terminator_03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.326
terminator_03_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.344
trex01_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.493
trex01_true-unreach-call.c [OCRS][without] 3 PASS
0.827 (0.72)
trex02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.414
trex02_true-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.405
trex03_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.906
trex03_true-unreach-call.c [OCRS][without] 3 PASS
0.837
trex04_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.384
veris.c_NetBSD-libc__loop_true-unreach-call.c [OCRS][without] 1 PASS
0.346
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c [OCRS][without] 3 26.381
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c [OCRS][without] 1 PASS
0.359
verisec_NetBSD-libc__loop_false-unreach-call.c [OCRS][without] 1 PASS
0.371
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c [OCRS][without] 3 PASS
18.464
vogal_false-unreach-call.c [OCRS][without] 1 PASS
0.911 (0.811)
vogal_true-unreach-call.c [OCRS][without] 1 FAIL
0.936 (0.8)
while_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.306
while_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.319
while_infinite_loop_3_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.327
while_infinite_loop_4_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.334
Total Below Time = 908.342 (was 558.066)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c [OCRS][without] TIMEOUT
300.034 (2.608)
Ackermann02_false-unreach-call_false-termination.c [OCRS][without] TIMEOUT
300.032 (2.537)
Ackermann03_true-unreach-call.c [OCRS][without] TIMEOUT
300.029 (2.68)
Ackermann04_true-unreach-call.c [OCRS][without] TIMEOUT
300.032 (2.635)
Addition01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.59
Addition02_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.596
Addition03_false-no-overflow.c [OCRS][without] 2 PASS
0.62
Addition03_true-unreach-call.c [OCRS][without] 2 PASS
0.616
BallRajamani-SPIN2000-Fig1_false-unreach-call.c [OCRS][without] 2 PASS
0.485
EvenOdd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.463
EvenOdd03_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.452
Fibonacci01_true-unreach-call.c [OCRS][without] EXCEPTION
1.015 (300.009)
Fibonacci02_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.973 (300.01)
Fibonacci03_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
1.061 (300.007)
Fibonacci04_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
1.02 (300.011)
Fibonacci05_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
1.043 (300.009)
gcd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.549
gcd02_true-unreach-call.c [OCRS][without] 2 FAIL
PASS
1.504 (1.221)
McCarthy91_false-unreach-call_false-termination.c [OCRS][without] 7 PASS
1.547 (1.252)
McCarthy91_true-unreach-call.c [OCRS][without] 7 FAIL
1.495 (1.187)
MultCommutative_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.753 (0.625)
Primes_true-unreach-call.c [OCRS][without] 3 FAIL
2.263
recHanoi01_true-unreach-call_true-termination.c [OCRS][without] 9 FAIL
6.459
recHanoi02_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.411
recHanoi03_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.409
Total Below Time = 1224.451 (was 1528.304)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c [OCRS][without] 2 PASS
PASS
0.435
afterrec_2calls_true-unreach-call.c [OCRS][without] 2 PASS
PASS
0.407
afterrec_false-unreach-call.c [OCRS][without] 2 PASS
0.364
afterrec_true-unreach-call.c [OCRS][without] 2 PASS
0.355
fibo_10_false-unreach-call.c [OCRS][without] EXCEPTION
1.055 (300.008)
fibo_10_true-unreach-call.c [OCRS][without] EXCEPTION
0.981 (300.011)
fibo_15_false-unreach-call.c [OCRS][without] EXCEPTION
1.054 (300.01)
fibo_15_true-unreach-call.c [OCRS][without] EXCEPTION
1.011 (300.01)
fibo_20_false-unreach-call.c [OCRS][without] EXCEPTION
1.048 (300.01)
fibo_20_true-unreach-call.c [OCRS][without] EXCEPTION
1.03 (300.004)
fibo_25_false-unreach-call.c [OCRS][without] EXCEPTION
1.009 (300.01)
fibo_25_true-unreach-call.c [OCRS][without] EXCEPTION
0.962 (300.011)
fibo_2calls_10_false-unreach-call.c [OCRS][without] EXCEPTION
18.404 (139.028)
fibo_2calls_10_true-unreach-call.c [OCRS][without] EXCEPTION
18.022 (139.216)
fibo_2calls_15_false-unreach-call.c [OCRS][without] EXCEPTION
18.215 (133.63)
fibo_2calls_15_true-unreach-call.c [OCRS][without] EXCEPTION
18.159 (137.343)
fibo_2calls_20_false-unreach-call.c [OCRS][without] EXCEPTION
17.987 (142.005)
fibo_2calls_20_true-unreach-call.c [OCRS][without] EXCEPTION
18.195 (140.769)
fibo_2calls_25_false-unreach-call.c [OCRS][without] EXCEPTION
18.118 (133.656)
fibo_2calls_25_true-unreach-call.c [OCRS][without] EXCEPTION
18.289 (138.094)
fibo_2calls_2_false-unreach-call.c [OCRS][without] EXCEPTION
18.013 (138.163)
fibo_2calls_2_true-unreach-call.c [OCRS][without] EXCEPTION
18.269 (140.451)
fibo_2calls_4_false-unreach-call.c [OCRS][without] EXCEPTION
18.102 (135.673)
fibo_2calls_4_true-unreach-call.c [OCRS][without] EXCEPTION
18.049 (141.011)
fibo_2calls_5_false-unreach-call.c [OCRS][without] EXCEPTION
18.193 (139.813)
fibo_2calls_5_true-unreach-call.c [OCRS][without] EXCEPTION
18.253 (138.462)
fibo_2calls_6_false-unreach-call.c [OCRS][without] EXCEPTION
18.183 (134.707)
fibo_2calls_6_true-unreach-call.c [OCRS][without] EXCEPTION
18.278 (137.022)
fibo_2calls_8_false-unreach-call.c [OCRS][without] EXCEPTION
18.05 (138.331)
fibo_2calls_8_true-unreach-call.c [OCRS][without] EXCEPTION
18.01 (138.644)
fibo_5_false-unreach-call.c [OCRS][without] EXCEPTION
0.992 (300.009)
fibo_5_true-unreach-call.c [OCRS][without] EXCEPTION
0.997 (300.011)
fibo_7_false-unreach-call.c [OCRS][without] EXCEPTION
0.998 (300.01)
fibo_7_true-unreach-call.c [OCRS][without] EXCEPTION
0.986 (300.01)
id2_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.988
id2_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
1.031
id2_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.99
id2_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
1.02
id2_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.469
id2_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.427
id_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.614
id_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.582
id_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.587
id_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.586
id_i10_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.39
id_i10_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.385
id_i15_o15_false-unreach-call.c [OCRS][without] 2 PASS
0.39
id_i15_o15_true-unreach-call.c [OCRS][without] 2 PASS
0.385
id_i20_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.375
id_i20_o20_true-unreach-call.c [OCRS][without] 2 PASS
0.379
id_i25_o25_false-unreach-call.c [OCRS][without] 2 PASS
0.374
id_i25_o25_true-unreach-call.c [OCRS][without] 2 PASS
0.393
id_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.403
id_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.399
id_o1000_false-unreach-call.c [OCRS][without] 2 PASS
0.383
id_o100_false-unreach-call.c [OCRS][without] 2 PASS
0.391
id_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.387
id_o200_false-unreach-call.c [OCRS][without] 2 PASS
0.406
id_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.396
id_o3_false-unreach-call.c [OCRS][without] 2 PASS
0.395
sum_10x0_false-unreach-call.c [OCRS][without] 2 PASS
0.413
sum_10x0_true-unreach-call.c [OCRS][without] 2 PASS
0.405
sum_15x0_false-unreach-call.c [OCRS][without] 2 PASS
0.41
sum_15x0_true-unreach-call.c [OCRS][without] 2 PASS
0.39
sum_20x0_false-unreach-call.c [OCRS][without] 2 PASS
0.429
sum_20x0_true-unreach-call.c [OCRS][without] 2 PASS
0.399
sum_25x0_false-unreach-call.c [OCRS][without] 2 PASS
0.405
sum_25x0_true-unreach-call.c [OCRS][without] 2 PASS
0.407
sum_2x3_false-unreach-call.c [OCRS][without] 2 PASS
0.41
sum_2x3_true-unreach-call.c [OCRS][without] 2 PASS
0.399
sum_non_eq_false-unreach-call.c [OCRS][without] 2 PASS
0.436
sum_non_eq_true-unreach-call.c [OCRS][without] 2 PASS
0.447
sum_non_false-unreach-call.c [OCRS][without] 2 PASS
0.423
sum_non_true-unreach-call.c [OCRS][without] 2 PASS
0.42
Total Below Time = 359.791 (was 6107.06)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-lit
rec-afnp2014_true-unreach-call.c [OCRS][without] 2 PASS
0.389
rec-bhmr2007_true-unreach-call.c [OCRS][without] 2 PASS
0.437
rec-cggmp2005b_true-unreach-call.c [OCRS][without] 3 PASS
0.772
rec-cggmp2005_true-unreach-call.c [OCRS][without] 2 PASS
0.345
rec-cggmp2005_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.372
rec-css2003_true-unreach-call.c [OCRS][without] 2 PASS
0.638
rec-ddlm2013_true-unreach-call.c [OCRS][without] EXCEPTION
0.379 (0.495)
rec-gcnr2008_false-unreach-call.c [OCRS][without] 2 PASS
0.928
rec-gj2007b_true-unreach-call.c [OCRS][without] 2 FAIL
FAIL
0.411
rec-gj2007_true-unreach-call.c [OCRS][without] 2 FAIL
0.397
rec-gr2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.419
rec-gsv2008_true-unreach-call.c [OCRS][without] 2 PASS
0.372
rec-hhk2008_true-unreach-call.c [OCRS][without] 2 PASS
0.386
rec-jm2006_true-unreach-call.c [OCRS][without] 2 PASS
0.385
rec-jm2006_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.414
rec-mcmillan2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.436
Total Below Time = 7.48 (was 7.502)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c [OCRS][without] 2 PASS
0.355
rec-count_by_1_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.368
rec-count_by_2_true-unreach-call.c [OCRS][without] 2 PASS
0.355
rec-count_by_k_true-unreach-call.c [OCRS][without] 2 PASS
0.377
rec-count_by_nondet_true-unreach-call.c [OCRS][without] 2 FAIL
0.406
rec-gauss_sum_true-unreach-call.c [OCRS][without] 2 PASS
0.378
rec-half_true-unreach-call.c [OCRS][without] EXCEPTION
0.352 (0.43)
rec-nested_true-unreach-call.c [OCRS][without] 3 PASS
0.604
Total Below Time = 3.195 (was 3.292)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c [OCRS][without] 2 PASS
0.524
edit_distance_bottom_up.c [OCRS][without] 3 TIMEOUT
300.008
edit_distance_top_down.c [OCRS][without] 3 FAIL
53.133
log_log_n_solution.c [OCRS][without] 3 FAIL
0.472 (0.672)
log_n_solution.c [OCRS][without] 2 FAIL
0.473
multivariate_1.c [OCRS][without] TIMEOUT
300.007
multivariate_higher_order.c [OCRS][without] 7 FAIL
FAIL
FAIL
28.242
n_cubed_solution.c [OCRS][without] EXCEPTION
0.356
n_log_n_solution.c [OCRS][without] TIMEOUT
300.039 (1.912)
n_squared_two_base_case_even.c [OCRS][without] 2 PASS
0.423
n_squared_two_base_case_odd.c [OCRS][without] 2 PASS
0.393 (0.437)
pascals_dynamic.c [OCRS][without] 3 FAIL
20.963
pascals_iterative.c [OCRS][without] 1 FAIL
5.754 (6.555)
pascals_recursive.c [OCRS][without] TIMEOUT
300.007
squared_solution.c [OCRS][without] TIMEOUT
300.143 (12.913)
two_n_even.c [OCRS][without] 2 PASS
0.407
two_n_odd.c [OCRS][without] 2 PASS
0.377
two_to_n_over_two_even.c [OCRS][without] TIMEOUT
300.022 (48.22)
two_to_n_over_two_odd.c [OCRS][without] TIMEOUT
300.022 (46.799)
two_to_n_squared.c [OCRS][without] 8 TIMEOUT
300.006 (149.925)
two_to_two_to_n.c [OCRS][without] 7 FAIL
1.748
Total Below Time = 2513.519 (was 1274.923)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c [OCRS][without] 1 PASS
0.329
binary_search_array_tree.c [OCRS][without] 1 FAIL
FAIL
1.458 (0.693)
exp_add_loop_rec.c [OCRS][without] 1 FAIL
0.372
exp_add_loop_variable.c [OCRS][without] 1 PASS
0.364
exp_with_linear_inner_loop.c [OCRS][without] 1 FAIL
0.443
halving_log1.c [OCRS][without] 1 PASS
0.479 (0.415)
linear_two_to_n.c [OCRS][without] 8 FAIL
1.635 (1.453)
loop_five_to_n.c [OCRS][without] 1 FAIL
0.366
non_loop_five_to_n.c [OCRS][without] 8 FAIL
10.788 (9.423)
power_log.c [OCRS][without] 1 PASS
0.432
power_log_modified.c [OCRS][without] 1 PASS
0.499 (0.399)
simple_exponential.c [OCRS][without] 1 PASS
0.376
simple_exponential_for.c [OCRS][without] 1 PASS
0.362
two_to_n_minus_n.c [OCRS][without] 8 FAIL
1.876
two_to_n_minus_n_loop.c [OCRS][without] 8 FAIL
2.92
Total Below Time = 22.699 (was 20.038)

>25% better
25%-10% better
No significant change
10%-25% worse
>25% worse