[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: 0fa8064dfa94888565bc782359017482a22e6f46 (2017-05-16 08:41:47 -0400) "Fixed build after merge"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-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
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               20170323  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.356
kmp.c [OCRS][without] 1 PASS
1.29 (1.161)
qsort.c [OCRS][without] 5 PASS
3.421 (2.056)
speed_pldi09_fig1.c [OCRS][without] 1 PASS
0.366
speed_pldi09_fig4_2.c [OCRS][without] 1 FAIL
0.399
speed_pldi09_fig4_4.c [OCRS][without] 1 PASS
0.453
speed_pldi09_fig4_5.c [OCRS][without] 1 PASS
0.367
speed_pldi10_ex1.c [OCRS][without] 1 PASS
3.799 (0.829)
speed_pldi10_ex3.c [OCRS][without] 1 PASS
0.455
speed_pldi10_ex4.c [OCRS][without] EXCEPTION
0.396
speed_popl10_fig2_1.c [OCRS][without] 1 PASS
0.388
speed_popl10_fig2_2.c [OCRS][without] 1 FAIL
0.353
speed_popl10_nested_multiple.c [OCRS][without] 1 PASS
0.445
speed_popl10_nested_single.c [OCRS][without] 1 PASS
0.388
speed_popl10_sequential_single.c [OCRS][without] 1 PASS
0.361
speed_popl10_simple_multiple.c [OCRS][without] 1 PASS
0.4
speed_popl10_simple_single_2.c [OCRS][without] 1 PASS
0.399
speed_popl10_simple_single.c [OCRS][without] 1 PASS
0.335
t07.c [OCRS][without] 1 PASS
0.383
t08.c [OCRS][without] 1 PASS
0.363
t09.c [OCRS][without] 1 PASS
0.355
t10.c [OCRS][without] 1 PASS
0.349
t11.c [OCRS][without] 1 PASS
0.38
t13.c [OCRS][without] 1 FAIL
0.386
t15.c [OCRS][without] 1 PASS
0.361
t16.c [OCRS][without] 1 PASS
0.363
t19.c [OCRS][without] 1 PASS
0.353
t20.c [OCRS][without] 1 PASS
0.339
t27.c [OCRS][without] 1 PASS
0.424
t28.c [OCRS][without] 1 PASS
0.377
t30.c [OCRS][without] 1 FAIL
0.357
t37.c [OCRS][without] 2 PASS
0.469
t39.c [OCRS][without] 2 PASS
0.491
t46.c [OCRS][without] 1 PASS
0.352
t47.c [OCRS][without] 1 PASS
0.363
Total Below Time = 20.836 (was 16.36)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c [OCRS][without] 2 PASS
PASS
0.379
qsort_full.c [OCRS][without] 5 TIMEOUT
300.009 (42.75)
rec1-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.365
rec1-param_unsafe.c [OCRS][without] 2 PASS
0.354
rec1_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.32
rec1_unsafe.c [OCRS][without] 2 PASS
0.33
rec2-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.343
rec2-param_unsafe.c [OCRS][without] 2 PASS
0.344
rec2_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.33
rec2_unsafe.c [OCRS][without] 2 PASS
0.328
rec-test.c [OCRS][without] 2 PASS
0.338
sas03_bothbranches.c [OCRS][without] 7 PASS
1.26
sas03.c [OCRS][without] 2 PASS
0.833
simulated_lese_recursive.c [OCRS][without] 2 PASS
0.405
Total Below Time = 305.938 (was 48.641)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c [OCRS][without] 1 PASS
0.314
count_up_down_unsafe.c [OCRS][without] 1 PASS
0.324
divide.c [OCRS][without] 1 PASS
0.318
factor_unsafe.c [OCRS][without] 1 PASS
0.321
for_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.353
for_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.308
interproc.c [OCRS][without] 1 PASS
0.315
mult.c [OCRS][without] 1 PASS
PASS
0.33
pointer_arith.c [OCRS][without] 1 PASS
PASS
PASS
PASS
0.302
quotient.c [OCRS][without] 3 PASS
0.434
subtract.c [OCRS][without] 1 PASS
0.317
sum01_bug02_sum01_bug02_base.case_unsafe.c [OCRS][without] 1 PASS
0.333
sum01_bug02_unsafe.c [OCRS][without] 1 PASS
0.374
sum01_real_safe.c [OCRS][without] 1 PASS
0.32
sum01_safe.c [OCRS][without] 1 PASS
0.325
sum01_unsafe.c [OCRS][without] 1 PASS
0.365
sum02_safe.c [OCRS][without] 1 PASS
0.337
sum03_safe.c [OCRS][without] 1 PASS
0.349
sum03_unsafe.c [OCRS][without] 1 PASS
0.403
sum04_safe.c [OCRS][without] 1 PASS
0.318
sum04_unsafe.c [OCRS][without] 1 PASS
0.354
terminator_02_safe.c [OCRS][without] 1 PASS
0.331
terminator_02_unsafe.c [OCRS][without] 1 PASS
0.34
terminator_03_safe.c [OCRS][without] 1 PASS
0.323
terminator_03_unsafe.c [OCRS][without] 1 PASS
0.334
token_ring01_safe.c [OCRS][without] TIMEOUT
300.007
token_ring01_unsafe.c [OCRS][without] TIMEOUT
300.006
toy_safe.c [OCRS][without] EXCEPTION
166.509
trex01_safe.c [OCRS][without] 1 PASS
0.725
trex01_unsafe.c [OCRS][without] 1 PASS
0.391
trex02_safe2.c [OCRS][without] 3 PASS
0.383
trex02_safe.c [OCRS][without] 3 PASS
0.385
trex02_unsafe.c [OCRS][without] 3 PASS
0.391
trex03_safe.c [OCRS][without] 1 PASS
0.456
trex03_unsafe.c [OCRS][without] 1 PASS
0.468 (0.41)
trex04_safe.c [OCRS][without] 1 PASS
0.343
while_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.306
while_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.32
while_infinite_loop_3_safe.c [OCRS][without] 1 PASS
0.312
Total Below Time = 779.444 (was 792.254)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c [OCRS][without] 3 PASS
0.447
blogger_simplified1.c [OCRS][without] 3 PASS
0.984
divided_difference2.c [OCRS][without] TIMEOUT
300.006
mult-proc.c [OCRS][without] 3 PASS
PASS
0.358
mult-proc-params.c [OCRS][without] 3 PASS
PASS
0.389
popall.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
0.413
simulated_scc.c [OCRS][without] 1 PASS
PASS
0.52
Total Below Time = 303.117 (was 303.1)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c [OCRS][without] 1 PASS
0.344
degree2_binomial.c [OCRS][without] 1 PASS
0.477
degree2_monomial.c [OCRS][without] 1 PASS
0.372
degree3_binomial.c [OCRS][without] 1 PASS
0.876
degree3_monomial.c [OCRS][without] 1 PASS
0.42
degree4_binomial.c [OCRS][without] 1 PASS
1.165
degree4_monomial.c [OCRS][without] 1 PASS
0.487
degree5_binomial.c [OCRS][without] 1 PASS
1.725
degree5_monomial.c [OCRS][without] 1 PASS
0.553
Total Below Time = 6.419 (was 6.476)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c [OCRS][without] 1 PASS
0.34
cubic_with_square_interproc.c [OCRS][without] 2 PASS
0.392
cubic_with_square_nonlinear.c [OCRS][without] 1 PASS
0.343
cubic_with_square_nonlinear_interproc.c [OCRS][without] 2 PASS
0.377
cubic_with_square_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.363
cubic_with_square_unsafe.c [OCRS][without] 1 PASS
0.351
multi-input.c [OCRS][without] 1 PASS
0.409
multi-input_unsafe.c [OCRS][without] 1 PASS
0.446
nondet_loop_bound.c [OCRS][without] 1 PASS
0.363
nondet_loop_bound_quartic.c [OCRS][without] 1 PASS
0.367
nondet_loop_bound_quartic_unsafe.c [OCRS][without] 1 PASS
0.371
nondet_loop_bound_unsafe.c [OCRS][without] 1 PASS
0.381
nonlinear_stratified.c [OCRS][without] 1 FAIL
0.349
nonlinear_stratified_unsafe.c [OCRS][without] 1 PASS
0.368
quartic_with_cube.c [OCRS][without] 1 PASS
0.355
quartic_with_cube_nonlinear.c [OCRS][without] 1 PASS
0.364
quartic_with_cube_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.368
quartic_with_cube_unsafe.c [OCRS][without] 1 PASS
0.359
quintic_with_quartic.c [OCRS][without] 1 PASS
0.36
quintic_with_quartic_nonlinear.c [OCRS][without] 1 PASS
0.395
quintic_with_quartic_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.379 (0.458)
quintic_with_quartic_unsafe.c [OCRS][without] 1 PASS
0.367
Total Below Time = 8.167 (was 8.207)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c [OCRS][without] 1 PASS
0.516
degree2_FD_AllAux_AllAssm.c [OCRS][without] 1 PASS
3.684 (3.094)
degree2_FD_AllAux_FewAssm.c [OCRS][without] 1 PASS
5.428 (3.108)
degree2_FD_FewAux_FewAssm.c [OCRS][without] 1 PASS
0.705
degree2_FD_FewAux_FewAssm_NonLinAsrt.c [OCRS][without] 1 PASS
0.7
degree3.c [OCRS][without] 1 PASS
0.569
degree3_FD.c [OCRS][without] 1 PASS
0.728
degree4.c [OCRS][without] 1 PASS
0.403
Total Below Time = 12.733 (was 9.763)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c [OCRS][without] 1 PASS
0.383
loop_unsafe.c [OCRS][without] 1 PASS
0.41
simulated_lese_parser.c [OCRS][without] 1 PASS
0.313
simulated_lese_sentinel.c [OCRS][without] 1 PASS
0.342
Total Below Time = 1.448 (was 1.461)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c [OCRS][without] 1 PASS
PASS
PASS
0.338
Total Below Time = 0.338 (was 0.341)
/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.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.338
array_false-unreach-call2.c [OCRS][without] 1 PASS
0.375
array_false-unreach-call3.c [OCRS][without] 1 PASS
0.339
array_true-unreach-call1.c [OCRS][without] 1 FAIL
0.347
array_true-unreach-call2.c [OCRS][without] 1 FAIL
0.371
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.32
const_true-unreach-call1.c [OCRS][without] 1 PASS
0.321
diamond_false-unreach-call1.c [OCRS][without] 1 PASS
0.333
diamond_true-unreach-call1.c [OCRS][without] 1 PASS
0.328
diamond_true-unreach-call2.c [OCRS][without] 1 PASS
0.377
functions_false-unreach-call1.c [OCRS][without] 3 PASS
0.368
functions_true-unreach-call1.c [OCRS][without] 3 PASS
0.349
multivar_false-unreach-call1.c [OCRS][without] 1 PASS
0.318
multivar_true-unreach-call1.c [OCRS][without] 1 PASS
0.322
nested_false-unreach-call1.c [OCRS][without] 1 PASS
0.339
nested_true-unreach-call1.c [OCRS][without] 1 PASS
0.334
overflow_true-unreach-call1.c [OCRS][without] 1 PASS
0.354 (0.31)
phases_false-unreach-call1.c [OCRS][without] 1 PASS
0.338
phases_false-unreach-call2.c [OCRS][without] 1 PASS
0.342
phases_true-unreach-call1.c [OCRS][without] 1 PASS
0.324
phases_true-unreach-call2.c [OCRS][without] 1 PASS
0.334
simple_false-unreach-call1.c [OCRS][without] 1 PASS
0.318
simple_false-unreach-call2.c [OCRS][without] 1 PASS
0.311
simple_false-unreach-call3.c [OCRS][without] 1 PASS
0.317
simple_false-unreach-call4.c [OCRS][without] 1 PASS
0.327
simple_true-unreach-call1.c [OCRS][without] 1 PASS
0.334
simple_true-unreach-call2.c [OCRS][without] 1 PASS
0.32
simple_true-unreach-call3.c [OCRS][without] 1 PASS
0.313
simple_true-unreach-call4.c [OCRS][without] 1 PASS
0.311
underapprox_false-unreach-call1.c [OCRS][without] 1 PASS
0.334
underapprox_false-unreach-call2.c [OCRS][without] 1 PASS
0.328
underapprox_true-unreach-call1.c [OCRS][without] 1 FAIL
0.329
underapprox_true-unreach-call2.c [OCRS][without] 1 PASS
0.321
Total Below Time = 11.701 (was 11.623)
/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.837
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.477 (0.428)
down_true-unreach-call.c [OCRS][without] 1 PASS
0.343
fragtest_simple_true-unreach-call.c [OCRS][without] 1 PASS
0.369
half_2_true-unreach-call.c [OCRS][without] 1 PASS
0.353
heapsort_true-unreach-call.c [OCRS][without] 1 TIMEOUT
300.141 (2.353)
id_build_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.338
id_trans_false-unreach-call.c [OCRS][without] 1 FAIL
FAIL
FAIL
PASS
0.363
large_const_true-unreach-call.c [OCRS][without] 1 PASS
0.414
MADWiFi-encode_ie_ok_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.374
nested6_true-unreach-call.c [OCRS][without] 1 FAIL
FAIL
PASS
0.427
nested9_true-unreach-call.c [OCRS][without] 1 PASS
0.45
nest-if3_true-unreach-call.c [OCRS][without] 1 PASS
0.413
NetBSD_loop_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.339
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.373
SpamAssassin-loop_true-unreach-call.c [OCRS][without] TIMEOUT
300.11 (1.16)
string_concat-noarr_true-unreach-call.c [OCRS][without] 1 PASS
0.352
up_true-unreach-call.c [OCRS][without] 1 PASS
0.335
Total Below Time = 607.205 (was 10.292)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c [OCRS][without] 1 PASS
0.338
bhmr2007_true-unreach-call.c [OCRS][without] 1 PASS
0.356
cggmp2005b_true-unreach-call.c [OCRS][without] 1 PASS
0.398
cggmp2005_true-unreach-call.c [OCRS][without] 1 PASS
0.334
cggmp2005_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.329
css2003_true-unreach-call.c [OCRS][without] 1 PASS
0.477
ddlm2013_true-unreach-call.c [OCRS][without] 1 PASS
0.387
gcnr2008_false-unreach-call.c [OCRS][without] 1 TIMEOUT
300.179 (0.85)
gj2007b_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
0.35
gj2007_true-unreach-call.c [OCRS][without] 1 PASS
0.339
gr2006_true-unreach-call.c [OCRS][without] 1 PASS
0.351
gsv2008_true-unreach-call.c [OCRS][without] 1 PASS
0.328
hhk2008_true-unreach-call.c [OCRS][without] 1 PASS
0.338
jm2006_true-unreach-call.c [OCRS][without] 1 PASS
0.351
jm2006_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.381
mcmillan2006_true-unreach-call.c [OCRS][without] 1 FAIL
0.375
Total Below Time = 305.611 (was 6.187)
/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.316
count_by_1_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.341
count_by_2_true-unreach-call.c [OCRS][without] 1 PASS
0.313
count_by_k_true-unreach-call.c [OCRS][without] 1 PASS
0.336
count_by_nondet_true-unreach-call.c [OCRS][without] 1 FAIL
0.345
gauss_sum_true-unreach-call.c [OCRS][without] 1 PASS
0.345
half_true-unreach-call.c [OCRS][without] EXCEPTION
0.33
nested_true-unreach-call.c [OCRS][without] 1 PASS
0.381
Total Below Time = 2.707 (was 2.652)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c [OCRS][without] 1 PASS
0.43
array_true-unreach-call.c [OCRS][without] 1 FAIL
0.423
bubble_sort_false-unreach-call.c [OCRS][without] 4 PASS
PASS
141.423
bubble_sort_true-unreach-call.c [OCRS][without] 1 3.825
compact_false-unreach-call.c [OCRS][without] 1 PASS
0.369
count_up_down_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.333
count_up_down_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.329
eureka_01_false-unreach-call.c [OCRS][without] 1 PASS
2.208
eureka_01_true-unreach-call.c [OCRS][without] 1 FAIL
1.922
eureka_05_true-unreach-call.c [OCRS][without] 1 FAIL
1.052 (0.743)
for_bounded_loop1_false-unreach-call_true-termination.c [OCRS][without] 1 FAIL
FAIL
PASS
0.331
for_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.313
for_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.317
heavy_false-unreach-call.c [OCRS][without] 1 PASS
0.544
heavy_true-unreach-call.c [OCRS][without] 1 PASS
0.499
insertion_sort_false-unreach-call.c [OCRS][without] 1 PASS
2.194
insertion_sort_true-unreach-call.c [OCRS][without] 1 FAIL
0.747
invert_string_false-unreach-call.c [OCRS][without] 1 PASS
0.5
invert_string_true-unreach-call.c [OCRS][without] 1 FAIL
0.494
linear_sea.ch_true-unreach-call.c [OCRS][without] 1 FAIL
0.378
linear_search_false-unreach-call.c [OCRS][without] 1 EXCEPTION
0.401
lu.cmp_true-unreach-call.c [OCRS][without] TIMEOUT
300.274 (124.22)
ludcmp_false-unreach-call.c [OCRS][without] TIMEOUT
300.242 (124.424)
matrix_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.983 (0.8)
matrix_true-unreach-call_true-termination.c [OCRS][without] 1 FAIL
0.508
n.c11_true-unreach-call.c [OCRS][without] 3 FAIL
0.471
n.c24_false-unreach-call.c [OCRS][without] 3 PASS
23.43
n.c40_true-unreach-call.c [OCRS][without] 1 FAIL
0.372
nec11_false-unreach-call.c [OCRS][without] 1 PASS
0.378
nec20_false-unreach-call.c [OCRS][without] 1 PASS
0.367
nec40_true-unreach-call.c [OCRS][without] 1 FAIL
0.38 (0.555)
string_false-unreach-call.c [OCRS][without] 1 PASS
0.674
string_true-unreach-call.c [OCRS][without] 1 FAIL
0.632
sum01_bug02_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.378
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.34
sum01_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.359
sum01_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.338
sum03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.503
sum03_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.352
sum04_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.357
sum04_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.331
sum_array_false-unreach-call.c [OCRS][without] 1 PASS
0.661
sum_array_true-unreach-call.c [OCRS][without] 1 FAIL
0.679
terminator_01_false-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.319
terminator_02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.425
terminator_02_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.34
terminator_03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.332
terminator_03_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.331
trex01_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.456
trex01_true-unreach-call.c [OCRS][without] 3 PASS
0.798 (0.679)
trex02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.408
trex02_true-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.392
trex03_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.883
trex03_true-unreach-call.c [OCRS][without] 3 PASS
0.837
trex04_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.391
veris.c_NetBSD-libc__loop_true-unreach-call.c [OCRS][without] 1 PASS
0.349
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c [OCRS][without] 3 24.527
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c [OCRS][without] 1 PASS
0.347
verisec_NetBSD-libc__loop_false-unreach-call.c [OCRS][without] 1 PASS
0.349
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c [OCRS][without] 3 PASS
17.053
vogal_false-unreach-call.c [OCRS][without] 1 PASS
0.832 (0.734)
vogal_true-unreach-call.c [OCRS][without] 1 FAIL
0.843
while_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.297
while_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.31
while_infinite_loop_3_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.31
while_infinite_loop_4_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.321
Total Below Time = 843.491 (was 488.599)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c [OCRS][without] TIMEOUT
300.031 (2.517)
Ackermann02_false-unreach-call_false-termination.c [OCRS][without] TIMEOUT
300.033 (2.335)
Ackermann03_true-unreach-call.c [OCRS][without] TIMEOUT
300.022 (2.556)
Ackermann04_true-unreach-call.c [OCRS][without] TIMEOUT
300.022 (2.464)
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.586
Addition03_false-no-overflow.c [OCRS][without] 2 PASS
0.566
Addition03_true-unreach-call.c [OCRS][without] 2 PASS
0.586
BallRajamani-SPIN2000-Fig1_false-unreach-call.c [OCRS][without] 2 PASS
0.452
EvenOdd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.441
EvenOdd03_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.415
Fibonacci01_true-unreach-call.c [OCRS][without] EXCEPTION
0.948 (300.011)
Fibonacci02_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.94 (300.004)
Fibonacci03_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.958 (300.004)
Fibonacci04_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.984 (300.011)
Fibonacci05_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.955 (300.006)
gcd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.574
gcd02_true-unreach-call.c [OCRS][without] 2 FAIL
PASS
1.36 (1.197)
McCarthy91_false-unreach-call_false-termination.c [OCRS][without] 7 PASS
1.445 (1.113)
McCarthy91_true-unreach-call.c [OCRS][without] 7 FAIL
1.401 (1.111)
MultCommutative_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.689 (0.62)
Primes_true-unreach-call.c [OCRS][without] 3 FAIL
2.111
recHanoi01_true-unreach-call_true-termination.c [OCRS][without] 9 FAIL
5.767
recHanoi02_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.371
recHanoi03_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.388
Total Below Time = 1222.635 (was 1526.825)
/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.417
afterrec_2calls_true-unreach-call.c [OCRS][without] 2 PASS
PASS
0.381
afterrec_false-unreach-call.c [OCRS][without] 2 PASS
0.356
afterrec_true-unreach-call.c [OCRS][without] 2 PASS
0.343
fibo_10_false-unreach-call.c [OCRS][without] EXCEPTION
0.952 (300.008)
fibo_10_true-unreach-call.c [OCRS][without] EXCEPTION
0.991 (300.011)
fibo_15_false-unreach-call.c [OCRS][without] EXCEPTION
0.979 (300.005)
fibo_15_true-unreach-call.c [OCRS][without] EXCEPTION
0.963 (300.007)
fibo_20_false-unreach-call.c [OCRS][without] EXCEPTION
0.992 (300.01)
fibo_20_true-unreach-call.c [OCRS][without] EXCEPTION
0.951 (300.005)
fibo_25_false-unreach-call.c [OCRS][without] EXCEPTION
0.943 (300.009)
fibo_25_true-unreach-call.c [OCRS][without] EXCEPTION
0.958 (300.011)
fibo_2calls_10_false-unreach-call.c [OCRS][without] EXCEPTION
16.952 (132.115)
fibo_2calls_10_true-unreach-call.c [OCRS][without] EXCEPTION
17.207 (129.288)
fibo_2calls_15_false-unreach-call.c [OCRS][without] EXCEPTION
17.216 (132.676)
fibo_2calls_15_true-unreach-call.c [OCRS][without] EXCEPTION
17.326 (131.59)
fibo_2calls_20_false-unreach-call.c [OCRS][without] EXCEPTION
17.172 (128.59)
fibo_2calls_20_true-unreach-call.c [OCRS][without] EXCEPTION
17.247 (132.123)
fibo_2calls_25_false-unreach-call.c [OCRS][without] EXCEPTION
17.287 (129.226)
fibo_2calls_25_true-unreach-call.c [OCRS][without] EXCEPTION
17.35 (129.357)
fibo_2calls_2_false-unreach-call.c [OCRS][without] EXCEPTION
17.183 (129.49)
fibo_2calls_2_true-unreach-call.c [OCRS][without] EXCEPTION
17.458 (128.901)
fibo_2calls_4_false-unreach-call.c [OCRS][without] EXCEPTION
18.05 (129.766)
fibo_2calls_4_true-unreach-call.c [OCRS][without] EXCEPTION
18.222 (129.599)
fibo_2calls_5_false-unreach-call.c [OCRS][without] EXCEPTION
17.528 (133.521)
fibo_2calls_5_true-unreach-call.c [OCRS][without] EXCEPTION
17.563 (132.07)
fibo_2calls_6_false-unreach-call.c [OCRS][without] EXCEPTION
17.587 (128.652)
fibo_2calls_6_true-unreach-call.c [OCRS][without] EXCEPTION
17.566 (129.257)
fibo_2calls_8_false-unreach-call.c [OCRS][without] EXCEPTION
17.409 (132.449)
fibo_2calls_8_true-unreach-call.c [OCRS][without] EXCEPTION
17.626 (131.527)
fibo_5_false-unreach-call.c [OCRS][without] EXCEPTION
0.96 (300.009)
fibo_5_true-unreach-call.c [OCRS][without] EXCEPTION
0.961 (300.011)
fibo_7_false-unreach-call.c [OCRS][without] EXCEPTION
0.996 (300.006)
fibo_7_true-unreach-call.c [OCRS][without] EXCEPTION
0.94 (300.008)
id2_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.94
id2_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
1.025
id2_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.995
id2_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
1.013
id2_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.45
id2_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.426
id_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.621
id_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.601
id_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.596
id_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.603
id_i10_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.427 (0.384)
id_i10_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.393
id_i15_o15_false-unreach-call.c [OCRS][without] 2 PASS
0.393
id_i15_o15_true-unreach-call.c [OCRS][without] 2 PASS
0.386
id_i20_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.37
id_i20_o20_true-unreach-call.c [OCRS][without] 2 PASS
0.377
id_i25_o25_false-unreach-call.c [OCRS][without] 2 PASS
0.389
id_i25_o25_true-unreach-call.c [OCRS][without] 2 PASS
0.378
id_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.389
id_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.377
id_o1000_false-unreach-call.c [OCRS][without] 2 PASS
0.378
id_o100_false-unreach-call.c [OCRS][without] 2 PASS
0.405
id_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.374
id_o200_false-unreach-call.c [OCRS][without] 2 PASS
0.391
id_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.394
id_o3_false-unreach-call.c [OCRS][without] 2 PASS
0.385
sum_10x0_false-unreach-call.c [OCRS][without] 2 PASS
0.401
sum_10x0_true-unreach-call.c [OCRS][without] 2 PASS
0.387
sum_15x0_false-unreach-call.c [OCRS][without] 2 PASS
0.415
sum_15x0_true-unreach-call.c [OCRS][without] 2 PASS
0.392
sum_20x0_false-unreach-call.c [OCRS][without] 2 PASS
0.411
sum_20x0_true-unreach-call.c [OCRS][without] 2 PASS
0.38
sum_25x0_false-unreach-call.c [OCRS][without] 2 PASS
0.395
sum_25x0_true-unreach-call.c [OCRS][without] 2 PASS
0.379
sum_2x3_false-unreach-call.c [OCRS][without] 2 PASS
0.407
sum_2x3_true-unreach-call.c [OCRS][without] 2 PASS
0.397
sum_non_eq_false-unreach-call.c [OCRS][without] 2 PASS
0.45
sum_non_eq_true-unreach-call.c [OCRS][without] 2 PASS
0.425
sum_non_false-unreach-call.c [OCRS][without] 2 PASS
0.416
sum_non_true-unreach-call.c [OCRS][without] 2 PASS
0.386
Total Below Time = 346.149 (was 5970.401)
/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.377
rec-bhmr2007_true-unreach-call.c [OCRS][without] 2 PASS
0.42
rec-cggmp2005b_true-unreach-call.c [OCRS][without] 3 PASS
0.793
rec-cggmp2005_true-unreach-call.c [OCRS][without] 2 PASS
0.331
rec-cggmp2005_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.353 (0.408)
rec-css2003_true-unreach-call.c [OCRS][without] 2 PASS
0.619
rec-ddlm2013_true-unreach-call.c [OCRS][without] EXCEPTION
0.346 (0.453)
rec-gcnr2008_false-unreach-call.c [OCRS][without] 2 PASS
0.903
rec-gj2007b_true-unreach-call.c [OCRS][without] 2 FAIL
FAIL
0.392
rec-gj2007_true-unreach-call.c [OCRS][without] 2 FAIL
0.381
rec-gr2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.41 (0.371)
rec-gsv2008_true-unreach-call.c [OCRS][without] 2 PASS
0.341
rec-hhk2008_true-unreach-call.c [OCRS][without] 2 PASS
0.344
rec-jm2006_true-unreach-call.c [OCRS][without] 2 PASS
0.381
rec-jm2006_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.397
rec-mcmillan2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.42
Total Below Time = 7.208 (was 7.26)
/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.329
rec-count_by_1_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.345
rec-count_by_2_true-unreach-call.c [OCRS][without] 2 PASS
0.347
rec-count_by_k_true-unreach-call.c [OCRS][without] 2 PASS
0.368
rec-count_by_nondet_true-unreach-call.c [OCRS][without] 2 FAIL
0.396
rec-gauss_sum_true-unreach-call.c [OCRS][without] 2 PASS
0.368
rec-half_true-unreach-call.c [OCRS][without] EXCEPTION
0.342 (0.408)
rec-nested_true-unreach-call.c [OCRS][without] 3 PASS
0.6
Total Below Time = 3.095 (was 3.175)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c [OCRS][without] 2 PASS
0.536
edit_distance_bottom_up.c [OCRS][without] 3 TIMEOUT
300.01
edit_distance_top_down.c [OCRS][without] 3 FAIL
51.673
log_log_n_solution.c [OCRS][without] 3 FAIL
0.426 (0.847)
log_n_solution.c [OCRS][without] 2 FAIL
0.441
multivariate_1.c [OCRS][without] TIMEOUT
300.007
multivariate_higher_order.c [OCRS][without] 7 FAIL
FAIL
FAIL
26.643
n_cubed_solution.c [OCRS][without] EXCEPTION
0.34
n_log_n_solution.c [OCRS][without] TIMEOUT
300.027 (1.901)
n_squared_two_base_case_even.c [OCRS][without] 2 PASS
0.385
n_squared_two_base_case_odd.c [OCRS][without] 2 PASS
0.387
pascals_dynamic.c [OCRS][without] 3 FAIL
20.127
pascals_iterative.c [OCRS][without] 1 FAIL
5.501 (6.165)
pascals_recursive.c [OCRS][without] TIMEOUT
300.005
squared_solution.c [OCRS][without] TIMEOUT
300.138 (12.223)
two_n_even.c [OCRS][without] 2 PASS
0.386
two_n_odd.c [OCRS][without] 2 PASS
0.367
two_to_n_over_two_even.c [OCRS][without] TIMEOUT
300.034 (44.617)
two_to_n_over_two_odd.c [OCRS][without] TIMEOUT
300.024 (44.636)
two_to_n_squared.c [OCRS][without] 8 TIMEOUT
300.005 (137.653)
two_to_two_to_n.c [OCRS][without] 7 FAIL
1.67
Total Below Time = 2509.132 (was 1250.232)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c [OCRS][without] 1 PASS
0.315
exp_add_loop_rec.c [OCRS][without] 1 FAIL
0.357
exp_add_loop_variable.c [OCRS][without] 1 PASS
0.351
exp_with_linear_inner_loop.c [OCRS][without] 1 FAIL
0.418
linear_two_to_n.c [OCRS][without] 8 FAIL
1.525 (1.385)
loop_five_to_n.c [OCRS][without] 1 FAIL
0.358
non_loop_five_to_n.c [OCRS][without] 8 FAIL
10.055 (8.656)
power_log.c [OCRS][without] 1 PASS
0.424
power_log_modified.c [OCRS][without] 1 PASS
0.49 (0.406)
simple_exponential.c [OCRS][without] 1 PASS
0.339
simple_exponential_for.c [OCRS][without] 1 PASS
0.347
two_to_n_minus_n.c [OCRS][without] 8 FAIL
1.817
two_to_n_minus_n_loop.c [OCRS][without] 8 FAIL
2.751
Total Below Time = 19.547 (was 17.575)

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