[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: 305dceab9ebfebd6989a176ac545ef407610a0c8 (2017-06-15 22:27:52 -0400) "Fixed newton build target"
# 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               20170614  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 Time (Prev.)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c [OCRS][without] 1 FAIL
0.341
kmp.c [OCRS][without] 1 PASS
0.974 (0.833)
qsort.c [OCRS][without] 5 PASS
1.804 (1.118)
speed_pldi09_fig1.c [OCRS][without] 1 PASS
0.373
speed_pldi09_fig4_2.c [OCRS][without] 1 FAIL
0.368
speed_pldi09_fig4_4.c [OCRS][without] 1 PASS
0.412
speed_pldi09_fig4_5.c [OCRS][without] 1 PASS
0.35
speed_pldi10_ex1.c [OCRS][without] 1 PASS
3.238 (0.646)
speed_pldi10_ex3.c [OCRS][without] 1 PASS
0.409
speed_pldi10_ex4.c [OCRS][without] 1 PASS
0.41
speed_popl10_fig2_1.c [OCRS][without] 1 PASS
0.357
speed_popl10_fig2_2.c [OCRS][without] 1 FAIL
0.368
speed_popl10_nested_multiple.c [OCRS][without] 1 PASS
0.4
speed_popl10_nested_single.c [OCRS][without] 1 PASS
0.374
speed_popl10_sequential_single.c [OCRS][without] 1 PASS
0.336
speed_popl10_simple_multiple.c [OCRS][without] 1 PASS
0.356
speed_popl10_simple_single_2.c [OCRS][without] 1 PASS
0.374
speed_popl10_simple_single.c [OCRS][without] 1 PASS
0.323
t07.c [OCRS][without] 1 PASS
0.351
t08.c [OCRS][without] 1 PASS
0.34
t09.c [OCRS][without] 1 PASS
0.327
t10.c [OCRS][without] 1 PASS
0.33
t11.c [OCRS][without] 1 PASS
0.363
t13.c [OCRS][without] 1 FAIL
0.365
t15.c [OCRS][without] 1 PASS
0.352
t16.c [OCRS][without] 1 PASS
0.347
t19.c [OCRS][without] 1 PASS
0.35
t20.c [OCRS][without] 1 PASS
0.332
t27.c [OCRS][without] 1 PASS
0.393
t28.c [OCRS][without] 1 PASS
0.372
t30.c [OCRS][without] 1 FAIL
0.336
t37.c [OCRS][without] 2 PASS
0.439
t39.c [OCRS][without] 2 PASS
0.43
t46.c [OCRS][without] 1 PASS
0.353
t47.c [OCRS][without] 1 PASS
0.336
Total Below Time = 17.683 (was 14.134)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c [OCRS][without] 2 PASS
PASS
0.358
qsort_full.c [OCRS][without] 7 TIMEOUT
300.005 (22.268)
rec1-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.328
rec1-param_unsafe.c [OCRS][without] 2 PASS
0.328
rec1_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.328
rec1_unsafe.c [OCRS][without] 2 PASS
0.336
rec2-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.332
rec2-param_unsafe.c [OCRS][without] 2 PASS
0.337
rec2_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.321
rec2_unsafe.c [OCRS][without] 2 PASS
0.337
rec-test.c [OCRS][without] 2 PASS
0.319
sas03_bothbranches.c [OCRS][without] 7 PASS
0.787
sas03.c [OCRS][without] 2 PASS
0.64
simulated_lese_recursive.c [OCRS][without] 2 PASS
0.347
Total Below Time = 305.103 (was 27.463)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c [OCRS][without] 1 PASS
0.311
count_up_down_unsafe.c [OCRS][without] 1 PASS
0.325
divide.c [OCRS][without] 1 PASS
0.303
factor_unsafe.c [OCRS][without] 1 PASS
0.311
for_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.298
for_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.318
interproc.c [OCRS][without] 1 PASS
0.313
mult.c [OCRS][without] 1 PASS
PASS
0.308
pointer_arith.c [OCRS][without] 1 PASS
PASS
PASS
PASS
0.308
quotient.c [OCRS][without] 3 PASS
0.379
subtract.c [OCRS][without] 1 PASS
0.312
sum01_bug02_sum01_bug02_base.case_unsafe.c [OCRS][without] 1 PASS
0.317
sum01_bug02_unsafe.c [OCRS][without] 1 PASS
0.351
sum01_real_safe.c [OCRS][without] 1 PASS
0.315
sum01_safe.c [OCRS][without] 1 PASS
0.305
sum01_unsafe.c [OCRS][without] 1 PASS
0.337
sum02_safe.c [OCRS][without] 1 PASS
0.32
sum03_safe.c [OCRS][without] 1 PASS
0.332
sum03_unsafe.c [OCRS][without] 1 PASS
0.361
sum04_safe.c [OCRS][without] 1 PASS
0.306
sum04_unsafe.c [OCRS][without] 1 PASS
0.343
terminator_02_safe.c [OCRS][without] 1 PASS
0.32
terminator_02_unsafe.c [OCRS][without] 1 PASS
0.332
terminator_03_safe.c [OCRS][without] 1 PASS
0.305
terminator_03_unsafe.c [OCRS][without] 1 PASS
0.31
token_ring01_safe.c [OCRS][without] TIMEOUT
300.006
token_ring01_unsafe.c [OCRS][without] TIMEOUT
300.005
toy_safe.c [OCRS][without] EXCEPTION
164.694
trex01_safe.c [OCRS][without] 1 PASS
0.514
trex01_unsafe.c [OCRS][without] 1 PASS
0.347
trex02_safe2.c [OCRS][without] 3 PASS
0.353
trex02_safe.c [OCRS][without] 3 PASS
0.372
trex02_unsafe.c [OCRS][without] 3 PASS
0.357
trex03_safe.c [OCRS][without] 1 PASS
0.404
trex03_unsafe.c [OCRS][without] 1 PASS
0.415
trex04_safe.c [OCRS][without] 1 PASS
0.33
while_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.31
while_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.3
while_infinite_loop_3_safe.c [OCRS][without] 1 PASS
0.314
Total Below Time = 776.761 (was 767.124)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c [OCRS][without] 3 PASS
0.373
blogger_simplified1.c [OCRS][without] 3 PASS
0.71
divided_difference2.c [OCRS][without] TIMEOUT
300.004
mult-proc.c [OCRS][without] 3 PASS
PASS
0.338
mult-proc-params.c [OCRS][without] 3 PASS
PASS
0.374
popall.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
0.372
simulated_scc.c [OCRS][without] 1 PASS
PASS
0.456
Total Below Time = 302.627 (was 302.58)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c [OCRS][without] 1 PASS
0.332
degree2_binomial.c [OCRS][without] 1 PASS
0.404
degree2_monomial.c [OCRS][without] 1 PASS
0.361
degree3_binomial.c [OCRS][without] 1 PASS
1.145
degree3_monomial.c [OCRS][without] 1 PASS
0.378
degree4_binomial.c [OCRS][without] 1 PASS
4.461
degree4_monomial.c [OCRS][without] 1 PASS
0.421
degree5_binomial.c [OCRS][without] 1 TIMEOUT
300.005
degree5_monomial.c [OCRS][without] 1 PASS
0.501
Total Below Time = 308.008 (was 307.537)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c [OCRS][without] 1 PASS
0.324
cubic_with_square_interproc.c [OCRS][without] 2 PASS
0.361
cubic_with_square_nonlinear.c [OCRS][without] 1 PASS
0.335
cubic_with_square_nonlinear_interproc.c [OCRS][without] 2 PASS
0.35
cubic_with_square_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.348
cubic_with_square_unsafe.c [OCRS][without] 1 PASS
0.327
multi-input.c [OCRS][without] 1 PASS
0.4
multi-input_unsafe.c [OCRS][without] 1 PASS
0.424 (0.475)
nondet_loop_bound.c [OCRS][without] 1 PASS
0.344
nondet_loop_bound_quartic.c [OCRS][without] 1 PASS
0.353
nondet_loop_bound_quartic_unsafe.c [OCRS][without] 1 PASS
0.335
nondet_loop_bound_unsafe.c [OCRS][without] 1 PASS
0.359
nonlinear_stratified.c [OCRS][without] 1 FAIL
0.347
nonlinear_stratified_unsafe.c [OCRS][without] 1 PASS
0.339
quartic_with_cube.c [OCRS][without] 1 PASS
0.342
quartic_with_cube_nonlinear.c [OCRS][without] 1 PASS
0.345
quartic_with_cube_nonlinear_unsafe.c [OCRS][without] 1 TIMEOUT
300.004 (0.354)
quartic_with_cube_unsafe.c [OCRS][without] 1 PASS
0.324
quintic_with_quartic.c [OCRS][without] 1 PASS
0.346
quintic_with_quartic_nonlinear.c [OCRS][without] 1 PASS
0.368
quintic_with_quartic_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.36 (0.453)
quintic_with_quartic_unsafe.c [OCRS][without] 1 PASS
0.349
Total Below Time = 307.384 (was 7.853)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c [OCRS][without] 1 PASS
0.433
degree2_FD_AllAux_AllAssm.c [OCRS][without] 1 PASS
2.416 (1.886)
degree2_FD_AllAux_FewAssm.c [OCRS][without] 1 PASS
4.178 (1.894)
degree2_FD_FewAux_FewAssm.c [OCRS][without] 1 PASS
0.571
degree2_FD_FewAux_FewAssm_NonLinAsrt.c [OCRS][without] 1 PASS
0.589
degree3.c [OCRS][without] 1 PASS
0.475
degree3_FD.c [OCRS][without] 1 PASS
0.564
degree4.c [OCRS][without] 1 PASS
0.361
Total Below Time = 9.587 (was 6.789)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c [OCRS][without] 1 PASS
0.375
loop_unsafe.c [OCRS][without] 1 PASS
0.38
simulated_lese_parser.c [OCRS][without] 1 PASS
0.314
simulated_lese_sentinel.c [OCRS][without] 1 PASS
0.33
Total Below Time = 1.399 (was 1.374)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c [OCRS][without] 1 PASS
PASS
PASS
0.328
Total Below Time = 0.328 (was 0.323)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c [OCRS][without] TIMEOUT
300.005
Total Below Time = 300.005 (was 300.007)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c [OCRS][without] 1 PASS
0.331
array_false-unreach-call2.c [OCRS][without] 1 PASS
0.34
array_false-unreach-call3.c [OCRS][without] 1 PASS
0.331
array_true-unreach-call1.c [OCRS][without] 1 FAIL
0.329
array_true-unreach-call2.c [OCRS][without] 1 FAIL
0.338
array_true-unreach-call3.c [OCRS][without] 1 PASS
0.335
array_true-unreach-call4.c [OCRS][without] 1 FAIL
0.332
const_false-unreach-call1.c [OCRS][without] 1 PASS
0.314
const_true-unreach-call1.c [OCRS][without] 1 PASS
0.303
diamond_false-unreach-call1.c [OCRS][without] 1 PASS
0.309
diamond_true-unreach-call1.c [OCRS][without] 1 PASS
0.333
diamond_true-unreach-call2.c [OCRS][without] 1 PASS
0.342
functions_false-unreach-call1.c [OCRS][without] 3 PASS
0.338
functions_true-unreach-call1.c [OCRS][without] 3 PASS
0.332
multivar_false-unreach-call1.c [OCRS][without] 1 PASS
0.311
multivar_true-unreach-call1.c [OCRS][without] 1 PASS
0.326
nested_false-unreach-call1.c [OCRS][without] 1 PASS
0.324
nested_true-unreach-call1.c [OCRS][without] 1 PASS
0.317
overflow_true-unreach-call1.c [OCRS][without] 1 PASS
0.298
phases_false-unreach-call1.c [OCRS][without] 1 PASS
0.32
phases_false-unreach-call2.c [OCRS][without] 1 PASS
0.321
phases_true-unreach-call1.c [OCRS][without] 1 PASS
0.311
phases_true-unreach-call2.c [OCRS][without] 1 PASS
0.332
simple_false-unreach-call1.c [OCRS][without] 1 PASS
0.305
simple_false-unreach-call2.c [OCRS][without] 1 PASS
0.308
simple_false-unreach-call3.c [OCRS][without] 1 PASS
0.311
simple_false-unreach-call4.c [OCRS][without] 1 PASS
0.304
simple_true-unreach-call1.c [OCRS][without] 1 PASS
0.303
simple_true-unreach-call2.c [OCRS][without] 1 PASS
0.313
simple_true-unreach-call3.c [OCRS][without] 1 PASS
0.316
simple_true-unreach-call4.c [OCRS][without] 1 PASS
0.306
underapprox_false-unreach-call1.c [OCRS][without] 1 PASS
0.312
underapprox_false-unreach-call2.c [OCRS][without] 1 PASS
0.308
underapprox_true-unreach-call1.c [OCRS][without] 1 FAIL
0.308
underapprox_true-unreach-call2.c [OCRS][without] 1 PASS
0.309
Total Below Time = 11.17 (was 11.248)
/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.715
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.42
down_true-unreach-call.c [OCRS][without] 1 PASS
0.32
fragtest_simple_true-unreach-call.c [OCRS][without] 1 PASS
0.351
half_2_true-unreach-call.c [OCRS][without] 1 PASS
0.328
heapsort_true-unreach-call.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
11.488 (1.497)
id_build_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.314
id_trans_false-unreach-call.c [OCRS][without] 1 FAIL
FAIL
FAIL
PASS
0.32
large_const_true-unreach-call.c [OCRS][without] 1 PASS
0.381
MADWiFi-encode_ie_ok_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.341
nested6_true-unreach-call.c [OCRS][without] 1 FAIL
FAIL
PASS
0.388
nested9_true-unreach-call.c [OCRS][without] 1 PASS
0.43
nest-if3_true-unreach-call.c [OCRS][without] 1 PASS
0.359
NetBSD_loop_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.326
sendmail-close-angle_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.351
seq_true-unreach-call.c [OCRS][without] 1 PASS
0.36
SpamAssassin-loop_true-unreach-call.c [OCRS][without] TIMEOUT
300.099 (0.92)
string_concat-noarr_true-unreach-call.c [OCRS][without] 1 PASS
0.321
up_true-unreach-call.c [OCRS][without] 1 PASS
0.328
Total Below Time = 317.94 (was 8.797)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c [OCRS][without] 1 PASS
0.312
bhmr2007_true-unreach-call.c [OCRS][without] 1 PASS
0.337
cggmp2005b_true-unreach-call.c [OCRS][without] 1 PASS
0.384
cggmp2005_true-unreach-call.c [OCRS][without] 1 PASS
0.301
cggmp2005_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.313
css2003_true-unreach-call.c [OCRS][without] 1 PASS
0.412
ddlm2013_true-unreach-call.c [OCRS][without] 1 PASS
0.354
gcnr2008_false-unreach-call.c [OCRS][without] 1 TIMEOUT
300.167 (0.606)
gj2007b_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
0.346
gj2007_true-unreach-call.c [OCRS][without] 1 PASS
0.332
gr2006_true-unreach-call.c [OCRS][without] 1 PASS
0.324
gsv2008_true-unreach-call.c [OCRS][without] 1 PASS
0.311
hhk2008_true-unreach-call.c [OCRS][without] 1 PASS
0.312
jm2006_true-unreach-call.c [OCRS][without] 1 PASS
0.339
jm2006_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.347
mcmillan2006_true-unreach-call.c [OCRS][without] 1 FAIL
0.363
Total Below Time = 305.254 (was 5.638)
/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.307
count_by_1_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.316
count_by_2_true-unreach-call.c [OCRS][without] 1 PASS
0.302
count_by_k_true-unreach-call.c [OCRS][without] 1 PASS
0.317
count_by_nondet_true-unreach-call.c [OCRS][without] 1 FAIL
0.322
gauss_sum_true-unreach-call.c [OCRS][without] 1 PASS
0.303
half_true-unreach-call.c [OCRS][without] EXCEPTION
0.317
nested_true-unreach-call.c [OCRS][without] 1 PASS
0.364
Total Below Time = 2.548 (was 2.587)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c [OCRS][without] 1 PASS
0.373
array_true-unreach-call.c [OCRS][without] 1 FAIL
0.371
bubble_sort_false-unreach-call.c [OCRS][without] 4 PASS
PASS
97.251
bubble_sort_true-unreach-call.c [OCRS][without] 1 2.067
compact_false-unreach-call.c [OCRS][without] 1 PASS
0.342
count_up_down_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.302
count_up_down_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.296
eureka_01_false-unreach-call.c [OCRS][without] 1 PASS
1.477
eureka_01_true-unreach-call.c [OCRS][without] 1 FAIL
1.31
eureka_05_true-unreach-call.c [OCRS][without] 1 FAIL
0.679 (0.572)
for_bounded_loop1_false-unreach-call_true-termination.c [OCRS][without] 1 FAIL
FAIL
PASS
0.312
for_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.305
for_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.316
heavy_false-unreach-call.c [OCRS][without] 1 PASS
0.443
heavy_true-unreach-call.c [OCRS][without] 1 PASS
0.424
insertion_sort_false-unreach-call.c [OCRS][without] 1 PASS
1.254
insertion_sort_true-unreach-call.c [OCRS][without] 1 FAIL
0.551
invert_string_false-unreach-call.c [OCRS][without] 1 PASS
0.426
invert_string_true-unreach-call.c [OCRS][without] 1 FAIL
0.42
linear_sea.ch_true-unreach-call.c [OCRS][without] 1 FAIL
0.358
linear_search_false-unreach-call.c [OCRS][without] 1 EXCEPTION
0.39
lu.cmp_true-unreach-call.c [OCRS][without] TIMEOUT
300.252 (51.575)
ludcmp_false-unreach-call.c [OCRS][without] TIMEOUT
300.254 (51.092)
matrix_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.782 (0.609)
matrix_true-unreach-call_true-termination.c [OCRS][without] 1 FAIL
0.423
n.c11_true-unreach-call.c [OCRS][without] 3 FAIL
0.404
n.c24_false-unreach-call.c [OCRS][without] 3 PASS
11.197
n.c40_true-unreach-call.c [OCRS][without] 1 FAIL
0.352
nec11_false-unreach-call.c [OCRS][without] 1 PASS
0.353
nec20_false-unreach-call.c [OCRS][without] 1 PASS
0.349
nec40_true-unreach-call.c [OCRS][without] 1 FAIL
0.355
string_false-unreach-call.c [OCRS][without] 1 PASS
0.521
string_true-unreach-call.c [OCRS][without] 1 FAIL
0.523
sum01_bug02_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.36
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.335
sum01_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.357
sum01_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.325
sum03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.41
sum03_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.34
sum04_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.35
sum04_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.309
sum_array_false-unreach-call.c [OCRS][without] 1 PASS
0.507
sum_array_true-unreach-call.c [OCRS][without] 1 FAIL
0.534
terminator_01_false-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.32
terminator_02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.392
terminator_02_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.334
terminator_03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.321
terminator_03_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.314
trex01_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.408
trex01_true-unreach-call.c [OCRS][without] 3 PASS
0.723 (0.608)
trex02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.371
trex02_true-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.374
trex03_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.65
trex03_true-unreach-call.c [OCRS][without] 3 PASS
0.653
trex04_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.355
veris.c_NetBSD-libc__loop_true-unreach-call.c [OCRS][without] 1 PASS
0.339
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c [OCRS][without] 3 12.053
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c [OCRS][without] 1 PASS
0.337
verisec_NetBSD-libc__loop_false-unreach-call.c [OCRS][without] 1 PASS
0.33
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c [OCRS][without] 3 PASS
7.611
vogal_false-unreach-call.c [OCRS][without] 1 PASS
0.661
vogal_true-unreach-call.c [OCRS][without] 1 FAIL
0.676 (0.614)
while_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.298
while_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.294
while_infinite_loop_3_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.297
while_infinite_loop_4_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.303
Total Below Time = 757.673 (was 259.408)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c [OCRS][without] TIMEOUT
300.028 (1.324)
Ackermann02_false-unreach-call_false-termination.c [OCRS][without] TIMEOUT
300.022 (1.272)
Ackermann03_true-unreach-call.c [OCRS][without] TIMEOUT
300.02 (1.302)
Ackermann04_true-unreach-call.c [OCRS][without] TIMEOUT
300.021 (1.31)
Addition01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.469
Addition02_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.457
Addition03_false-no-overflow.c [OCRS][without] 2 PASS
0.465
Addition03_true-unreach-call.c [OCRS][without] 2 PASS
0.451
BallRajamani-SPIN2000-Fig1_false-unreach-call.c [OCRS][without] 2 PASS
0.388
EvenOdd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.399
EvenOdd03_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.387
Fibonacci01_true-unreach-call.c [OCRS][without] EXCEPTION
0.701 (300.004)
Fibonacci02_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.667 (300.004)
Fibonacci03_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.668 (300.004)
Fibonacci04_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.699 (300.004)
Fibonacci05_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.644 (300.004)
gcd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.442
gcd02_true-unreach-call.c [OCRS][without] 2 FAIL
PASS
0.852
McCarthy91_false-unreach-call_false-termination.c [OCRS][without] 7 PASS
0.88 (0.722)
McCarthy91_true-unreach-call.c [OCRS][without] 7 FAIL
0.874 (0.714)
MultCommutative_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.49
Primes_true-unreach-call.c [OCRS][without] 3 FAIL
1.297
recHanoi01_true-unreach-call_true-termination.c [OCRS][without] TIMEOUT
300.006
recHanoi02_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.348
recHanoi03_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.354
Total Below Time = 1512.029 (was 1813.403)
/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.369
afterrec_2calls_true-unreach-call.c [OCRS][without] 2 PASS
PASS
0.374
afterrec_false-unreach-call.c [OCRS][without] 2 PASS
0.331
afterrec_true-unreach-call.c [OCRS][without] 2 PASS
0.345
fibo_10_false-unreach-call.c [OCRS][without] EXCEPTION
0.652 (300.004)
fibo_10_true-unreach-call.c [OCRS][without] EXCEPTION
0.661 (300.004)
fibo_15_false-unreach-call.c [OCRS][without] EXCEPTION
0.66 (300.005)
fibo_15_true-unreach-call.c [OCRS][without] EXCEPTION
0.64 (300.005)
fibo_20_false-unreach-call.c [OCRS][without] EXCEPTION
0.671 (300.005)
fibo_20_true-unreach-call.c [OCRS][without] EXCEPTION
0.655 (300.005)
fibo_25_false-unreach-call.c [OCRS][without] EXCEPTION
0.652 (300.004)
fibo_25_true-unreach-call.c [OCRS][without] EXCEPTION
0.653 (300.005)
fibo_2calls_10_false-unreach-call.c [OCRS][without] TIMEOUT
300.163
fibo_2calls_10_true-unreach-call.c [OCRS][without] TIMEOUT
300.174
fibo_2calls_15_false-unreach-call.c [OCRS][without] TIMEOUT
300.161
fibo_2calls_15_true-unreach-call.c [OCRS][without] TIMEOUT
300.162
fibo_2calls_20_false-unreach-call.c [OCRS][without] TIMEOUT
300.145
fibo_2calls_20_true-unreach-call.c [OCRS][without] TIMEOUT
300.161
fibo_2calls_25_false-unreach-call.c [OCRS][without] TIMEOUT
300.161
fibo_2calls_25_true-unreach-call.c [OCRS][without] TIMEOUT
300.146
fibo_2calls_2_false-unreach-call.c [OCRS][without] TIMEOUT
300.16
fibo_2calls_2_true-unreach-call.c [OCRS][without] TIMEOUT
300.161
fibo_2calls_4_false-unreach-call.c [OCRS][without] TIMEOUT
300.163
fibo_2calls_4_true-unreach-call.c [OCRS][without] TIMEOUT
300.171
fibo_2calls_5_false-unreach-call.c [OCRS][without] TIMEOUT
300.082
fibo_2calls_5_true-unreach-call.c [OCRS][without] TIMEOUT
300.145
fibo_2calls_6_false-unreach-call.c [OCRS][without] TIMEOUT
300.16
fibo_2calls_6_true-unreach-call.c [OCRS][without] TIMEOUT
300.161
fibo_2calls_8_false-unreach-call.c [OCRS][without] TIMEOUT
300.163
fibo_2calls_8_true-unreach-call.c [OCRS][without] TIMEOUT
300.173
fibo_5_false-unreach-call.c [OCRS][without] EXCEPTION
0.659 (300.004)
fibo_5_true-unreach-call.c [OCRS][without] EXCEPTION
0.673 (300.004)
fibo_7_false-unreach-call.c [OCRS][without] EXCEPTION
0.667 (300.004)
fibo_7_true-unreach-call.c [OCRS][without] EXCEPTION
0.644 (300.004)
id2_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.608
id2_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.653
id2_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.644
id2_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.633
id2_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.381
id2_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.371
id_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.454
id_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.46
id_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.478
id_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.471
id_i10_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.339
id_i10_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.354
id_i15_o15_false-unreach-call.c [OCRS][without] 2 PASS
0.343
id_i15_o15_true-unreach-call.c [OCRS][without] 2 PASS
0.345
id_i20_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.335
id_i20_o20_true-unreach-call.c [OCRS][without] 2 PASS
0.333
id_i25_o25_false-unreach-call.c [OCRS][without] 2 PASS
0.344
id_i25_o25_true-unreach-call.c [OCRS][without] 2 PASS
0.348
id_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.345
id_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.355
id_o1000_false-unreach-call.c [OCRS][without] 2 PASS
0.362
id_o100_false-unreach-call.c [OCRS][without] 2 PASS
0.346
id_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.343
id_o200_false-unreach-call.c [OCRS][without] 2 PASS
0.347
id_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.355
id_o3_false-unreach-call.c [OCRS][without] 2 PASS
0.37
sum_10x0_false-unreach-call.c [OCRS][without] 2 PASS
0.362
sum_10x0_true-unreach-call.c [OCRS][without] 2 PASS
0.352
sum_15x0_false-unreach-call.c [OCRS][without] 2 PASS
0.362
sum_15x0_true-unreach-call.c [OCRS][without] 2 PASS
0.354
sum_20x0_false-unreach-call.c [OCRS][without] 2 PASS
0.355
sum_20x0_true-unreach-call.c [OCRS][without] 2 PASS
0.362
sum_25x0_false-unreach-call.c [OCRS][without] 2 PASS
0.358
sum_25x0_true-unreach-call.c [OCRS][without] 2 PASS
0.348
sum_2x3_false-unreach-call.c [OCRS][without] 2 PASS
0.354
sum_2x3_true-unreach-call.c [OCRS][without] 2 PASS
0.352
sum_non_eq_false-unreach-call.c [OCRS][without] 2 PASS
0.365
sum_non_eq_true-unreach-call.c [OCRS][without] 2 PASS
0.361
sum_non_false-unreach-call.c [OCRS][without] 2 PASS
0.367
sum_non_true-unreach-call.c [OCRS][without] 2 PASS
0.362
Total Below Time = 5427.849 (was 9017.125)
/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.344
rec-bhmr2007_true-unreach-call.c [OCRS][without] 2 PASS
0.366
rec-cggmp2005b_true-unreach-call.c [OCRS][without] 3 PASS
0.568
rec-cggmp2005_true-unreach-call.c [OCRS][without] 2 PASS
0.326
rec-cggmp2005_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.354
rec-css2003_true-unreach-call.c [OCRS][without] 2 PASS
0.541
rec-ddlm2013_true-unreach-call.c [OCRS][without] EXCEPTION
0.326 (0.405)
rec-gcnr2008_false-unreach-call.c [OCRS][without] 2 PASS
0.652
rec-gj2007b_true-unreach-call.c [OCRS][without] 2 FAIL
FAIL
0.361
rec-gj2007_true-unreach-call.c [OCRS][without] 2 FAIL
0.384
rec-gr2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.368
rec-gsv2008_true-unreach-call.c [OCRS][without] 2 PASS
0.322
rec-hhk2008_true-unreach-call.c [OCRS][without] 2 PASS
0.332
rec-jm2006_true-unreach-call.c [OCRS][without] 2 PASS
0.348
rec-jm2006_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.363
rec-mcmillan2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.395
Total Below Time = 6.35 (was 6.367)
/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.317
rec-count_by_1_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.328
rec-count_by_2_true-unreach-call.c [OCRS][without] 2 PASS
0.316
rec-count_by_k_true-unreach-call.c [OCRS][without] 2 PASS
0.338 (0.378)
rec-count_by_nondet_true-unreach-call.c [OCRS][without] 2 FAIL
0.358
rec-gauss_sum_true-unreach-call.c [OCRS][without] 2 PASS
0.336
rec-half_true-unreach-call.c [OCRS][without] EXCEPTION
0.318 (0.369)
rec-nested_true-unreach-call.c [OCRS][without] 3 PASS
0.51
Total Below Time = 2.821 (was 2.912)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c [OCRS][without] 2 PASS
0.464
edit_distance_bottom_up.c [OCRS][without] 3 FAIL
159.719
edit_distance_top_down.c [OCRS][without] 3 FAIL
17.641
log_log_n_solution.c [OCRS][without] 3 FAIL
0.395
log_n_solution.c [OCRS][without] 2 FAIL
0.391
multivariate_1.c [OCRS][without] TIMEOUT
300.004
multivariate_higher_order.c [OCRS][without] 7 FAIL
FAIL
FAIL
10.023 (11.856)
n_cubed_solution.c [OCRS][without] EXCEPTION
0.339
n_log_n_solution.c [OCRS][without] TIMEOUT
300.026 (1.132)
n_squared_two_base_case_even.c [OCRS][without] 2 PASS
0.346
n_squared_two_base_case_odd.c [OCRS][without] 2 PASS
0.341
pascals_dynamic.c [OCRS][without] 3 FAIL
8.991
pascals_iterative.c [OCRS][without] 1 FAIL
2.919 (3.421)
pascals_recursive.c [OCRS][without] TIMEOUT
300.005
squared_solution.c [OCRS][without] TIMEOUT
300.129 (10.241)
two_n_even.c [OCRS][without] 2 PASS
0.343
two_n_odd.c [OCRS][without] 2 PASS
0.339
two_to_n_over_two_even.c [OCRS][without] TIMEOUT
300.007
two_to_n_over_two_odd.c [OCRS][without] TIMEOUT
300.006
two_to_n_squared.c [OCRS][without] 7 FAIL
171.263 (64.386)
two_to_two_to_n.c [OCRS][without] 7 FAIL
0.997
Total Below Time = 2174.688 (was 1485.016)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c [OCRS][without] 1 PASS
0.305
binary_search_array_tree.c [OCRS][without] 1 FAIL
FAIL
0.854 (0.567)
exp_add_loop_rec.c [OCRS][without] 1 FAIL
0.322
exp_add_loop_variable.c [OCRS][without] 1 PASS
0.328
exp_with_linear_inner_loop.c [OCRS][without] 1 FAIL
0.378
halving_log1.c [OCRS][without] 1 PASS
0.396
linear_two_to_n.c [OCRS][without] TIMEOUT
300.005
loop_five_to_n.c [OCRS][without] 1 FAIL
0.356
non_loop_five_to_n.c [OCRS][without] TIMEOUT
300.006
power_log.c [OCRS][without] 1 PASS
0.398 (0.353)
power_log_modified.c [OCRS][without] 1 PASS
0.419 (0.369)
simple_exponential.c [OCRS][without] 1 PASS
0.321
simple_exponential_for.c [OCRS][without] 1 PASS
0.332
two_to_n_minus_n.c [OCRS][without] EXCEPTION
2.615 (300.005)
two_to_n_minus_n_loop.c [OCRS][without] EXCEPTION
1.82 (300.004)
Total Below Time = 608.855 (was 1204.027)

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