[Version Information]
Phase2 (IST-Java-ICRA) WALi-OpenNWA version: 9042782a9a5ed8987eef2dfeec4e384ee950f24c (2017-05-01 17:41:53 -0500) "Adding benchmarks for model of malware analyzer."
Phase2 (IST-Java-ICRA) duet version: 9c9e95ed58abc89f69fc775b6f484eb2863d8b6e (2017-05-09 22:35:28 -0400) "Added extra bytecode costs for thread.sleep"

Phase3 WALi-OpenNWA version: 9042782a9a5ed8987eef2dfeec4e384ee950f24c (2017-05-01 17:41:53 -0500) "Adding benchmarks for model of malware analyzer."
Phase3 duet version: 05dc712315a9f1a66cd0a3c927666793fd03610e (2017-04-27 22:38:51 -0400) "Merge remote-tracking branch 'origin/ark2' into Newton-ark2"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-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.365
kmp.c [OCRS][without] 1 PASS
1.313 (1.184)
qsort.c [OCRS][without] 4 PASS
2.579 (2.066)
speed_pldi09_fig1.c [OCRS][without] 1 PASS
0.371
speed_pldi09_fig4_2.c [OCRS][without] 1 FAIL
0.404
speed_pldi09_fig4_4.c [OCRS][without] 1 PASS
0.447
speed_pldi09_fig4_5.c [OCRS][without] 1 PASS
0.37
speed_pldi10_ex1.c [OCRS][without] 1 PASS
3.767 (0.814)
speed_pldi10_ex3.c [OCRS][without] 1 PASS
0.451
speed_pldi10_ex4.c [OCRS][without] EXCEPTION
0.415
speed_popl10_fig2_1.c [OCRS][without] 1 PASS
0.371
speed_popl10_fig2_2.c [OCRS][without] 1 FAIL
0.354
speed_popl10_nested_multiple.c [OCRS][without] 1 PASS
0.428
speed_popl10_nested_single.c [OCRS][without] 1 PASS
0.398
speed_popl10_sequential_single.c [OCRS][without] 1 PASS
0.344
speed_popl10_simple_multiple.c [OCRS][without] 1 PASS
0.384
speed_popl10_simple_single_2.c [OCRS][without] 1 PASS
0.407
speed_popl10_simple_single.c [OCRS][without] 1 PASS
0.339
t07.c [OCRS][without] 1 PASS
0.364
t08.c [OCRS][without] 1 PASS
0.342
t09.c [OCRS][without] 1 PASS
0.336
t10.c [OCRS][without] 1 PASS
0.354
t11.c [OCRS][without] 1 PASS
0.39
t13.c [OCRS][without] 1 FAIL
0.395
t15.c [OCRS][without] 1 PASS
0.369
t16.c [OCRS][without] 1 PASS
0.369
t19.c [OCRS][without] 1 PASS
0.342
t20.c [OCRS][without] 1 PASS
0.336
t27.c [OCRS][without] 1 PASS
0.425
t28.c [OCRS][without] 1 PASS
0.39
t30.c [OCRS][without] 1 FAIL
0.353
t37.c [OCRS][without] 2 PASS
0.465
t39.c [OCRS][without] 2 PASS
0.478
t46.c [OCRS][without] 1 PASS
0.347
t47.c [OCRS][without] 1 PASS
0.356
Total Below Time = 19.918 (was 16.408)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c [OCRS][without] 2 PASS
PASS
0.386
qsort_full.c [OCRS][without] 4 TIMEOUT
300.005 (42.771)
rec1-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.352
rec1-param_unsafe.c [OCRS][without] 2 PASS
0.355
rec1_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.338
rec1_unsafe.c [OCRS][without] 2 PASS
0.333
rec2-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.338
rec2-param_unsafe.c [OCRS][without] 2 PASS
0.35
rec2_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.338
rec2_unsafe.c [OCRS][without] 2 PASS
0.339
rec-test.c [OCRS][without] 2 PASS
0.337
sas03_bothbranches.c [OCRS][without] 7 PASS
1.276
sas03.c [OCRS][without] 2 PASS
0.782
simulated_lese_recursive.c [OCRS][without] 2 PASS
0.371
Total Below Time = 305.9 (was 48.725)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c [OCRS][without] 1 PASS
0.317
count_up_down_unsafe.c [OCRS][without] 1 PASS
0.34
divide.c [OCRS][without] 1 PASS
0.342
factor_unsafe.c [OCRS][without] TIMEOUT
300.004
for_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.326
for_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.323
interproc.c [OCRS][without] 1 PASS
0.302
mult.c [OCRS][without] 1 PASS
PASS
0.317
pointer_arith.c [OCRS][without] 1 PASS
PASS
PASS
PASS
0.297
quotient.c [OCRS][without] 3 PASS
0.41
subtract.c [OCRS][without] 1 PASS
0.33
sum01_bug02_sum01_bug02_base.case_unsafe.c [OCRS][without] 1 PASS
0.36
sum01_bug02_unsafe.c [OCRS][without] 1 PASS
0.391
sum01_real_safe.c [OCRS][without] 1 PASS
0.326
sum01_safe.c [OCRS][without] 1 PASS
0.332
sum01_unsafe.c [OCRS][without] 1 PASS
0.37
sum02_safe.c [OCRS][without] 1 PASS
0.335
sum03_safe.c [OCRS][without] 1 PASS
0.322
sum03_unsafe.c [OCRS][without] 1 PASS
0.4
sum04_safe.c [OCRS][without] 1 PASS
0.322
sum04_unsafe.c [OCRS][without] 1 PASS
0.356
terminator_02_safe.c [OCRS][without] 1 PASS
0.329
terminator_02_unsafe.c [OCRS][without] 1 PASS
0.348
terminator_03_safe.c [OCRS][without] 1 PASS
0.311
terminator_03_unsafe.c [OCRS][without] 1 PASS
0.324
token_ring01_safe.c [OCRS][without] TIMEOUT
300.007
token_ring01_unsafe.c [OCRS][without] TIMEOUT
300.006
toy_safe.c [OCRS][without] EXCEPTION
178.652
trex01_safe.c [OCRS][without] 1 PASS
0.681 (0.764)
trex01_unsafe.c [OCRS][without] 1 PASS
0.375
trex02_safe2.c [OCRS][without] 3 PASS
0.385
trex02_safe.c [OCRS][without] 3 PASS
0.381
trex02_unsafe.c [OCRS][without] 3 PASS
0.383
trex03_safe.c [OCRS][without] 1 PASS
0.452
trex03_unsafe.c [OCRS][without] 1 PASS
0.453
trex04_safe.c [OCRS][without] 1 PASS
0.355
while_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.305
while_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.313
while_infinite_loop_3_safe.c [OCRS][without] 1 PASS
0.307
Total Below Time = 1091.189 (was 1076.228)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c [OCRS][without] 3 PASS
0.453
blogger_simplified1.c [OCRS][without] 3 PASS
1.036 (0.941)
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.397
popall.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
0.407
simulated_scc.c [OCRS][without] 1 PASS
PASS
0.505
Total Below Time = 303.162 (was 303.084)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c [OCRS][without] 1 PASS
0.322
degree2_binomial.c [OCRS][without] 1 PASS
0.469
degree2_monomial.c [OCRS][without] 1 PASS
0.363
degree3_binomial.c [OCRS][without] 1 PASS
0.892
degree3_monomial.c [OCRS][without] 1 PASS
0.408
degree4_binomial.c [OCRS][without] 1 PASS
1.148
degree4_monomial.c [OCRS][without] 1 PASS
0.488
degree5_binomial.c [OCRS][without] 1 PASS
1.713 (1.93)
degree5_monomial.c [OCRS][without] 1 PASS
0.56
Total Below Time = 6.363 (was 6.583)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c [OCRS][without] 1 PASS
0.344
cubic_with_square_interproc.c [OCRS][without] 2 PASS
0.373
cubic_with_square_nonlinear.c [OCRS][without] 1 PASS
0.336
cubic_with_square_nonlinear_interproc.c [OCRS][without] 2 PASS
0.368
cubic_with_square_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.348
cubic_with_square_unsafe.c [OCRS][without] 1 PASS
0.363
multi-input.c [OCRS][without] 1 PASS
0.395
multi-input_unsafe.c [OCRS][without] 1 PASS
0.428 (0.496)
nondet_loop_bound.c [OCRS][without] 1 PASS
0.352
nondet_loop_bound_quartic.c [OCRS][without] 1 PASS
0.362
nondet_loop_bound_quartic_unsafe.c [OCRS][without] 1 PASS
0.348
nondet_loop_bound_unsafe.c [OCRS][without] 1 PASS
0.389
nonlinear_stratified.c [OCRS][without] 1 FAIL
0.393 (0.352)
nonlinear_stratified_unsafe.c [OCRS][without] 1 PASS
0.362
quartic_with_cube.c [OCRS][without] 1 PASS
0.356
quartic_with_cube_nonlinear.c [OCRS][without] 1 PASS
0.37
quartic_with_cube_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.373
quartic_with_cube_unsafe.c [OCRS][without] 1 PASS
0.351
quintic_with_quartic.c [OCRS][without] 1 PASS
0.346
quintic_with_quartic_nonlinear.c [OCRS][without] 1 PASS
0.38
quintic_with_quartic_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.391 (0.46)
quintic_with_quartic_unsafe.c [OCRS][without] 1 PASS
0.351
Total Below Time = 8.079 (was 8.229)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c [OCRS][without] 1 PASS
0.496
degree2_FD_AllAux_AllAssm.c [OCRS][without] 1 PASS
3.602 (3.13)
degree2_FD_AllAux_FewAssm.c [OCRS][without] 1 PASS
5.447 (3.107)
degree2_FD_FewAux_FewAssm.c [OCRS][without] 1 PASS
0.686
degree2_FD_FewAux_FewAssm_NonLinAsrt.c [OCRS][without] 1 PASS
0.711
degree3.c [OCRS][without] 1 PASS
0.56
degree3_FD.c [OCRS][without] 1 PASS
0.729
degree4.c [OCRS][without] 1 PASS
0.388
Total Below Time = 12.619 (was 9.812)
/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.405
simulated_lese_parser.c [OCRS][without] 1 PASS
0.318
simulated_lese_sentinel.c [OCRS][without] 1 PASS
0.337
Total Below Time = 1.449 (was 1.474)
/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.34)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c [OCRS][without] TIMEOUT
300.013
Total Below Time = 300.013 (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.337
array_false-unreach-call2.c [OCRS][without] 1 PASS
0.365
array_false-unreach-call3.c [OCRS][without] 1 PASS
0.33
array_true-unreach-call1.c [OCRS][without] 1 FAIL
0.34
array_true-unreach-call2.c [OCRS][without] 1 FAIL
0.373
array_true-unreach-call3.c [OCRS][without] 1 PASS
0.324
array_true-unreach-call4.c [OCRS][without] 1 FAIL
0.332
const_false-unreach-call1.c [OCRS][without] 1 PASS
0.315
const_true-unreach-call1.c [OCRS][without] 1 PASS
0.315
diamond_false-unreach-call1.c [OCRS][without] 1 PASS
0.34 (0.379)
diamond_true-unreach-call1.c [OCRS][without] 1 PASS
0.334
diamond_true-unreach-call2.c [OCRS][without] 1 PASS
0.371
functions_false-unreach-call1.c [OCRS][without] 3 PASS
0.347
functions_true-unreach-call1.c [OCRS][without] 3 PASS
0.35
multivar_false-unreach-call1.c [OCRS][without] 1 PASS
0.333
multivar_true-unreach-call1.c [OCRS][without] 1 PASS
0.338
nested_false-unreach-call1.c [OCRS][without] 1 PASS
0.335
nested_true-unreach-call1.c [OCRS][without] 1 PASS
0.331
overflow_true-unreach-call1.c [OCRS][without] 1 PASS
0.317
phases_false-unreach-call1.c [OCRS][without] 1 PASS
0.338
phases_false-unreach-call2.c [OCRS][without] 1 PASS
0.348
phases_true-unreach-call1.c [OCRS][without] 1 PASS
0.341
phases_true-unreach-call2.c [OCRS][without] 1 PASS
0.346
simple_false-unreach-call1.c [OCRS][without] 1 PASS
0.33
simple_false-unreach-call2.c [OCRS][without] 1 PASS
0.342 (0.31)
simple_false-unreach-call3.c [OCRS][without] 1 PASS
0.309
simple_false-unreach-call4.c [OCRS][without] 1 PASS
0.314
simple_true-unreach-call1.c [OCRS][without] 1 PASS
0.314
simple_true-unreach-call2.c [OCRS][without] 1 PASS
0.314
simple_true-unreach-call3.c [OCRS][without] 1 PASS
0.327
simple_true-unreach-call4.c [OCRS][without] 1 PASS
0.308
underapprox_false-unreach-call1.c [OCRS][without] 1 PASS
0.315
underapprox_false-unreach-call2.c [OCRS][without] 1 PASS
0.323
underapprox_true-unreach-call1.c [OCRS][without] 1 FAIL
0.323
underapprox_true-unreach-call2.c [OCRS][without] 1 PASS
0.324
Total Below Time = 11.643 (was 11.743)
/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.844
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.439
down_true-unreach-call.c [OCRS][without] 1 PASS
0.323
fragtest_simple_true-unreach-call.c [OCRS][without] 1 PASS
0.379
half_2_true-unreach-call.c [OCRS][without] 1 PASS
0.328
heapsort_true-unreach-call.c [OCRS][without] 1 TIMEOUT
300.14 (2.384)
id_build_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.321
id_trans_false-unreach-call.c [OCRS][without] 1 FAIL
FAIL
FAIL
PASS
0.332
large_const_true-unreach-call.c [OCRS][without] 1 PASS
0.387
MADWiFi-encode_ie_ok_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.365
nested6_true-unreach-call.c [OCRS][without] 1 FAIL
FAIL
PASS
0.413
nested9_true-unreach-call.c [OCRS][without] 1 PASS
0.448
nest-if3_true-unreach-call.c [OCRS][without] 1 PASS
0.428
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.384
seq_true-unreach-call.c [OCRS][without] 1 PASS
0.368
SpamAssassin-loop_true-unreach-call.c [OCRS][without] TIMEOUT
300.107 (1.219)
string_concat-noarr_true-unreach-call.c [OCRS][without] 1 PASS
0.338
up_true-unreach-call.c [OCRS][without] 1 PASS
0.333
Total Below Time = 607.017 (was 10.515)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c [OCRS][without] 1 PASS
0.331
bhmr2007_true-unreach-call.c [OCRS][without] 1 PASS
0.357
cggmp2005b_true-unreach-call.c [OCRS][without] 1 PASS
0.392
cggmp2005_true-unreach-call.c [OCRS][without] 1 PASS
0.315
cggmp2005_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.327
css2003_true-unreach-call.c [OCRS][without] 1 PASS
0.461
ddlm2013_true-unreach-call.c [OCRS][without] 1 PASS
0.398
gcnr2008_false-unreach-call.c [OCRS][without] 1 TIMEOUT
300.153 (0.866)
gj2007b_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
0.363
gj2007_true-unreach-call.c [OCRS][without] 1 PASS
0.341
gr2006_true-unreach-call.c [OCRS][without] 1 PASS
0.325
gsv2008_true-unreach-call.c [OCRS][without] 1 PASS
0.319
hhk2008_true-unreach-call.c [OCRS][without] 1 PASS
0.322
jm2006_true-unreach-call.c [OCRS][without] 1 PASS
0.352
jm2006_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.361
mcmillan2006_true-unreach-call.c [OCRS][without] 1 FAIL
0.383
Total Below Time = 305.5 (was 6.32)
/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.313
count_by_1_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.334
count_by_2_true-unreach-call.c [OCRS][without] 1 PASS
0.319
count_by_k_true-unreach-call.c [OCRS][without] 1 PASS
0.34
count_by_nondet_true-unreach-call.c [OCRS][without] 1 FAIL
0.342
gauss_sum_true-unreach-call.c [OCRS][without] 1 PASS
0.352
half_true-unreach-call.c [OCRS][without] EXCEPTION
0.331
nested_true-unreach-call.c [OCRS][without] 1 PASS
0.383
Total Below Time = 2.714 (was 2.717)
/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.429
bubble_sort_false-unreach-call.c [OCRS][without] EXCEPTION
106.535 (140.638)
bubble_sort_true-unreach-call.c [OCRS][without] TIMEOUT
300.005
compact_false-unreach-call.c [OCRS][without] 1 PASS
0.373
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.318
eureka_01_false-unreach-call.c [OCRS][without] 1 PASS
2.196
eureka_01_true-unreach-call.c [OCRS][without] 1 FAIL
1.946
eureka_05_true-unreach-call.c [OCRS][without] 1 FAIL
1.059 (0.755)
for_bounded_loop1_false-unreach-call_true-termination.c [OCRS][without] 1 FAIL
FAIL
PASS
0.341
for_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.321
for_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.319
heavy_false-unreach-call.c [OCRS][without] 1 PASS
0.522
heavy_true-unreach-call.c [OCRS][without] 1 PASS
0.491
insertion_sort_false-unreach-call.c [OCRS][without] 1 PASS
2.144
insertion_sort_true-unreach-call.c [OCRS][without] 1 FAIL
0.734
invert_string_false-unreach-call.c [OCRS][without] 1 PASS
0.492
invert_string_true-unreach-call.c [OCRS][without] 1 FAIL
0.492
linear_sea.ch_true-unreach-call.c [OCRS][without] 1 FAIL
0.362
linear_search_false-unreach-call.c [OCRS][without] 1 EXCEPTION
0.414
lu.cmp_true-unreach-call.c [OCRS][without] TIMEOUT
300.239 (125.231)
ludcmp_false-unreach-call.c [OCRS][without] TIMEOUT
300.245 (122.67)
matrix_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
1.004 (0.829)
matrix_true-unreach-call_true-termination.c [OCRS][without] 1 FAIL
0.532
n.c11_true-unreach-call.c [OCRS][without] 3 FAIL
0.472
n.c24_false-unreach-call.c [OCRS][without] 3 PASS
22.798
n.c40_true-unreach-call.c [OCRS][without] 1 FAIL
0.363
nec11_false-unreach-call.c [OCRS][without] 1 PASS
0.377
nec20_false-unreach-call.c [OCRS][without] 1 PASS
0.363
nec40_true-unreach-call.c [OCRS][without] 1 FAIL
0.372
string_false-unreach-call.c [OCRS][without] 1 PASS
0.652
string_true-unreach-call.c [OCRS][without] 1 FAIL
0.648
sum01_bug02_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.391
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.357
sum01_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.375
sum01_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.339
sum03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.465
sum03_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.359
sum04_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.377
sum04_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.328
sum_array_false-unreach-call.c [OCRS][without] 1 PASS
0.621
sum_array_true-unreach-call.c [OCRS][without] 1 FAIL
0.695
terminator_01_false-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.32
terminator_02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.423
terminator_02_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.346
terminator_03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.327
terminator_03_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.326
trex01_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.471
trex01_true-unreach-call.c [OCRS][without] 3 PASS
0.773 (0.672)
trex02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.38
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.892
trex03_true-unreach-call.c [OCRS][without] 3 PASS
0.868
trex04_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.373
veris.c_NetBSD-libc__loop_true-unreach-call.c [OCRS][without] 1 PASS
0.327
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c [OCRS][without] 3 24.048
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c [OCRS][without] 1 PASS
0.355
verisec_NetBSD-libc__loop_false-unreach-call.c [OCRS][without] 1 PASS
0.346
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c [OCRS][without] 3 PASS
17.203
vogal_false-unreach-call.c [OCRS][without] 1 PASS
0.9 (0.757)
vogal_true-unreach-call.c [OCRS][without] 1 FAIL
0.896 (0.764)
while_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.295
while_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.323
while_infinite_loop_3_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.322
while_infinite_loop_4_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.313
Total Below Time = 1103.845 (was 784.504)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c [OCRS][without] TIMEOUT
300.021 (2.512)
Ackermann02_false-unreach-call_false-termination.c [OCRS][without] TIMEOUT
300.02 (2.32)
Ackermann03_true-unreach-call.c [OCRS][without] TIMEOUT
300.02 (2.475)
Ackermann04_true-unreach-call.c [OCRS][without] TIMEOUT
300.02 (2.397)
Addition01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.586
Addition02_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.58
Addition03_false-no-overflow.c [OCRS][without] 2 PASS
0.591
Addition03_true-unreach-call.c [OCRS][without] 2 PASS
0.58
BallRajamani-SPIN2000-Fig1_false-unreach-call.c [OCRS][without] 2 PASS
0.448
EvenOdd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.408
EvenOdd03_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.432
Fibonacci01_true-unreach-call.c [OCRS][without] EXCEPTION
0.95 (300.008)
Fibonacci02_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.933 (300.011)
Fibonacci03_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.963 (300.01)
Fibonacci04_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.983 (300.008)
Fibonacci05_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.958 (300.011)
gcd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.544
gcd02_true-unreach-call.c [OCRS][without] 2 FAIL
PASS
1.369 (1.163)
McCarthy91_false-unreach-call_false-termination.c [OCRS][without] 7 PASS
1.442 (1.143)
McCarthy91_true-unreach-call.c [OCRS][without] 7 FAIL
1.476 (1.113)
MultCommutative_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.699 (0.602)
Primes_true-unreach-call.c [OCRS][without] 3 FAIL
2.158 (1.93)
recHanoi01_true-unreach-call_true-termination.c [OCRS][without] 9 FAIL
5.908
recHanoi02_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.366
recHanoi03_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.394
Total Below Time = 1222.849 (was 1526.457)
/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.432
afterrec_2calls_true-unreach-call.c [OCRS][without] 2 PASS
PASS
0.393
afterrec_false-unreach-call.c [OCRS][without] 2 PASS
0.376
afterrec_true-unreach-call.c [OCRS][without] 2 PASS
0.34
fibo_10_false-unreach-call.c [OCRS][without] EXCEPTION
0.989 (300.005)
fibo_10_true-unreach-call.c [OCRS][without] EXCEPTION
0.962 (300.008)
fibo_15_false-unreach-call.c [OCRS][without] EXCEPTION
0.961 (300.009)
fibo_15_true-unreach-call.c [OCRS][without] EXCEPTION
0.946 (300.008)
fibo_20_false-unreach-call.c [OCRS][without] EXCEPTION
0.949 (300.007)
fibo_20_true-unreach-call.c [OCRS][without] EXCEPTION
0.936 (300.011)
fibo_25_false-unreach-call.c [OCRS][without] EXCEPTION
0.924 (300.009)
fibo_25_true-unreach-call.c [OCRS][without] EXCEPTION
0.942 (300.01)
fibo_2calls_10_false-unreach-call.c [OCRS][without] EXCEPTION
17.212 (131.553)
fibo_2calls_10_true-unreach-call.c [OCRS][without] EXCEPTION
17.482 (131.157)
fibo_2calls_15_false-unreach-call.c [OCRS][without] EXCEPTION
17.11 (129.082)
fibo_2calls_15_true-unreach-call.c [OCRS][without] EXCEPTION
17.396 (132.058)
fibo_2calls_20_false-unreach-call.c [OCRS][without] EXCEPTION
17.203 (130.977)
fibo_2calls_20_true-unreach-call.c [OCRS][without] EXCEPTION
17.577 (131.089)
fibo_2calls_25_false-unreach-call.c [OCRS][without] EXCEPTION
17.236 (127.481)
fibo_2calls_25_true-unreach-call.c [OCRS][without] EXCEPTION
17.583 (130.918)
fibo_2calls_2_false-unreach-call.c [OCRS][without] EXCEPTION
17.406 (130.291)
fibo_2calls_2_true-unreach-call.c [OCRS][without] EXCEPTION
17.356 (128.768)
fibo_2calls_4_false-unreach-call.c [OCRS][without] EXCEPTION
17.478 (131.133)
fibo_2calls_4_true-unreach-call.c [OCRS][without] EXCEPTION
17.524 (130.75)
fibo_2calls_5_false-unreach-call.c [OCRS][without] EXCEPTION
17.559 (128.396)
fibo_2calls_5_true-unreach-call.c [OCRS][without] EXCEPTION
17.505 (129.022)
fibo_2calls_6_false-unreach-call.c [OCRS][without] EXCEPTION
17.472 (130.799)
fibo_2calls_6_true-unreach-call.c [OCRS][without] EXCEPTION
17.209 (129.507)
fibo_2calls_8_false-unreach-call.c [OCRS][without] EXCEPTION
17.282 (130.579)
fibo_2calls_8_true-unreach-call.c [OCRS][without] EXCEPTION
17.268 (132.384)
fibo_5_false-unreach-call.c [OCRS][without] EXCEPTION
0.954 (300.009)
fibo_5_true-unreach-call.c [OCRS][without] EXCEPTION
0.938 (300.009)
fibo_7_false-unreach-call.c [OCRS][without] EXCEPTION
0.979 (300.009)
fibo_7_true-unreach-call.c [OCRS][without] EXCEPTION
0.94 (300.009)
id2_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.981
id2_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.989
id2_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.956
id2_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.97
id2_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.432
id2_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.423
id_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.583
id_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.603
id_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.565
id_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.557
id_i10_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.367
id_i10_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.371
id_i15_o15_false-unreach-call.c [OCRS][without] 2 PASS
0.364
id_i15_o15_true-unreach-call.c [OCRS][without] 2 PASS
0.373
id_i20_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.373
id_i20_o20_true-unreach-call.c [OCRS][without] 2 PASS
0.358
id_i25_o25_false-unreach-call.c [OCRS][without] 2 PASS
0.379
id_i25_o25_true-unreach-call.c [OCRS][without] 2 PASS
0.363
id_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.371
id_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.376
id_o1000_false-unreach-call.c [OCRS][without] 2 PASS
0.381
id_o100_false-unreach-call.c [OCRS][without] 2 PASS
0.37
id_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.372
id_o200_false-unreach-call.c [OCRS][without] 2 PASS
0.379
id_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.365
id_o3_false-unreach-call.c [OCRS][without] 2 PASS
0.383
sum_10x0_false-unreach-call.c [OCRS][without] 2 PASS
0.393
sum_10x0_true-unreach-call.c [OCRS][without] 2 PASS
0.385
sum_15x0_false-unreach-call.c [OCRS][without] 2 PASS
0.38
sum_15x0_true-unreach-call.c [OCRS][without] 2 PASS
0.367
sum_20x0_false-unreach-call.c [OCRS][without] 2 PASS
0.396
sum_20x0_true-unreach-call.c [OCRS][without] 2 PASS
0.374
sum_25x0_false-unreach-call.c [OCRS][without] 2 PASS
0.401
sum_25x0_true-unreach-call.c [OCRS][without] 2 PASS
0.385
sum_2x3_false-unreach-call.c [OCRS][without] 2 PASS
0.404
sum_2x3_true-unreach-call.c [OCRS][without] 2 PASS
0.388
sum_non_eq_false-unreach-call.c [OCRS][without] 2 PASS
0.433
sum_non_eq_true-unreach-call.c [OCRS][without] 2 PASS
0.422
sum_non_false-unreach-call.c [OCRS][without] 2 PASS
0.396
sum_non_true-unreach-call.c [OCRS][without] 2 PASS
0.385
Total Below Time = 344.332 (was 5966.008)
/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.379
rec-bhmr2007_true-unreach-call.c [OCRS][without] 2 PASS
0.403
rec-cggmp2005b_true-unreach-call.c [OCRS][without] 3 PASS
0.759
rec-cggmp2005_true-unreach-call.c [OCRS][without] 2 PASS
0.348
rec-cggmp2005_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.346
rec-css2003_true-unreach-call.c [OCRS][without] 2 PASS
0.626
rec-ddlm2013_true-unreach-call.c [OCRS][without] EXCEPTION
0.351 (0.446)
rec-gcnr2008_false-unreach-call.c [OCRS][without] 2 PASS
0.856
rec-gj2007b_true-unreach-call.c [OCRS][without] 2 FAIL
FAIL
0.396
rec-gj2007_true-unreach-call.c [OCRS][without] 2 FAIL
0.383
rec-gr2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.393
rec-gsv2008_true-unreach-call.c [OCRS][without] 2 PASS
0.351
rec-hhk2008_true-unreach-call.c [OCRS][without] 2 PASS
0.351
rec-jm2006_true-unreach-call.c [OCRS][without] 2 PASS
0.37
rec-jm2006_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.386
rec-mcmillan2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.42
Total Below Time = 7.118 (was 7.175)
/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.335
rec-count_by_1_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.352
rec-count_by_2_true-unreach-call.c [OCRS][without] 2 PASS
0.338
rec-count_by_k_true-unreach-call.c [OCRS][without] 2 PASS
0.354
rec-count_by_nondet_true-unreach-call.c [OCRS][without] 2 FAIL
0.372
rec-gauss_sum_true-unreach-call.c [OCRS][without] 2 PASS
0.37
rec-half_true-unreach-call.c [OCRS][without] EXCEPTION
0.341 (0.395)
rec-nested_true-unreach-call.c [OCRS][without] 3 PASS
0.631
Total Below Time = 3.093 (was 3.172)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c [OCRS][without] 2 PASS
0.51
edit_distance_bottom_up.c [OCRS][without] 3 TIMEOUT
300.009
edit_distance_top_down.c [OCRS][without] 3 FAIL
50.732
log_log_n_solution.c [OCRS][without] 3 FAIL
0.429 (0.797)
log_n_solution.c [OCRS][without] 2 FAIL
0.442
multivariate_1.c [OCRS][without] TIMEOUT
300.006
multivariate_higher_order.c [OCRS][without] 7 FAIL
FAIL
FAIL
26.221
n_cubed_solution.c [OCRS][without] EXCEPTION
0.338
n_log_n_solution.c [OCRS][without] TIMEOUT
300.034 (1.816)
n_squared_two_base_case_even.c [OCRS][without] 2 PASS
0.382
n_squared_two_base_case_odd.c [OCRS][without] 2 PASS
0.396
pascals_dynamic.c [OCRS][without] 3 FAIL
19.803
pascals_iterative.c [OCRS][without] 1 FAIL
5.38 (6.115)
pascals_recursive.c [OCRS][without] TIMEOUT
300.005
squared_solution.c [OCRS][without] TIMEOUT
300.137 (10.407)
two_n_even.c [OCRS][without] 2 PASS
0.369
two_n_odd.c [OCRS][without] 2 PASS
0.376
two_to_n_over_two_even.c [OCRS][without] TIMEOUT
300.034 (44.977)
two_to_n_over_two_odd.c [OCRS][without] TIMEOUT
300.029 (44.79)
two_to_n_squared.c [OCRS][without] 5 FAIL
208.029 (134.269)
two_to_two_to_n.c [OCRS][without] 7 FAIL
1.684
Total Below Time = 2415.345 (was 1243.074)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c [OCRS][without] 1 PASS
0.323
exp_add_loop_rec.c [OCRS][without] 1 FAIL
0.363
exp_add_loop_variable.c [OCRS][without] 1 PASS
0.356
exp_with_linear_inner_loop.c [OCRS][without] 1 FAIL
0.414
linear_two_to_n.c [OCRS][without] 8 FAIL
1.574 (1.338)
loop_five_to_n.c [OCRS][without] 1 FAIL
0.355
non_loop_five_to_n.c [OCRS][without] 8 FAIL
9.8 (8.79)
power_log.c [OCRS][without] 1 PASS
0.414 (0.375)
power_log_modified.c [OCRS][without] 1 PASS
0.478 (0.386)
simple_exponential.c [OCRS][without] 1 PASS
0.348
simple_exponential_for.c [OCRS][without] 1 PASS
0.355
two_to_n_minus_n.c [OCRS][without] 8 FAIL
1.816 (1.636)
two_to_n_minus_n_loop.c [OCRS][without] 8 FAIL
2.693
Total Below Time = 19.289 (was 17.594)

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