[Version Information]
Phase2 (IST-Java-ICRA) WALi-OpenNWA version: 0f994ef6a5cbe02200899575605ae35f227d9ddb (2017-07-12 11:45:09 -0500) "Added programs and files used for POPL18"
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: 0f994ef6a5cbe02200899575605ae35f227d9ddb (2017-07-12 11:45:09 -0500) "Added programs and files used for POPL18"
Phase3 duet version: 81b6696f6f312fabfa1611e9943c2a6ea2f1ed79 (2017-07-20 23:59:08 +0200) "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-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.5.3  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
camlp4               4.02+7  Camlp4 is a system for writing extensible parsers f
cil                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
conf-which                1  Virtual package relying on which
cppo                  1.4.1  Equivalent of the C preprocessor for OCaml programs
deriving           20140904  Extension to OCaml for deriving functions from type
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170101  LR(1) parser generator
mlgmpidl              1.2.4  OCaml interface to the GMP library
num                       0  The Num library for arbitrary-precision integer and
oasis                 0.4.8  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.7.1  A library manager for OCaml
ocamlgraph            1.8.7  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.8  Generate OCaml modules from source files
OCRS             20170627v3  Recurrence solver based on operational calculus
optcomp                 1.6  Optional compilation with cpp-like directives
ounit                 2.0.0  Unit testing framework loosely based on HUnit. It i
ppx_deriving            4.1  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
result                  1.2  Compatibility Result module
Z3                 20161217  Z3 SMT solver

