[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.349
kmp.c [OCRS][without] 1 PASS
1.315 (1.18)
qsort.c [OCRS][without] 5 PASS
3.525 (1.996)
speed_pldi09_fig1.c [OCRS][without] 1 PASS
0.405
speed_pldi09_fig4_2.c [OCRS][without] 1 FAIL
0.39
speed_pldi09_fig4_4.c [OCRS][without] 1 PASS
0.467
speed_pldi09_fig4_5.c [OCRS][without] 1 PASS
0.371
speed_pldi10_ex1.c [OCRS][without] 1 PASS
3.746 (0.788)
speed_pldi10_ex3.c [OCRS][without] 1 PASS
0.448
speed_pldi10_ex4.c [OCRS][without] EXCEPTION
0.412
speed_popl10_fig2_1.c [OCRS][without] 1 PASS
0.408
speed_popl10_fig2_2.c [OCRS][without] 1 FAIL
0.358
speed_popl10_nested_multiple.c [OCRS][without] 1 PASS
0.431
speed_popl10_nested_single.c [OCRS][without] 1 PASS
0.417
speed_popl10_sequential_single.c [OCRS][without] 1 PASS
0.351
speed_popl10_simple_multiple.c [OCRS][without] 1 PASS
0.387
speed_popl10_simple_single_2.c [OCRS][without] 1 PASS
0.411
speed_popl10_simple_single.c [OCRS][without] 1 PASS
0.33
t07.c [OCRS][without] 1 PASS
0.37
t08.c [OCRS][without] 1 PASS
0.36
t09.c [OCRS][without] 1 PASS
0.365
t10.c [OCRS][without] 1 PASS
0.355
t11.c [OCRS][without] 1 PASS
0.377
t13.c [OCRS][without] 1 FAIL
0.386
t15.c [OCRS][without] 1 PASS
0.379
t16.c [OCRS][without] 1 PASS
0.347
t19.c [OCRS][without] 1 PASS
0.335
t20.c [OCRS][without] 1 PASS
0.34
t27.c [OCRS][without] 1 PASS
0.43
t28.c [OCRS][without] 1 PASS
0.378
t30.c [OCRS][without] 1 FAIL
0.345
t37.c [OCRS][without] 2 PASS
0.483
t39.c [OCRS][without] 2 PASS
0.501
t46.c [OCRS][without] 1 PASS
0.362
t47.c [OCRS][without] 1 PASS
0.363
Total Below Time = 20.997 (was 16.261)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c [OCRS][without] 2 PASS
PASS
0.392
qsort_full.c [OCRS][without] 5 TIMEOUT
300.005 (42.179)
rec1-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.333
rec1-param_unsafe.c [OCRS][without] 2 PASS
0.359
rec1_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.347
rec1_unsafe.c [OCRS][without] 2 PASS
0.349
rec2-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.351
rec2-param_unsafe.c [OCRS][without] 2 PASS
0.352
rec2_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.324
rec2_unsafe.c [OCRS][without] 2 PASS
0.339
rec-test.c [OCRS][without] 2 PASS
0.332
sas03_bothbranches.c [OCRS][without] 7 PASS
1.274
sas03.c [OCRS][without] 2 PASS
0.849
simulated_lese_recursive.c [OCRS][without] 2 PASS
0.4
Total Below Time = 306.006 (was 48.158)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c [OCRS][without] 1 PASS
0.329
count_up_down_unsafe.c [OCRS][without] 1 PASS
0.32
divide.c [OCRS][without] 1 PASS
0.344
factor_unsafe.c [OCRS][without] 1 PASS
0.339
for_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.32
for_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.319
interproc.c [OCRS][without] 1 PASS
0.319
mult.c [OCRS][without] 1 PASS
PASS
0.328
pointer_arith.c [OCRS][without] 1 PASS
PASS
PASS
PASS
0.315
quotient.c [OCRS][without] 3 PASS
0.414
subtract.c [OCRS][without] 1 PASS
0.311
sum01_bug02_sum01_bug02_base.case_unsafe.c [OCRS][without] 1 PASS
0.35
sum01_bug02_unsafe.c [OCRS][without] 1 PASS
0.383
sum01_real_safe.c [OCRS][without] 1 PASS
0.313
sum01_safe.c [OCRS][without] 1 PASS
0.327
sum01_unsafe.c [OCRS][without] 1 PASS
0.36
sum02_safe.c [OCRS][without] 1 PASS
0.333
sum03_safe.c [OCRS][without] 1 PASS
0.345
sum03_unsafe.c [OCRS][without] 1 PASS
0.398
sum04_safe.c [OCRS][without] 1 PASS
0.315
sum04_unsafe.c [OCRS][without] 1 PASS
0.347
terminator_02_safe.c [OCRS][without] 1 PASS
0.326
terminator_02_unsafe.c [OCRS][without] 1 PASS
0.356
terminator_03_safe.c [OCRS][without] 1 PASS
0.339
terminator_03_unsafe.c [OCRS][without] 1 PASS
0.327
token_ring01_safe.c [OCRS][without] TIMEOUT
300.005
token_ring01_unsafe.c [OCRS][without] TIMEOUT
300.007
toy_safe.c [OCRS][without] EXCEPTION
143.4 (167.13)
trex01_safe.c [OCRS][without] 1 PASS
0.731
trex01_unsafe.c [OCRS][without] 1 PASS
0.396
trex02_safe2.c [OCRS][without] 3 PASS
0.39
trex02_safe.c [OCRS][without] 3 PASS
0.383
trex02_unsafe.c [OCRS][without] 3 PASS
0.399
trex03_safe.c [OCRS][without] 1 PASS
0.486 (0.42)
trex03_unsafe.c [OCRS][without] 1 PASS
0.466
trex04_safe.c [OCRS][without] 1 PASS
0.349
while_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.319
while_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.312
while_infinite_loop_3_safe.c [OCRS][without] 1 PASS
0.308
Total Below Time = 756.428 (was 780.027)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c [OCRS][without] 3 PASS
0.448
blogger_simplified1.c [OCRS][without] 3 PASS
1.015
divided_difference2.c [OCRS][without] TIMEOUT
300.004
mult-proc.c [OCRS][without] 3 PASS
PASS
0.363
mult-proc-params.c [OCRS][without] 3 PASS
PASS
0.407
popall.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
0.406
simulated_scc.c [OCRS][without] 1 PASS
PASS
0.528
Total Below Time = 303.171 (was 303.144)
/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.468
degree2_monomial.c [OCRS][without] 1 PASS
0.369
degree3_binomial.c [OCRS][without] 1 PASS
0.898 (0.815)
degree3_monomial.c [OCRS][without] 1 PASS
0.442
degree4_binomial.c [OCRS][without] 1 PASS
1.173
degree4_monomial.c [OCRS][without] 1 PASS
0.48
degree5_binomial.c [OCRS][without] 1 PASS
1.768
degree5_monomial.c [OCRS][without] 1 PASS
0.578
Total Below Time = 6.508 (was 6.437)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c [OCRS][without] 1 PASS
0.341
cubic_with_square_interproc.c [OCRS][without] 2 PASS
0.385
cubic_with_square_nonlinear.c [OCRS][without] 1 PASS
0.35
cubic_with_square_nonlinear_interproc.c [OCRS][without] 2 PASS
0.381
cubic_with_square_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.373
cubic_with_square_unsafe.c [OCRS][without] 1 PASS
0.355
multi-input.c [OCRS][without] 1 PASS
0.445 (0.385)
multi-input_unsafe.c [OCRS][without] 1 PASS
0.444
nondet_loop_bound.c [OCRS][without] 1 PASS
0.37
nondet_loop_bound_quartic.c [OCRS][without] 1 PASS
0.371
nondet_loop_bound_quartic_unsafe.c [OCRS][without] 1 PASS
0.351
nondet_loop_bound_unsafe.c [OCRS][without] 1 PASS
0.382
nonlinear_stratified.c [OCRS][without] 1 FAIL
0.367
nonlinear_stratified_unsafe.c [OCRS][without] 1 PASS
0.37
quartic_with_cube.c [OCRS][without] 1 PASS
0.352
quartic_with_cube_nonlinear.c [OCRS][without] 1 PASS
0.361
quartic_with_cube_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.37
quartic_with_cube_unsafe.c [OCRS][without] 1 PASS
0.354
quintic_with_quartic.c [OCRS][without] 1 PASS
0.374
quintic_with_quartic_nonlinear.c [OCRS][without] 1 PASS
0.391
quintic_with_quartic_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.381 (0.476)
quintic_with_quartic_unsafe.c [OCRS][without] 1 PASS
0.357
Total Below Time = 8.225 (was 8.172)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c [OCRS][without] 1 PASS
0.518
degree2_FD_AllAux_AllAssm.c [OCRS][without] 1 PASS
3.676 (3.131)
degree2_FD_AllAux_FewAssm.c [OCRS][without] 1 PASS
5.493 (3.102)
degree2_FD_FewAux_FewAssm.c [OCRS][without] 1 PASS
0.695
degree2_FD_FewAux_FewAssm_NonLinAsrt.c [OCRS][without] 1 PASS
0.711
degree3.c [OCRS][without] 1 PASS
0.569
degree3_FD.c [OCRS][without] 1 PASS
0.701
degree4.c [OCRS][without] 1 PASS
0.386
Total Below Time = 12.749 (was 9.75)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c [OCRS][without] 1 PASS
0.389
loop_unsafe.c [OCRS][without] 1 PASS
0.41
simulated_lese_parser.c [OCRS][without] 1 PASS
0.335
simulated_lese_sentinel.c [OCRS][without] 1 PASS
0.337
Total Below Time = 1.471 (was 1.459)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c [OCRS][without] 1 PASS
PASS
PASS
0.337
Total Below Time = 0.337 (was 0.326)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c [OCRS][without] TIMEOUT
300.015
Total Below Time = 300.015 (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.344
array_false-unreach-call2.c [OCRS][without] 1 PASS
0.355
array_false-unreach-call3.c [OCRS][without] 1 PASS
0.336
array_true-unreach-call1.c [OCRS][without] 1 FAIL
0.349
array_true-unreach-call2.c [OCRS][without] 1 FAIL
0.375
array_true-unreach-call3.c [OCRS][without] 1 PASS
0.337
array_true-unreach-call4.c [OCRS][without] 1 FAIL
0.34
const_false-unreach-call1.c [OCRS][without] 1 PASS
0.328
const_true-unreach-call1.c [OCRS][without] 1 PASS
0.319
diamond_false-unreach-call1.c [OCRS][without] 1 PASS
0.332
diamond_true-unreach-call1.c [OCRS][without] 1 PASS
0.338
diamond_true-unreach-call2.c [OCRS][without] 1 PASS
0.37
functions_false-unreach-call1.c [OCRS][without] 3 PASS
0.372
functions_true-unreach-call1.c [OCRS][without] 3 PASS
0.358
multivar_false-unreach-call1.c [OCRS][without] 1 PASS
0.332
multivar_true-unreach-call1.c [OCRS][without] 1 PASS
0.333
nested_false-unreach-call1.c [OCRS][without] 1 PASS
0.33
nested_true-unreach-call1.c [OCRS][without] 1 PASS
0.332
overflow_true-unreach-call1.c [OCRS][without] 1 PASS
0.313
phases_false-unreach-call1.c [OCRS][without] 1 PASS
0.336
phases_false-unreach-call2.c [OCRS][without] 1 PASS
0.34
phases_true-unreach-call1.c [OCRS][without] 1 PASS
0.327
phases_true-unreach-call2.c [OCRS][without] 1 PASS
0.35
simple_false-unreach-call1.c [OCRS][without] 1 PASS
0.323
simple_false-unreach-call2.c [OCRS][without] 1 PASS
0.331
simple_false-unreach-call3.c [OCRS][without] 1 PASS
0.336
simple_false-unreach-call4.c [OCRS][without] 1 PASS
0.324
simple_true-unreach-call1.c [OCRS][without] 1 PASS
0.331
simple_true-unreach-call2.c [OCRS][without] 1 PASS
0.321
simple_true-unreach-call3.c [OCRS][without] 1 PASS
0.314
simple_true-unreach-call4.c [OCRS][without] 1 PASS
0.32
underapprox_false-unreach-call1.c [OCRS][without] 1 PASS
0.327
underapprox_false-unreach-call2.c [OCRS][without] 1 PASS
0.336
underapprox_true-unreach-call1.c [OCRS][without] 1 FAIL
0.323
underapprox_true-unreach-call2.c [OCRS][without] 1 PASS
0.319
Total Below Time = 11.751 (was 11.68)
/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.873
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.46
down_true-unreach-call.c [OCRS][without] 1 PASS
0.34
fragtest_simple_true-unreach-call.c [OCRS][without] 1 PASS
0.377
half_2_true-unreach-call.c [OCRS][without] 1 PASS
0.349
heapsort_true-unreach-call.c [OCRS][without] 1 TIMEOUT
300.156 (2.502)
id_build_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.328
id_trans_false-unreach-call.c [OCRS][without] 1 FAIL
FAIL
FAIL
PASS
0.327
large_const_true-unreach-call.c [OCRS][without] 1 PASS
0.422
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.429
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.34
sendmail-close-angle_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.377
seq_true-unreach-call.c [OCRS][without] 1 PASS
0.366
SpamAssassin-loop_true-unreach-call.c [OCRS][without] TIMEOUT
300.115 (1.202)
string_concat-noarr_true-unreach-call.c [OCRS][without] 1 PASS
0.343
up_true-unreach-call.c [OCRS][without] 1 PASS
0.337
Total Below Time = 607.176 (was 10.551)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c [OCRS][without] 1 PASS
0.345
bhmr2007_true-unreach-call.c [OCRS][without] 1 PASS
0.361
cggmp2005b_true-unreach-call.c [OCRS][without] 1 PASS
0.396
cggmp2005_true-unreach-call.c [OCRS][without] 1 PASS
0.319
cggmp2005_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.329
css2003_true-unreach-call.c [OCRS][without] 1 PASS
0.476
ddlm2013_true-unreach-call.c [OCRS][without] 1 PASS
0.389
gcnr2008_false-unreach-call.c [OCRS][without] 1 TIMEOUT
300.168 (0.841)
gj2007b_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
0.347
gj2007_true-unreach-call.c [OCRS][without] 1 PASS
0.338
gr2006_true-unreach-call.c [OCRS][without] 1 PASS
0.342
gsv2008_true-unreach-call.c [OCRS][without] 1 PASS
0.325
hhk2008_true-unreach-call.c [OCRS][without] 1 PASS
0.333
jm2006_true-unreach-call.c [OCRS][without] 1 PASS
0.351
jm2006_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.367
mcmillan2006_true-unreach-call.c [OCRS][without] 1 FAIL
0.39
Total Below Time = 305.576 (was 6.136)
/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.336
count_by_1_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.327
count_by_2_true-unreach-call.c [OCRS][without] 1 PASS
0.318
count_by_k_true-unreach-call.c [OCRS][without] 1 PASS
0.329
count_by_nondet_true-unreach-call.c [OCRS][without] 1 FAIL
0.341
gauss_sum_true-unreach-call.c [OCRS][without] 1 PASS
0.344
half_true-unreach-call.c [OCRS][without] EXCEPTION
0.336
nested_true-unreach-call.c [OCRS][without] 1 PASS
0.38
Total Below Time = 2.711 (was 2.687)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c [OCRS][without] 1 PASS
0.422
array_true-unreach-call.c [OCRS][without] 1 FAIL
0.415
bubble_sort_false-unreach-call.c [OCRS][without] 4 PASS
PASS
140.538
bubble_sort_true-unreach-call.c [OCRS][without] 1 3.908
compact_false-unreach-call.c [OCRS][without] 1 PASS
0.383
count_up_down_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.327
count_up_down_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.323
eureka_01_false-unreach-call.c [OCRS][without] 1 PASS
2.173
eureka_01_true-unreach-call.c [OCRS][without] 1 FAIL
1.947
eureka_05_true-unreach-call.c [OCRS][without] 1 FAIL
1.067 (0.724)
for_bounded_loop1_false-unreach-call_true-termination.c [OCRS][without] 1 FAIL
FAIL
PASS
0.326
for_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.302
for_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.312
heavy_false-unreach-call.c [OCRS][without] 1 PASS
0.534
heavy_true-unreach-call.c [OCRS][without] 1 PASS
0.513
insertion_sort_false-unreach-call.c [OCRS][without] 1 PASS
2.16
insertion_sort_true-unreach-call.c [OCRS][without] 1 FAIL
0.782
invert_string_false-unreach-call.c [OCRS][without] 1 PASS
0.49
invert_string_true-unreach-call.c [OCRS][without] 1 FAIL
0.498
linear_sea.ch_true-unreach-call.c [OCRS][without] 1 FAIL
0.367
linear_search_false-unreach-call.c [OCRS][without] 1 EXCEPTION
0.399
lu.cmp_true-unreach-call.c [OCRS][without] TIMEOUT
300.271 (121.918)
ludcmp_false-unreach-call.c [OCRS][without] TIMEOUT
300.286 (125.744)
matrix_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
1.225 (0.829)
matrix_true-unreach-call_true-termination.c [OCRS][without] 1 FAIL
0.527
n.c11_true-unreach-call.c [OCRS][without] 3 FAIL
0.482
n.c24_false-unreach-call.c [OCRS][without] 3 PASS
23.502
n.c40_true-unreach-call.c [OCRS][without] 1 FAIL
0.378
nec11_false-unreach-call.c [OCRS][without] 1 PASS
0.382
nec20_false-unreach-call.c [OCRS][without] 1 PASS
0.365
nec40_true-unreach-call.c [OCRS][without] 1 FAIL
0.364
string_false-unreach-call.c [OCRS][without] 1 PASS
0.658
string_true-unreach-call.c [OCRS][without] 1 FAIL
0.652
sum01_bug02_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.385
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.353
sum01_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.366
sum01_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.324
sum03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.461
sum03_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.36
sum04_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.373
sum04_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.327
sum_array_false-unreach-call.c [OCRS][without] 1 PASS
0.66
sum_array_true-unreach-call.c [OCRS][without] 1 FAIL
0.734
terminator_01_false-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.337
terminator_02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.428
terminator_02_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.355
terminator_03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.342
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.822 (0.659)
trex02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.396
trex02_true-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.398
trex03_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.875 (0.778)
trex03_true-unreach-call.c [OCRS][without] 3 PASS
0.848
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.335
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c [OCRS][without] 3 24.934
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c [OCRS][without] 1 PASS
0.365
verisec_NetBSD-libc__loop_false-unreach-call.c [OCRS][without] 1 PASS
0.352
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c [OCRS][without] 3 PASS
17.286
vogal_false-unreach-call.c [OCRS][without] 1 PASS
0.883 (0.743)
vogal_true-unreach-call.c [OCRS][without] 1 FAIL
0.896 (0.779)
while_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.308
while_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.324
while_infinite_loop_3_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.316
while_infinite_loop_4_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.326
Total Below Time = 843.918 (was 487.59)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c [OCRS][without] TIMEOUT
300.033 (2.416)
Ackermann02_false-unreach-call_false-termination.c [OCRS][without] TIMEOUT
300.033 (2.341)
Ackermann03_true-unreach-call.c [OCRS][without] TIMEOUT
300.025 (2.421)
Ackermann04_true-unreach-call.c [OCRS][without] TIMEOUT
300.021 (2.4)
Addition01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.578
Addition02_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.582
Addition03_false-no-overflow.c [OCRS][without] 2 PASS
0.566
Addition03_true-unreach-call.c [OCRS][without] 2 PASS
0.567
BallRajamani-SPIN2000-Fig1_false-unreach-call.c [OCRS][without] 2 PASS
0.45
EvenOdd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.425
EvenOdd03_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.444
Fibonacci01_true-unreach-call.c [OCRS][without] EXCEPTION
0.984 (300.008)
Fibonacci02_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.989 (300.009)
Fibonacci03_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
1.032 (300.006)
Fibonacci04_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.983 (300.01)
Fibonacci05_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.992 (300.007)
gcd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.567
gcd02_true-unreach-call.c [OCRS][without] 2 FAIL
PASS
1.366 (1.165)
McCarthy91_false-unreach-call_false-termination.c [OCRS][without] 7 PASS
1.479 (1.126)
McCarthy91_true-unreach-call.c [OCRS][without] 7 FAIL
1.432 (1.128)
MultCommutative_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.672 (0.597)
Primes_true-unreach-call.c [OCRS][without] 3 FAIL
2.142
recHanoi01_true-unreach-call_true-termination.c [OCRS][without] 9 FAIL
6.042
recHanoi02_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.375
recHanoi03_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.39
Total Below Time = 1223.169 (was 1526.281)
/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.424
afterrec_2calls_true-unreach-call.c [OCRS][without] 2 PASS
PASS
0.373
afterrec_false-unreach-call.c [OCRS][without] 2 PASS
0.356
afterrec_true-unreach-call.c [OCRS][without] 2 PASS
0.348
fibo_10_false-unreach-call.c [OCRS][without] EXCEPTION
0.958 (300.005)
fibo_10_true-unreach-call.c [OCRS][without] EXCEPTION
0.966 (300.008)
fibo_15_false-unreach-call.c [OCRS][without] EXCEPTION
0.976 (300.009)
fibo_15_true-unreach-call.c [OCRS][without] EXCEPTION
0.969 (300.009)
fibo_20_false-unreach-call.c [OCRS][without] EXCEPTION
0.981 (300.008)
fibo_20_true-unreach-call.c [OCRS][without] EXCEPTION
0.955 (300.007)
fibo_25_false-unreach-call.c [OCRS][without] EXCEPTION
0.979 (300.007)
fibo_25_true-unreach-call.c [OCRS][without] EXCEPTION
0.975 (300.009)
fibo_2calls_10_false-unreach-call.c [OCRS][without] EXCEPTION
17.805 (131.705)
fibo_2calls_10_true-unreach-call.c [OCRS][without] EXCEPTION
17.728 (131.34)
fibo_2calls_15_false-unreach-call.c [OCRS][without] EXCEPTION
17.423 (130.259)
fibo_2calls_15_true-unreach-call.c [OCRS][without] EXCEPTION
17.834 (130.725)
fibo_2calls_20_false-unreach-call.c [OCRS][without] EXCEPTION
17.611 (128.131)
fibo_2calls_20_true-unreach-call.c [OCRS][without] EXCEPTION
17.627 (130.813)
fibo_2calls_25_false-unreach-call.c [OCRS][without] EXCEPTION
17.602 (131.892)
fibo_2calls_25_true-unreach-call.c [OCRS][without] EXCEPTION
17.617 (128.511)
fibo_2calls_2_false-unreach-call.c [OCRS][without] EXCEPTION
17.704 (129.243)
fibo_2calls_2_true-unreach-call.c [OCRS][without] EXCEPTION
17.575 (130.747)
fibo_2calls_4_false-unreach-call.c [OCRS][without] EXCEPTION
17.41 (130.997)
fibo_2calls_4_true-unreach-call.c [OCRS][without] EXCEPTION
17.701 (129.391)
fibo_2calls_5_false-unreach-call.c [OCRS][without] EXCEPTION
17.651 (130.356)
fibo_2calls_5_true-unreach-call.c [OCRS][without] EXCEPTION
17.68 (129.497)
fibo_2calls_6_false-unreach-call.c [OCRS][without] EXCEPTION
17.477 (128.993)
fibo_2calls_6_true-unreach-call.c [OCRS][without] EXCEPTION
17.586 (131.203)
fibo_2calls_8_false-unreach-call.c [OCRS][without] EXCEPTION
17.641 (130.384)
fibo_2calls_8_true-unreach-call.c [OCRS][without] EXCEPTION
17.499 (130.287)
fibo_5_false-unreach-call.c [OCRS][without] EXCEPTION
0.947 (300.009)
fibo_5_true-unreach-call.c [OCRS][without] EXCEPTION
0.944 (300.01)
fibo_7_false-unreach-call.c [OCRS][without] EXCEPTION
0.982 (300.007)
fibo_7_true-unreach-call.c [OCRS][without] EXCEPTION
0.92 (300.007)
id2_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.942
id2_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
1.04
id2_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.944
id2_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.979
id2_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.44
id2_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.408
id_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.582
id_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.597
id_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.595
id_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.582
id_i10_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.383
id_i10_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.362
id_i15_o15_false-unreach-call.c [OCRS][without] 2 PASS
0.383
id_i15_o15_true-unreach-call.c [OCRS][without] 2 PASS
0.362
id_i20_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.362
id_i20_o20_true-unreach-call.c [OCRS][without] 2 PASS
0.378
id_i25_o25_false-unreach-call.c [OCRS][without] 2 PASS
0.375
id_i25_o25_true-unreach-call.c [OCRS][without] 2 PASS
0.383
id_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.385
id_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.371
id_o1000_false-unreach-call.c [OCRS][without] 2 PASS
0.388
id_o100_false-unreach-call.c [OCRS][without] 2 PASS
0.377
id_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.402
id_o200_false-unreach-call.c [OCRS][without] 2 PASS
0.399
id_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.394
id_o3_false-unreach-call.c [OCRS][without] 2 PASS
0.384
sum_10x0_false-unreach-call.c [OCRS][without] 2 PASS
0.395
sum_10x0_true-unreach-call.c [OCRS][without] 2 PASS
0.389
sum_15x0_false-unreach-call.c [OCRS][without] 2 PASS
0.412
sum_15x0_true-unreach-call.c [OCRS][without] 2 PASS
0.389
sum_20x0_false-unreach-call.c [OCRS][without] 2 PASS
0.399
sum_20x0_true-unreach-call.c [OCRS][without] 2 PASS
0.376
sum_25x0_false-unreach-call.c [OCRS][without] 2 PASS
0.382
sum_25x0_true-unreach-call.c [OCRS][without] 2 PASS
0.388
sum_2x3_false-unreach-call.c [OCRS][without] 2 PASS
0.395
sum_2x3_true-unreach-call.c [OCRS][without] 2 PASS
0.375
sum_non_eq_false-unreach-call.c [OCRS][without] 2 PASS
0.444
sum_non_eq_true-unreach-call.c [OCRS][without] 2 PASS
0.407
sum_non_false-unreach-call.c [OCRS][without] 2 PASS
0.397
sum_non_true-unreach-call.c [OCRS][without] 2 PASS
0.386
Total Below Time = 348.955 (was 5964.319)
/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.387
rec-bhmr2007_true-unreach-call.c [OCRS][without] 2 PASS
0.401
rec-cggmp2005b_true-unreach-call.c [OCRS][without] 3 PASS
0.771
rec-cggmp2005_true-unreach-call.c [OCRS][without] 2 PASS
0.344
rec-cggmp2005_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.357
rec-css2003_true-unreach-call.c [OCRS][without] 2 PASS
0.625
rec-ddlm2013_true-unreach-call.c [OCRS][without] EXCEPTION
0.35 (0.446)
rec-gcnr2008_false-unreach-call.c [OCRS][without] 2 PASS
0.919
rec-gj2007b_true-unreach-call.c [OCRS][without] 2 FAIL
FAIL
0.379
rec-gj2007_true-unreach-call.c [OCRS][without] 2 FAIL
0.367
rec-gr2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.399
rec-gsv2008_true-unreach-call.c [OCRS][without] 2 PASS
0.342
rec-hhk2008_true-unreach-call.c [OCRS][without] 2 PASS
0.354
rec-jm2006_true-unreach-call.c [OCRS][without] 2 PASS
0.368
rec-jm2006_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.39
rec-mcmillan2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.422
Total Below Time = 7.175 (was 7.091)
/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.327
rec-count_by_1_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.346
rec-count_by_2_true-unreach-call.c [OCRS][without] 2 PASS
0.334
rec-count_by_k_true-unreach-call.c [OCRS][without] 2 PASS
0.369
rec-count_by_nondet_true-unreach-call.c [OCRS][without] 2 FAIL
0.389
rec-gauss_sum_true-unreach-call.c [OCRS][without] 2 PASS
0.355
rec-half_true-unreach-call.c [OCRS][without] EXCEPTION
0.337 (0.39)
rec-nested_true-unreach-call.c [OCRS][without] 3 PASS
0.601
Total Below Time = 3.058 (was 3.095)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c [OCRS][without] 2 PASS
0.514
edit_distance_bottom_up.c [OCRS][without] 3 TIMEOUT
300.008
edit_distance_top_down.c [OCRS][without] 3 FAIL
50.39
log_log_n_solution.c [OCRS][without] 3 FAIL
0.446 (0.834)
log_n_solution.c [OCRS][without] 2 FAIL
0.467
multivariate_1.c [OCRS][without] TIMEOUT
300.006
multivariate_higher_order.c [OCRS][without] 7 FAIL
FAIL
FAIL
26.566
n_cubed_solution.c [OCRS][without] EXCEPTION
0.33
n_log_n_solution.c [OCRS][without] TIMEOUT
300.037 (1.863)
n_squared_two_base_case_even.c [OCRS][without] 2 PASS
0.38 (0.426)
n_squared_two_base_case_odd.c [OCRS][without] 2 PASS
0.383
pascals_dynamic.c [OCRS][without] 3 FAIL
20.795
pascals_iterative.c [OCRS][without] 1 FAIL
5.623 (6.317)
pascals_recursive.c [OCRS][without] TIMEOUT
300.005
squared_solution.c [OCRS][without] TIMEOUT
300.134 (12.364)
two_n_even.c [OCRS][without] 2 PASS
0.366
two_n_odd.c [OCRS][without] 2 PASS
0.375
two_to_n_over_two_even.c [OCRS][without] TIMEOUT
300.023 (44.502)
two_to_n_over_two_odd.c [OCRS][without] TIMEOUT
300.022 (44.868)
two_to_n_squared.c [OCRS][without] 8 TIMEOUT
300.006 (134.689)
two_to_two_to_n.c [OCRS][without] 7 FAIL
1.66
Total Below Time = 2508.536 (was 1246.02)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c [OCRS][without] 1 PASS
0.318
exp_add_loop_rec.c [OCRS][without] 1 FAIL
0.352
exp_add_loop_variable.c [OCRS][without] 1 PASS
0.34
exp_with_linear_inner_loop.c [OCRS][without] 1 FAIL
0.42
linear_two_to_n.c [OCRS][without] 8 FAIL
1.526
loop_five_to_n.c [OCRS][without] 1 FAIL
0.346
non_loop_five_to_n.c [OCRS][without] 8 FAIL
10.153 (8.788)
power_log.c [OCRS][without] 1 PASS
0.406
power_log_modified.c [OCRS][without] 1 PASS
0.476 (0.38)
simple_exponential.c [OCRS][without] 1 PASS
0.342
simple_exponential_for.c [OCRS][without] 1 PASS
0.338
two_to_n_minus_n.c [OCRS][without] 8 FAIL
1.758
two_to_n_minus_n_loop.c [OCRS][without] 8 FAIL
2.88 (2.578)
Total Below Time = 19.655 (was 17.621)

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