Test Name Output No. of Rounds Result Time (Prev.)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c [OCRS][without] 1 FAIL
0.378
kmp.c [OCRS][without] 1 PASS
1.716 (0.735)
qsort.c [OCRS][without] 5 PASS
0.911 (0.702)
speed_pldi09_fig1.c [OCRS][without] 1 PASS
0.512 (0.375)
speed_pldi09_fig4_2.c [OCRS][without] 1 FAIL
0.383
speed_pldi09_fig4_4.c [OCRS][without] 1 PASS
4.826 (0.429)
speed_pldi09_fig4_5.c [OCRS][without] 1 PASS
0.399 (0.355)
speed_pldi10_ex1.c [OCRS][without] 1 PASS
1.263 (0.644)
speed_pldi10_ex3.c [OCRS][without] 1 PASS
0.481 (0.433)
speed_pldi10_ex4.c [OCRS][without] 1 PASS
0.534 (0.375)
speed_popl10_fig2_1.c [OCRS][without] 1 PASS
0.452 (0.372)
speed_popl10_fig2_2.c [OCRS][without] 1 FAIL
0.368
speed_popl10_nested_multiple.c [OCRS][without] 1 PASS
0.453 (0.378)
speed_popl10_nested_single.c [OCRS][without] 1 PASS
0.44 (0.376)
speed_popl10_sequential_single.c [OCRS][without] 1 PASS
0.402 (0.364)
speed_popl10_simple_multiple.c [OCRS][without] 1 PASS
0.528 (0.378)
speed_popl10_simple_single_2.c [OCRS][without] 1 PASS
0.617 (0.397)
speed_popl10_simple_single.c [OCRS][without] 1 PASS
0.352
t07.c [OCRS][without] 1 PASS
0.43 (0.36)
t08.c [OCRS][without] 1 PASS
0.392 (0.339)
t09.c [OCRS][without] 1 PASS
0.391 (0.341)
t10.c [OCRS][without] 1 PASS
0.349
t11.c [OCRS][without] 1 PASS
0.461 (0.376)
t13.c [OCRS][without] 1 FAIL
0.412
t15.c [OCRS][without] 1 PASS
0.443 (0.369)
t16.c [OCRS][without] 1 PASS
0.408 (0.365)
t19.c [OCRS][without] 1 PASS
0.39 (0.348)
t20.c [OCRS][without] 1 PASS
0.38
t27.c [OCRS][without] 1 PASS
0.545 (0.386)
t28.c [OCRS][without] 1 PASS
0.469 (0.382)
t30.c [OCRS][without] 1 FAIL
0.421 (0.342)
t37.c [OCRS][without] 2 PASS
0.631 (0.446)
t39.c [OCRS][without] 2 PASS
0.52 (0.421)
t46.c [OCRS][without] 1 PASS
0.431 (0.359)
t47.c [OCRS][without] 1 FAIL
0.556 (0.369)
Total Below Time = 22.644 (was 13.969)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c [OCRS][without] 2 PASS
PASS
0.376
qsort_full.c [OCRS][without] 4 PASS
PASS
PASS
PASS
PASS
PASS
6.338
rec1-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.383 (0.348)
rec1-param_unsafe.c [OCRS][without] 2 OKAY
0.391 (0.337)
rec1_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.38 (0.331)
rec1_unsafe.c [OCRS][without] 2 OKAY
0.372 (0.328)
rec2-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.371
rec2-param_unsafe.c [OCRS][without] 2 OKAY
0.368
rec2_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.373 (0.33)
rec2_unsafe.c [OCRS][without] 2 OKAY
0.36 (0.317)
rec-test.c [OCRS][without] 2 PASS
0.382 (0.339)
sas03_bothbranches.c [OCRS][without] 7 PASS
0.706 (0.518)
sas03.c [OCRS][without] 2 PASS
0.738
simulated_lese_recursive.c [OCRS][without] 2 PASS
0.453 (0.373)
Total Below Time = 11.991 (was 11.099)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c [OCRS][without] 1 PASS
0.336
count_up_down_unsafe.c [OCRS][without] 1 OKAY
0.345
divide.c [OCRS][without] 1 PASS
0.343
factor_unsafe.c [OCRS][without] 1 OKAY
0.328
for_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.32
for_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.311
interproc.c [OCRS][without] 1 PASS
0.31
mult.c [OCRS][without] 1 PASS
PASS
0.326
pointer_arith.c [OCRS][without] 1 PASS
PASS
PASS
PASS
0.305
quotient.c [OCRS][without] 3 PASS
0.491 (0.388)
subtract.c [OCRS][without] 1 PASS
0.319
sum01_bug02_sum01_bug02_base.case_unsafe.c [OCRS][without] 1 OKAY
0.338
sum01_bug02_unsafe.c [OCRS][without] 1 OKAY
0.61 (0.363)
sum01_real_safe.c [OCRS][without] 1 PASS
0.337
sum01_safe.c [OCRS][without] 1 PASS
0.349
sum01_unsafe.c [OCRS][without] 1 OKAY
0.459 (0.349)
sum02_safe.c [OCRS][without] 1 PASS
0.365 (0.33)
sum03_safe.c [OCRS][without] 1 PASS
0.406 (0.335)
sum03_unsafe.c [OCRS][without] 1 OKAY
0.48 (0.357)
sum04_safe.c [OCRS][without] 1 PASS
0.358 (0.322)
sum04_unsafe.c [OCRS][without] 1 OKAY
0.471 (0.34)
terminator_02_safe.c [OCRS][without] 1 PASS
0.324
terminator_02_unsafe.c [OCRS][without] 1 OKAY
0.34
terminator_03_safe.c [OCRS][without] 1 PASS
0.332
terminator_03_unsafe.c [OCRS][without] 1 OKAY
0.338
token_ring01_safe.c [OCRS][without] 4 FAIL
100.613 (59.917)
token_ring01_unsafe.c [OCRS][without] 4 OKAY
256.997 (83.954)
toy_safe.c [OCRS][without] EXCEPTION
168.063
trex01_safe.c [OCRS][without] 1 PASS
0.523
trex01_unsafe.c [OCRS][without] 1 OKAY
0.368
trex02_safe2.c [OCRS][without] 3 PASS
0.391
trex02_safe.c [OCRS][without] 3 PASS
0.397 (0.358)
trex02_unsafe.c [OCRS][without] 3 OKAY
0.404
trex03_safe.c [OCRS][without] 1 PASS
0.426
trex03_unsafe.c [OCRS][without] 1 OKAY
0.422
trex04_safe.c [OCRS][without] 1 PASS
0.355
while_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.308
while_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.317
while_infinite_loop_3_safe.c [OCRS][without] 1 PASS
0.316
Total Below Time = 539.141 (was 315.466)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c [OCRS][without] 3 PASS
0.377
blogger_simplified1.c [OCRS][without] 3 PASS
1.075 (0.773)
divided_difference2.c [OCRS][without] TIMEOUT
300.007
mult-proc.c [OCRS][without] 3 PASS
PASS
0.38
mult-proc-params.c [OCRS][without] 3 PASS
PASS
0.378
popall.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
0.716 (0.394)
simulated_scc.c [OCRS][without] 1 PASS
PASS
0.62 (0.448)
Total Below Time = 303.553 (was 302.705)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c [OCRS][without] 1 PASS
0.349
degree2_binomial.c [OCRS][without] 1 FAIL
0.822 (0.419)
degree2_monomial.c [OCRS][without] 1 PASS
0.375
degree3_binomial.c [OCRS][without] 1 FAIL
1.341 (0.827)
degree3_monomial.c [OCRS][without] 1 PASS
0.44 (0.379)
degree4_binomial.c [OCRS][without] 1 FAIL
3.024 (1.164)
degree4_monomial.c [OCRS][without] 1 PASS
0.49
degree5_binomial.c [OCRS][without] 1 FAIL
9.251 (1.476)
degree5_monomial.c [OCRS][without] 1 PASS
0.554
Total Below Time = 16.646 (was 5.967)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c [OCRS][without] 1 PASS
0.454 (0.343)
cubic_with_square_interproc.c [OCRS][without] 2 FAIL
0.584 (0.4)
cubic_with_square_nonlinear.c [OCRS][without] 1 FAIL
0.387
cubic_with_square_nonlinear_interproc.c [OCRS][without] 2 FAIL
0.431 (0.391)
cubic_with_square_nonlinear_unsafe.c [OCRS][without] 1 OKAY
0.371
cubic_with_square_unsafe.c [OCRS][without] 1 OKAY
0.45 (0.359)
multi-input.c [OCRS][without] 1 PASS
214.23 (0.421)
multi-input_unsafe.c [OCRS][without] 1 OKAY
0.52 (0.421)
nondet_loop_bound.c [OCRS][without] 1 FAIL
0.363
nondet_loop_bound_quartic.c [OCRS][without] 1 FAIL
0.398
nondet_loop_bound_quartic_unsafe.c [OCRS][without] 1 OKAY
0.387
nondet_loop_bound_unsafe.c [OCRS][without] 1 OKAY
0.362
nonlinear_stratified.c [OCRS][without] 1 PASS
79.974 (0.353)
nonlinear_stratified_unsafe.c [OCRS][without] 1 TIMEOUT
300.004 (0.357)
quartic_with_cube.c [OCRS][without] 1 PASS
0.639 (0.376)
quartic_with_cube_nonlinear.c [OCRS][without] 1 FAIL
0.383
quartic_with_cube_nonlinear_unsafe.c [OCRS][without] 1 OKAY
0.404 (0.362)
quartic_with_cube_unsafe.c [OCRS][without] 1 OKAY
0.492 (0.375)
quintic_with_quartic.c [OCRS][without] 1 PASS
1.038 (0.36)
quintic_with_quartic_nonlinear.c [OCRS][without] 1 PASS
0.439 (0.384)
quintic_with_quartic_nonlinear_unsafe.c [OCRS][without] 1 OKAY
0.451 (0.379)
quintic_with_quartic_unsafe.c [OCRS][without] 1 OKAY
1.069 (0.386)
Total Below Time = 603.83 (was 8.161)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c [OCRS][without] 1 PASS
0.703 (0.449)
degree2_FD_AllAux_AllAssm.c [OCRS][without] 1 PASS
217.935 (1.798)
degree2_FD_AllAux_FewAssm.c [OCRS][without] 1 PASS
4.933 (1.782)
degree2_FD_FewAux_FewAssm.c [OCRS][without] 1 PASS
0.878 (0.584)
degree2_FD_FewAux_FewAssm_NonLinAsrt.c [OCRS][without] 1 PASS
0.888 (0.583)
degree3.c [OCRS][without] 1 PASS
0.652 (0.489)
degree3_FD.c [OCRS][without] 1 PASS
0.834 (0.611)
degree4.c [OCRS][without] 1 PASS
0.43 (0.388)
Total Below Time = 227.253 (was 6.684)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c [OCRS][without] 1 PASS
0.436 (0.379)
loop_unsafe.c [OCRS][without] 1 OKAY
0.439 (0.379)
simulated_lese_parser.c [OCRS][without] 1 PASS
0.344
simulated_lese_sentinel.c [OCRS][without] 1 PASS
0.356
Total Below Time = 1.575 (was 1.418)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c [OCRS][without] 1 PASS
PASS
PASS
0.347
Total Below Time = 0.347 (was 0.327)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c [OCRS][without] TIMEOUT
300.006
Total Below Time = 300.006 (was 300.006)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c [OCRS][without] 1 OKAY
0.339
array_false-unreach-call2.c [OCRS][without] 1 OKAY
0.353
array_false-unreach-call3.c [OCRS][without] 1 OKAY
0.348
array_true-unreach-call1.c [OCRS][without] 1 FAIL
0.367
array_true-unreach-call2.c [OCRS][without] 1 FAIL
0.356
array_true-unreach-call3.c [OCRS][without] 1 PASS
0.352
array_true-unreach-call4.c [OCRS][without] 1 FAIL
0.347
const_false-unreach-call1.c [OCRS][without] 1 OKAY
0.357 (0.317)
const_true-unreach-call1.c [OCRS][without] 1 PASS
0.344
diamond_false-unreach-call1.c [OCRS][without] 1 OKAY
0.36 (0.318)
diamond_true-unreach-call1.c [OCRS][without] 1 PASS
0.36 (0.32)
diamond_true-unreach-call2.c [OCRS][without] 1 PASS
0.377
functions_false-unreach-call1.c [OCRS][without] 3 OKAY
0.387 (0.34)
functions_true-unreach-call1.c [OCRS][without] 3 PASS
0.387 (0.341)
multivar_false-unreach-call1.c [OCRS][without] 1 OKAY
0.357 (0.309)
multivar_true-unreach-call1.c [OCRS][without] 1 PASS
0.344
nested_false-unreach-call1.c [OCRS][without] 1 OKAY
0.365 (0.328)
nested_true-unreach-call1.c [OCRS][without] 1 PASS
0.368 (0.325)
overflow_true-unreach-call1.c [OCRS][without] 1 PASS
0.324
phases_false-unreach-call1.c [OCRS][without] 1 OKAY
0.414 (0.328)
phases_false-unreach-call2.c [OCRS][without] 1 OKAY
0.331
phases_true-unreach-call1.c [OCRS][without] 1 PASS
0.39 (0.324)
phases_true-unreach-call2.c [OCRS][without] 1 PASS
0.337
simple_false-unreach-call1.c [OCRS][without] 1 OKAY
0.314
simple_false-unreach-call2.c [OCRS][without] 1 OKAY
0.319
simple_false-unreach-call3.c [OCRS][without] 1 OKAY
0.319
simple_false-unreach-call4.c [OCRS][without] 1 OKAY
0.323
simple_true-unreach-call1.c [OCRS][without] 1 PASS
0.337
simple_true-unreach-call2.c [OCRS][without] 1 PASS
0.313
simple_true-unreach-call3.c [OCRS][without] 1 PASS
0.319
simple_true-unreach-call4.c [OCRS][without] 1 PASS
0.329
underapprox_false-unreach-call1.c [OCRS][without] 1 OKAY
0.338
underapprox_false-unreach-call2.c [OCRS][without] 1 OKAY
0.334
underapprox_true-unreach-call1.c [OCRS][without] 1 FAIL
0.349
underapprox_true-unreach-call2.c [OCRS][without] 1 PASS
0.343
Total Below Time = 12.201 (was 11.452)
/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.842 (0.75)
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.411
down_true-unreach-call.c [OCRS][without] 1 PASS
0.367
fragtest_simple_true-unreach-call.c [OCRS][without] 1 PASS
0.435 (0.379)
half_2_true-unreach-call.c [OCRS][without] 1 PASS
0.387 (0.347)
heapsort_true-unreach-call.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
1.353
id_build_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.371 (0.327)
id_trans_false-unreach-call.c [OCRS][without] 1 UNSOUND
UNSOUND
UNSOUND
OKAY
0.334
large_const_true-unreach-call.c [OCRS][without] 1 PASS
0.426
MADWiFi-encode_ie_ok_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.386
nested6_true-unreach-call.c [OCRS][without] 1 FAIL
FAIL
PASS
0.51 (0.394)
nested9_true-unreach-call.c [OCRS][without] 1 PASS
0.494
nest-if3_true-unreach-call.c [OCRS][without] 1 PASS
0.472 (0.363)
NetBSD_loop_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.335
sendmail-close-angle_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.384
seq_true-unreach-call.c [OCRS][without] 1 PASS
0.417 (0.37)
SpamAssassin-loop_true-unreach-call.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
1.277 (1.001)
string_concat-noarr_true-unreach-call.c [OCRS][without] 1 PASS
0.394
up_true-unreach-call.c [OCRS][without] 1 PASS
0.381 (0.336)
Total Below Time = 9.976 (was 9.0)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c [OCRS][without] 1 PASS
0.364
bhmr2007_true-unreach-call.c [OCRS][without] 1 PASS
0.362
cggmp2005b_true-unreach-call.c [OCRS][without] 1 PASS
0.499 (0.364)
cggmp2005_true-unreach-call.c [OCRS][without] 1 PASS
0.349 (0.308)
cggmp2005_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.351
css2003_true-unreach-call.c [OCRS][without] 1 PASS
0.775 (0.457)
ddlm2013_true-unreach-call.c [OCRS][without] 1 PASS
0.501 (0.367)
gcnr2008_false-unreach-call.c [OCRS][without] 1 OKAY
0.921 (0.625)
gj2007b_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
0.376 (0.338)
gj2007_true-unreach-call.c [OCRS][without] 1 PASS
0.422 (0.343)
gr2006_true-unreach-call.c [OCRS][without] 1 PASS
0.455 (0.335)
gsv2008_true-unreach-call.c [OCRS][without] 1 PASS
0.357 (0.314)
hhk2008_true-unreach-call.c [OCRS][without] 1 PASS
0.334
jm2006_true-unreach-call.c [OCRS][without] 1 PASS
0.408 (0.352)
jm2006_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.463 (0.356)
mcmillan2006_true-unreach-call.c [OCRS][without] 1 FAIL
0.395
Total Below Time = 7.332 (was 5.909)
/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.376 (0.315)
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.324
count_by_nondet_true-unreach-call.c [OCRS][without] 1 FAIL
0.328
gauss_sum_true-unreach-call.c [OCRS][without] 1 PASS
0.368 (0.332)
half_true-unreach-call.c [OCRS][without] 1 FAIL
0.366
nested_true-unreach-call.c [OCRS][without] 1 PASS
0.407
Total Below Time = 2.823 (was 2.641)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c [OCRS][without] 1 OKAY
0.393
array_true-unreach-call.c [OCRS][without] 1 FAIL
0.39
bubble_sort_false-unreach-call.c [OCRS][without] 4 OKAY
OKAY
49.9 (70.056)
bubble_sort_true-unreach-call.c [OCRS][without] 1 3.761 (1.367)
compact_false-unreach-call.c [OCRS][without] 1 OKAY
0.387
count_up_down_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
0.342
count_up_down_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.327
eureka_01_false-unreach-call.c [OCRS][without] 1 OKAY
2.151 (1.441)
eureka_01_true-unreach-call.c [OCRS][without] 1 FAIL
1.494 (1.253)
eureka_05_true-unreach-call.c [OCRS][without] 1 FAIL
0.669 (0.543)
for_bounded_loop1_false-unreach-call_true-termination.c [OCRS][without] 1 UNSOUND
UNSOUND
OKAY
0.339
for_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.319
for_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.325
heavy_false-unreach-call.c [OCRS][without] 1 OKAY
0.469 (0.423)
heavy_true-unreach-call.c [OCRS][without] 1 PASS
0.452
insertion_sort_false-unreach-call.c [OCRS][without] 1 OKAY
1.735 (1.075)
insertion_sort_true-unreach-call.c [OCRS][without] 1 FAIL
0.583
invert_string_false-unreach-call.c [OCRS][without] 1 OKAY
0.505
invert_string_true-unreach-call.c [OCRS][without] 1 FAIL
0.527 (0.475)
linear_sea.ch_true-unreach-call.c [OCRS][without] 1 FAIL
0.371
linear_search_false-unreach-call.c [OCRS][without] 1 OKAY
0.391
lu.cmp_true-unreach-call.c [OCRS][without] 3 PASS
17.733 (9.969)
ludcmp_false-unreach-call.c [OCRS][without] 3 OKAY
18.354 (10.274)
matrix_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
1.078 (0.56)
matrix_true-unreach-call_true-termination.c [OCRS][without] 1 FAIL
0.414
n.c11_true-unreach-call.c [OCRS][without] 3 FAIL
0.432
n.c24_false-unreach-call.c [OCRS][without] 3 OKAY
2.846
n.c40_true-unreach-call.c [OCRS][without] 1 FAIL
0.367
nec11_false-unreach-call.c [OCRS][without] 1 OKAY
0.353
nec20_false-unreach-call.c [OCRS][without] 1 OKAY
0.373
nec40_true-unreach-call.c [OCRS][without] 1 FAIL
0.368
string_false-unreach-call.c [OCRS][without] 1 OKAY
0.608 (0.541)
string_true-unreach-call.c [OCRS][without] 1 FAIL
0.602 (0.519)
sum01_bug02_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
0.62 (0.372)
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
0.357
sum01_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
0.465 (0.349)
sum01_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.343
sum03_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
0.493 (0.412)
sum03_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.433 (0.334)
sum04_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
0.467 (0.345)
sum04_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.352
sum_array_false-unreach-call.c [OCRS][without] 1 OKAY
0.583
sum_array_true-unreach-call.c [OCRS][without] 1 FAIL
0.692 (0.604)
terminator_01_false-unreach-call_false-termination.c [OCRS][without] 1 OKAY
0.319
terminator_02_false-unreach-call_true-termination.c [OCRS][without] 3 OKAY
0.454 (0.378)
terminator_02_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.348
terminator_03_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
0.335
terminator_03_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.336
trex01_false-unreach-call_true-termination.c [OCRS][without] 3 OKAY
0.425
trex01_true-unreach-call.c [OCRS][without] 3 PASS
0.689
trex02_false-unreach-call_true-termination.c [OCRS][without] 3 OKAY
0.389
trex02_true-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.394
trex03_false-unreach-call_true-termination.c [OCRS][without] 3 OKAY
0.667
trex03_true-unreach-call.c [OCRS][without] 3 PASS
0.661
trex04_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.369
veris.c_NetBSD-libc__loop_true-unreach-call.c [OCRS][without] 1 PASS
0.348
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c [OCRS][without] 3 6.098 (4.732)
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c [OCRS][without] 1 PASS
0.361
verisec_NetBSD-libc__loop_false-unreach-call.c [OCRS][without] 1 OKAY
0.36
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c [OCRS][without] 3 OKAY
4.503 (3.006)
vogal_false-unreach-call.c [OCRS][without] 1 OKAY
0.727 (0.632)
vogal_true-unreach-call.c [OCRS][without] 1 FAIL
0.746 (0.619)
while_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.304
while_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.313
while_infinite_loop_3_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.307
while_infinite_loop_4_false-unreach-call_true-termination.c [OCRS][without] 1 OKAY
0.299
Total Below Time = 133.915 (was 128.62)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c [OCRS][without] 7 PASS
0.957 (0.756)
Ackermann02_false-unreach-call_false-termination.c [OCRS][without] 7 OKAY
0.899 (0.707)
Ackermann03_true-unreach-call.c [OCRS][without] 7 FAIL
0.93 (0.769)
Ackermann04_true-unreach-call.c [OCRS][without] 7 FAIL
0.953 (0.767)
Addition01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.549 (0.443)
Addition02_false-unreach-call_false-termination.c [OCRS][without] 2 OKAY
0.508 (0.413)
Addition03_false-no-overflow.c [OCRS][without] 2 PASS
0.548 (0.422)
Addition03_true-unreach-call.c [OCRS][without] 2 PASS
0.544 (0.415)
BallRajamani-SPIN2000-Fig1_false-unreach-call.c [OCRS][without] 2 OKAY
0.483 (0.381)
EvenOdd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.418
EvenOdd03_false-unreach-call_false-termination.c [OCRS][without] 2 OKAY
0.409
Fibonacci01_true-unreach-call.c [OCRS][without] 7 FAIL
0.655 (300.004)
Fibonacci02_true-unreach-call_true-termination.c [OCRS][without] 7 FAIL
0.665 (300.006)
Fibonacci03_true-unreach-call_true-termination.c [OCRS][without] 7 FAIL
0.677 (300.004)
Fibonacci04_false-unreach-call_true-termination.c [OCRS][without] 7 OKAY
0.673 (300.006)
Fibonacci05_false-unreach-call_true-termination.c [OCRS][without] 7 OKAY
0.657 (300.005)
gcd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.53 (0.428)
gcd02_true-unreach-call.c [OCRS][without] 2 FAIL
PASS
0.954 (0.674)
McCarthy91_false-unreach-call_false-termination.c [OCRS][without] TIMEOUT
300.008 (0.536)
McCarthy91_true-unreach-call.c [OCRS][without] TIMEOUT
300.004 (0.532)
MultCommutative_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.544 (0.425)
Primes_true-unreach-call.c [OCRS][without] 3 FAIL
1.378 (0.903)
recHanoi01_true-unreach-call_true-termination.c [OCRS][without] 8 FAIL
1.786 (300.007)
recHanoi02_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.377
recHanoi03_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.39 (0.345)
Total Below Time = 616.496 (was 1810.079)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c [OCRS][without] 2 OKAY
OKAY
0.416 (0.36)
afterrec_2calls_true-unreach-call.c [OCRS][without] 2 PASS
PASS
0.384
afterrec_false-unreach-call.c [OCRS][without] 2 OKAY
0.377
afterrec_true-unreach-call.c [OCRS][without] 2 PASS
0.369 (0.332)
fibo_10_false-unreach-call.c [OCRS][without] 7 OKAY
0.684 (300.007)
fibo_10_true-unreach-call.c [OCRS][without] 7 FAIL
0.66 (300.005)
fibo_15_false-unreach-call.c [OCRS][without] 7 OKAY
0.664 (300.006)
fibo_15_true-unreach-call.c [OCRS][without] 7 FAIL
0.702 (300.004)
fibo_20_false-unreach-call.c [OCRS][without] 7 OKAY
0.681 (300.006)
fibo_20_true-unreach-call.c [OCRS][without] 7 FAIL
0.664 (300.006)
fibo_25_false-unreach-call.c [OCRS][without] 7 OKAY
0.68 (300.005)
fibo_25_true-unreach-call.c [OCRS][without] 7 FAIL
0.682 (300.006)
fibo_2calls_10_false-unreach-call.c [OCRS][without] TIMEOUT
300.014
fibo_2calls_10_true-unreach-call.c [OCRS][without] TIMEOUT
300.014
fibo_2calls_15_false-unreach-call.c [OCRS][without] TIMEOUT
300.01
fibo_2calls_15_true-unreach-call.c [OCRS][without] TIMEOUT
300.013
fibo_2calls_20_false-unreach-call.c [OCRS][without] TIMEOUT
300.008
fibo_2calls_20_true-unreach-call.c [OCRS][without] TIMEOUT
300.01
fibo_2calls_25_false-unreach-call.c [OCRS][without] TIMEOUT
300.014
fibo_2calls_25_true-unreach-call.c [OCRS][without] TIMEOUT
300.009
fibo_2calls_2_false-unreach-call.c [OCRS][without] TIMEOUT
300.012
fibo_2calls_2_true-unreach-call.c [OCRS][without] TIMEOUT
300.009
fibo_2calls_4_false-unreach-call.c [OCRS][without] TIMEOUT
300.009
fibo_2calls_4_true-unreach-call.c [OCRS][without] TIMEOUT
300.012
fibo_2calls_5_false-unreach-call.c [OCRS][without] TIMEOUT
300.016
fibo_2calls_5_true-unreach-call.c [OCRS][without] TIMEOUT
300.01
fibo_2calls_6_false-unreach-call.c [OCRS][without] TIMEOUT
300.006
fibo_2calls_6_true-unreach-call.c [OCRS][without] TIMEOUT
300.014
fibo_2calls_8_false-unreach-call.c [OCRS][without] TIMEOUT
300.009
fibo_2calls_8_true-unreach-call.c [OCRS][without] TIMEOUT
300.01
fibo_5_false-unreach-call.c [OCRS][without] 7 OKAY
0.666 (300.004)
fibo_5_true-unreach-call.c [OCRS][without] 7 FAIL
0.659 (300.006)
fibo_7_false-unreach-call.c [OCRS][without] 7 OKAY
0.684 (300.006)
fibo_7_true-unreach-call.c [OCRS][without] 7 FAIL
0.67 (300.004)
id2_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.618 (0.517)
id2_b3_o2_false-unreach-call.c [OCRS][without] 2 OKAY
0.662 (0.536)
id2_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.617 (0.522)
id2_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.613 (0.518)
id2_i5_o5_false-unreach-call.c [OCRS][without] 2 OKAY
0.416 (0.374)
id2_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.406
id_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.542 (0.425)
id_b3_o2_false-unreach-call.c [OCRS][without] 2 OKAY
0.531 (0.432)
id_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.525 (0.421)
id_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.565 (0.409)
id_i10_o10_false-unreach-call.c [OCRS][without] 2 OKAY
0.374 (0.336)
id_i10_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.376 (0.336)
id_i15_o15_false-unreach-call.c [OCRS][without] 2 OKAY
0.374
id_i15_o15_true-unreach-call.c [OCRS][without] 2 PASS
0.372
id_i20_o20_false-unreach-call.c [OCRS][without] 2 OKAY
0.38
id_i20_o20_true-unreach-call.c [OCRS][without] 2 PASS
0.363
id_i25_o25_false-unreach-call.c [OCRS][without] 2 OKAY
0.379 (0.342)
id_i25_o25_true-unreach-call.c [OCRS][without] 2 PASS
0.361
id_i5_o5_false-unreach-call.c [OCRS][without] 2 OKAY
0.378
id_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.379
id_o1000_false-unreach-call.c [OCRS][without] 2 OKAY
0.368
id_o100_false-unreach-call.c [OCRS][without] 2 OKAY
0.386 (0.348)
id_o10_false-unreach-call.c [OCRS][without] 2 OKAY
0.375
id_o200_false-unreach-call.c [OCRS][without] 2 OKAY
0.397 (0.345)
id_o20_false-unreach-call.c [OCRS][without] 2 OKAY
0.392 (0.35)
id_o3_false-unreach-call.c [OCRS][without] 2 OKAY
0.378
sum_10x0_false-unreach-call.c [OCRS][without] 2 OKAY
0.432 (0.36)
sum_10x0_true-unreach-call.c [OCRS][without] 2 PASS
0.406 (0.343)
sum_15x0_false-unreach-call.c [OCRS][without] 2 OKAY
0.404
sum_15x0_true-unreach-call.c [OCRS][without] 2 PASS
0.4 (0.353)
sum_20x0_false-unreach-call.c [OCRS][without] 2 OKAY
0.404 (0.347)
sum_20x0_true-unreach-call.c [OCRS][without] 2 PASS
0.428 (0.353)
sum_25x0_false-unreach-call.c [OCRS][without] 2 OKAY
0.44 (0.353)
sum_25x0_true-unreach-call.c [OCRS][without] 2 PASS
0.457 (0.351)
sum_2x3_false-unreach-call.c [OCRS][without] 2 OKAY
0.427 (0.349)
sum_2x3_true-unreach-call.c [OCRS][without] 2 PASS
0.419 (0.342)
sum_non_eq_false-unreach-call.c [OCRS][without] 2 OKAY
0.431 (0.373)
sum_non_eq_true-unreach-call.c [OCRS][without] 2 PASS
0.387
sum_non_false-unreach-call.c [OCRS][without] 2 OKAY
0.439 (0.345)
sum_non_true-unreach-call.c [OCRS][without] 2 PASS
0.401 (0.357)
Total Below Time = 5427.243 (was 9016.627)
/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.441 (0.351)
rec-bhmr2007_true-unreach-call.c [OCRS][without] 2 PASS
0.412 (0.359)
rec-cggmp2005b_true-unreach-call.c [OCRS][without] 3 PASS
0.637 (0.485)
rec-cggmp2005_true-unreach-call.c [OCRS][without] 2 PASS
0.389 (0.337)
rec-cggmp2005_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.408 (0.345)
rec-css2003_true-unreach-call.c [OCRS][without] 2 PASS
0.986 (0.547)
rec-ddlm2013_true-unreach-call.c [OCRS][without] 2 FAIL
1.049 (0.41)
rec-gcnr2008_false-unreach-call.c [OCRS][without] 2 OKAY
0.767 (0.586)
rec-gj2007b_true-unreach-call.c [OCRS][without] 2 FAIL
FAIL
0.385
rec-gj2007_true-unreach-call.c [OCRS][without] 2 FAIL
0.471 (0.364)
rec-gr2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.474 (0.381)
rec-gsv2008_true-unreach-call.c [OCRS][without] 2 PASS
0.437 (0.342)
rec-hhk2008_true-unreach-call.c [OCRS][without] 2 PASS
0.383 (0.342)
rec-jm2006_true-unreach-call.c [OCRS][without] 2 PASS
0.437 (0.35)
rec-jm2006_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.497 (0.371)
rec-mcmillan2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.404
Total Below Time = 8.577 (was 6.318)
/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.357
rec-count_by_1_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.401 (0.335)
rec-count_by_2_true-unreach-call.c [OCRS][without] 2 PASS
0.36 (0.323)
rec-count_by_k_true-unreach-call.c [OCRS][without] 2 PASS
0.391 (0.347)
rec-count_by_nondet_true-unreach-call.c [OCRS][without] 2 FAIL
0.407 (0.365)
rec-gauss_sum_true-unreach-call.c [OCRS][without] 2 PASS
0.433 (0.377)
rec-half_true-unreach-call.c [OCRS][without] 2 PASS
0.388
rec-nested_true-unreach-call.c [OCRS][without] 3 FAIL
0.512 (0.433)
Total Below Time = 3.249 (was 2.877)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c [OCRS][without] 2 PASS
0.513 (0.392)
cubic_polynomial_unsafe.c [OCRS][without] 2 OKAY
0.513 (0.411)
edit_distance_bottom_up.c [OCRS][without] 3 FAIL
132.605 (35.993)
edit_distance_top_down.c [OCRS][without] 3 FAIL
2.946 (2.54)
log_log_n_solution.c [OCRS][without] 3 FAIL
0.434
log_log_n_solution_unsafe.c [OCRS][without] 3 OKAY
0.433 (0.386)
log_n_solution.c [OCRS][without] 2 FAIL
0.447 (0.379)
log_n_solution_unsafe.c [OCRS][without] 2 OKAY
0.432 (0.387)
multivariate_1.c [OCRS][without] TIMEOUT
300.096
multivariate_1_unsafe.c [OCRS][without] TIMEOUT
300.006
multivariate_higher_order.c [OCRS][without] 7 FAIL
FAIL
FAIL
32.419 (1.468)
multivariate_higher_order_unsafe.c [OCRS][without] 7 OKAY
OKAY
OKAY
8.039 (1.465)
n_cubed_solution.c [OCRS][without] EXCEPTION
46.585 (91.045)
n_cubed_solution_unsafe.c [OCRS][without] EXCEPTION
0.024
n_log_n_solution.c [OCRS][without] 10 FAIL
4.458 (1.021)
n_log_n_solution_unsafe.c [OCRS][without] 10 OKAY
4.519 (0.987)
n_squared_two_base_case_even.c [OCRS][without] 2 PASS
0.468 (0.366)
n_squared_two_base_case_even_unsafe.c [OCRS][without] 2 OKAY
0.484 (0.361)
n_squared_two_base_case_odd.c [OCRS][without] 2 PASS
0.47 (0.358)
n_squared_two_base_case_odd_unsafe.c [OCRS][without] 2 OKAY
0.475 (0.359)
pascals_dynamic.c [OCRS][without] 3 FAIL
2.632
pascals_dynamic_unsafe.c [OCRS][without] 3 OKAY
2.573
pascals_iterative.c [OCRS][without] 1 FAIL
3.619 (1.411)
pascals_iterative_unsafe.c [OCRS][without] 1 OKAY
3.631 (1.432)
pascals_recursive.c [OCRS][without] 8 FAIL
2.384 (300.005)
pascals_recursive_unsafe.c [OCRS][without] 8 OKAY
2.368 (300.007)
squared_solution.c [OCRS][without] TIMEOUT
300.007 (1.886)
squared_solution_unsafe.c [OCRS][without] TIMEOUT
300.004 (1.931)
two_n_even.c [OCRS][without] 2 PASS
0.395 (0.345)
two_n_even_unsafe.c [OCRS][without] 2 OKAY
0.409 (0.357)
two_n_odd.c [OCRS][without] 2 PASS
0.408 (0.341)
two_n_odd_unsafe.c [OCRS][without] 2 OKAY
0.414 (0.354)
two_to_n_over_two_even.c [OCRS][without] TIMEOUT
300.006
two_to_n_over_two_even_unsafe.c [OCRS][without] 8 OKAY
296.902
two_to_n_over_two_odd.c [OCRS][without] TIMEOUT
300.005
two_to_n_over_two_odd_unsafe.c [OCRS][without] TIMEOUT
300.005
two_to_n_squared.c [OCRS][without] 8 EXCEPTION
17.03 (8.234)
two_to_n_squared_unsafe.c [OCRS][without] 8 EXCEPTION
17.011 (8.205)
two_to_two_to_n.c [OCRS][without] 7 FAIL
0.879 (0.601)
two_to_two_to_n_unsafe.c [OCRS][without] 7 OKAY
0.862 (0.592)
Total Below Time = 2687.91 (was 2568.982)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c [OCRS][without] 1 PASS
0.369 (0.32)
adding_and_mult_unsafe.c [OCRS][without] 1 OKAY
0.359 (0.314)
binary_search_array_tree.c [OCRS][without] 1 FAIL
FAIL
0.691 (0.522)
exp_add_linear.c [OCRS][without] 1 PASS
0.438 (0.349)
exp_add_linear_unsafe.c [OCRS][without] 1 OKAY
0.442 (0.346)
exp_add_loop_rec.c [OCRS][without] 1 FAIL
0.353
exp_add_loop_rec_unsafe.c [OCRS][without] 1 OKAY
0.369
exp_add_loop_variable.c [OCRS][without] 1 PASS
0.404 (0.347)
exp_add_loop_variable_unsafe.c [OCRS][without] 1 OKAY
0.415 (0.368)
exp_with_linear_inner_loop.c [OCRS][without] 1 FAIL
0.486 (0.389)
exp_with_linear_inner_loop_unsafe.c [OCRS][without] 1 OKAY
0.465 (0.366)
halving_log1.c [OCRS][without] 1 FAIL
0.485 (0.378)
linear_two_to_n.c [OCRS][without] 8 FAIL
1.043 (300.006)
linear_two_to_n_unsafe.c [OCRS][without] 8 OKAY
1.041 (300.007)
loop_five_to_n.c [OCRS][without] 1 PASS
0.379
loop_five_to_n_unsafe.c [OCRS][without] 1 OKAY
0.386
non_loop_five_to_n.c [OCRS][without] TIMEOUT
300.039
non_loop_five_to_n_unsafe.c [OCRS][without] TIMEOUT
300.036
power_log.c [OCRS][without] 1 PASS
0.451 (0.362)
power_log_modified.c [OCRS][without] 1 PASS
0.505 (0.385)
simple_exponential.c [OCRS][without] 1 PASS
0.386 (0.338)
simple_exponential_for.c [OCRS][without] 1 PASS
0.39 (0.332)
simple_exponential_for_unsafe.c [OCRS][without] 1 OKAY
0.394 (0.342)
simple_exponential_unsafe.c [OCRS][without] 1 OKAY
0.381
two_to_n_minus_n.c [OCRS][without] 7 FAIL
1.196 (300.004)
two_to_n_minus_n_loop.c [OCRS][without] 7 FAIL
1.713 (300.007)
two_to_n_minus_n_loop_unsafe.c [OCRS][without] 7 OKAY
1.62 (300.006)
two_to_n_minus_n_unsafe.c [OCRS][without] 7 OKAY
1.19 (300.005)
Total Below Time = 616.426 (was 2407.25)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c [OCRS][without] 3 PASS
0.551 (0.373)
02.c [OCRS][without] 3 FAIL
0.704 (0.503)
03.c [OCRS][without] 1 PASS
0.422 (0.372)
04.c [OCRS][without] 1 PASS
0.343
05.c [OCRS][without] 3 PASS
0.966 (0.476)
06.c [OCRS][without] 3 PASS
13.728 (2.98)
07.c [OCRS][without] 3 PASS
0.506 (0.388)
08.c [OCRS][without] 3 PASS
1.064 (0.76)
09.c [OCRS][without] 3 PASS
0.634 (0.476)
10.c [OCRS][without] 3 FAIL
0.822 (0.532)
11.c [OCRS][without] 1 PASS
0.348 (0.312)
12.c [OCRS][without] 3 PASS
1.151 (0.555)
13.c [OCRS][without] 3 PASS
0.499 (0.402)
14.c [OCRS][without] 3 PASS
PASS
0.444 (0.366)
15.c [OCRS][without] 1 PASS
0.34
16.c [OCRS][without] 1 PASS
0.412 (0.346)
17.c [OCRS][without] EXCEPTION
0.363
18.c [OCRS][without] 1 PASS
0.419 (0.337)
19.c [OCRS][without] 1 PASS
0.443 (0.365)
20.c [OCRS][without] 3 PASS
PASS
FAIL
0.566 (0.443)
21.c [OCRS][without] 3 PASS
0.489 (0.423)
22.c [OCRS][without] 3 FAIL
PASS
0.978 (0.445)
23.c [OCRS][without] 1 PASS
0.371 (0.32)
24.c [OCRS][without] 1 PASS
0.377
25.c [OCRS][without] 3 FAIL
1.135 (0.785)
26.c [OCRS][without] TIMEOUT
300.004
27.c [OCRS][without] 1 PASS
0.412 (0.355)
28.c [OCRS][without] 3 PASS
0.474 (0.377)
29.c [OCRS][without] EXCEPTION
0.411 (0.37)
30.c [OCRS][without] 1 PASS
0.36 (0.305)
31.c [OCRS][without] 3 PASS
PASS
0.778 (0.562)
32.c [OCRS][without] 1 FAIL
0.374
33.c [OCRS][without] 3 PASS
1.058 (0.761)
34.c [OCRS][without] 1 FAIL
0.384 (0.346)
35.c [OCRS][without] 1 PASS
0.324
36.c [OCRS][without] 3 PASS
2.257 (1.493)
37.c [OCRS][without] 3 FAIL
0.465 (0.354)
38.c [OCRS][without] 1 FAIL
0.376 (0.337)
39.c [OCRS][without] 3 PASS
PASS
0.417
40.c [OCRS][without] 3 PASS
0.67 (0.49)
41.c [OCRS][without] 1 PASS
0.37 (0.317)
42.c [OCRS][without] 3 PASS
0.753 (0.509)
43.c [OCRS][without] 3 PASS
0.445
44.c [OCRS][without] 1 PASS
0.366 (0.325)
45.c [OCRS][without] 3 FAIL
2.305 (1.377)
46.c [OCRS][without] 3 FAIL
1.989 (0.785)
Total Below Time = 343.067 (was 323.886)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c [OCRS][without] 1 PASS
0.391 (0.341)
AGHKTW2017_foo.c [OCRS][without] 1 PASS
0.402 (0.34)
AGHKTW2017_loginSafe.c [OCRS][without] 1 PASS
0.77 (0.505)
AGHKTW2017_loopAndBranch_safe.c [OCRS][without] 1 FAIL
0.43 (0.362)
BCK2011_gauss.c [OCRS][without] 1 PASS
0.421 (0.363)
BCK2011_strength_reduction.c [OCRS][without] 1 PASS
0.392 (0.346)
BCK2011_strength_reduction_linear.c [OCRS][without] 1 PASS
0.415 (0.371)
fibonacci_information_flow.c [OCRS][without] 1 PASS
0.561 (0.362)
TA2005_fib2.c [OCRS][without] 1 PASS
0.532 (0.437)
TA2005_fib.c [OCRS][without] 1 PASS
0.424 (0.349)
Total Below Time = 4.738 (was 3.776)

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