[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: ec42b354b66f3431bf96ccb9826b656af28914b9 (2017-04-18 07:32:57 -0400) "Updated which variables get havoked"

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.388
kmp.c [OCRS][without] 1 PASS
1.33 (1.155)
qsort.c [OCRS][without] 4 PASS
2.666 (2.025)
speed_pldi09_fig1.c [OCRS][without] 1 PASS
0.381
speed_pldi09_fig4_2.c [OCRS][without] 1 FAIL
0.396
speed_pldi09_fig4_4.c [OCRS][without] 1 PASS
0.459
speed_pldi09_fig4_5.c [OCRS][without] 1 PASS
0.4
speed_pldi10_ex1.c [OCRS][without] 1 PASS
3.889 (0.834)
speed_pldi10_ex3.c [OCRS][without] 1 PASS
0.471
speed_pldi10_ex4.c [OCRS][without] EXCEPTION
0.412
speed_popl10_fig2_1.c [OCRS][without] 1 PASS
0.394
speed_popl10_fig2_2.c [OCRS][without] 1 FAIL
0.357
speed_popl10_nested_multiple.c [OCRS][without] 1 PASS
0.428
speed_popl10_nested_single.c [OCRS][without] 1 PASS
0.407
speed_popl10_sequential_single.c [OCRS][without] 1 PASS
0.358
speed_popl10_simple_multiple.c [OCRS][without] 1 PASS
0.4
speed_popl10_simple_single_2.c [OCRS][without] 1 PASS
0.43
speed_popl10_simple_single.c [OCRS][without] 1 PASS
0.337
t07.c [OCRS][without] 1 PASS
0.365
t08.c [OCRS][without] 1 PASS
0.358
t09.c [OCRS][without] 1 PASS
0.355
t10.c [OCRS][without] 1 PASS
0.355
t11.c [OCRS][without] 1 PASS
0.389
t13.c [OCRS][without] 1 FAIL
0.41
t15.c [OCRS][without] 1 PASS
0.378
t16.c [OCRS][without] 1 PASS
0.353
t19.c [OCRS][without] 1 PASS
0.341
t20.c [OCRS][without] 1 PASS
0.345
t27.c [OCRS][without] 1 PASS
0.428
t28.c [OCRS][without] 1 PASS
0.382
t30.c [OCRS][without] 1 FAIL
0.357
t37.c [OCRS][without] 2 PASS
0.5
t39.c [OCRS][without] 2 PASS
0.488
t46.c [OCRS][without] 1 PASS
0.359
t47.c [OCRS][without] 1 PASS
0.354
Total Below Time = 20.42 (was 16.316)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c [OCRS][without] 2 PASS
PASS
0.385
qsort_full.c [OCRS][without] 4 TIMEOUT
300.004 (43.087)
rec1-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.343
rec1-param_unsafe.c [OCRS][without] 2 PASS
0.355
rec1_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.34
rec1_unsafe.c [OCRS][without] 2 PASS
0.342
rec2-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.345
rec2-param_unsafe.c [OCRS][without] 2 PASS
0.356
rec2_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.345
rec2_unsafe.c [OCRS][without] 2 PASS
0.331
rec-test.c [OCRS][without] 2 PASS
0.325
sas03_bothbranches.c [OCRS][without] 7 PASS
1.283
sas03.c [OCRS][without] 2 PASS
0.813
simulated_lese_recursive.c [OCRS][without] 2 PASS
0.39
Total Below Time = 305.957 (was 49.044)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c [OCRS][without] 1 PASS
0.333
count_up_down_unsafe.c [OCRS][without] 1 PASS
0.316
divide.c [OCRS][without] 1 PASS
0.332
factor_unsafe.c [OCRS][without] TIMEOUT
300.005
for_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.309
for_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.314
interproc.c [OCRS][without] 1 PASS
0.313
mult.c [OCRS][without] 1 PASS
PASS
0.35
pointer_arith.c [OCRS][without] 1 PASS
PASS
PASS
PASS
0.327
quotient.c [OCRS][without] 3 PASS
0.425
subtract.c [OCRS][without] 1 PASS
0.324
sum01_bug02_sum01_bug02_base.case_unsafe.c [OCRS][without] 1 PASS
0.343
sum01_bug02_unsafe.c [OCRS][without] 1 PASS
0.397
sum01_real_safe.c [OCRS][without] 1 PASS
0.339
sum01_safe.c [OCRS][without] 1 PASS
0.34
sum01_unsafe.c [OCRS][without] 1 PASS
0.366
sum02_safe.c [OCRS][without] 1 PASS
0.326
sum03_safe.c [OCRS][without] 1 PASS
0.337
sum03_unsafe.c [OCRS][without] 1 PASS
0.404
sum04_safe.c [OCRS][without] 1 PASS
0.31
sum04_unsafe.c [OCRS][without] 1 PASS
0.354
terminator_02_safe.c [OCRS][without] 1 PASS
0.343
terminator_02_unsafe.c [OCRS][without] 1 PASS
0.355
terminator_03_safe.c [OCRS][without] 1 PASS
0.342
terminator_03_unsafe.c [OCRS][without] 1 PASS
0.335
token_ring01_safe.c [OCRS][without] TIMEOUT
300.007
token_ring01_unsafe.c [OCRS][without] TIMEOUT
300.005
toy_safe.c [OCRS][without] EXCEPTION
180.171
trex01_safe.c [OCRS][without] 1 PASS
0.732
trex01_unsafe.c [OCRS][without] 1 PASS
0.387 (0.351)
trex02_safe2.c [OCRS][without] 3 PASS
0.396
trex02_safe.c [OCRS][without] 3 PASS
0.386
trex02_unsafe.c [OCRS][without] 3 PASS
0.398
trex03_safe.c [OCRS][without] 1 PASS
0.461
trex03_unsafe.c [OCRS][without] 1 PASS
0.456 (0.414)
trex04_safe.c [OCRS][without] 1 PASS
0.344
while_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.311
while_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.315
while_infinite_loop_3_safe.c [OCRS][without] 1 PASS
0.326
Total Below Time = 1092.934 (was 1082.221)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c [OCRS][without] 3 PASS
0.464
blogger_simplified1.c [OCRS][without] 3 PASS
0.995
divided_difference2.c [OCRS][without] TIMEOUT
300.006
mult-proc.c [OCRS][without] 3 PASS
PASS
0.363
mult-proc-params.c [OCRS][without] 3 PASS
PASS
0.392
popall.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
0.414
simulated_scc.c [OCRS][without] 1 PASS
PASS
0.51
Total Below Time = 303.144 (was 303.092)
/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 PASS
0.476
degree2_monomial.c [OCRS][without] 1 PASS
0.378
degree3_binomial.c [OCRS][without] 1 PASS
0.913 (0.816)
degree3_monomial.c [OCRS][without] 1 PASS
0.443
degree4_binomial.c [OCRS][without] 1 PASS
1.147
degree4_monomial.c [OCRS][without] 1 PASS
0.494
degree5_binomial.c [OCRS][without] 1 PASS
1.759
degree5_monomial.c [OCRS][without] 1 PASS
0.576
Total Below Time = 6.535 (was 6.391)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c [OCRS][without] 1 PASS
0.345
cubic_with_square_interproc.c [OCRS][without] 2 PASS
0.38
cubic_with_square_nonlinear.c [OCRS][without] 1 PASS
0.353
cubic_with_square_nonlinear_interproc.c [OCRS][without] 2 PASS
0.359
cubic_with_square_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.366
cubic_with_square_unsafe.c [OCRS][without] 1 PASS
0.353
multi-input.c [OCRS][without] 1 PASS
0.391
multi-input_unsafe.c [OCRS][without] 1 PASS
0.45
nondet_loop_bound.c [OCRS][without] 1 PASS
0.354
nondet_loop_bound_quartic.c [OCRS][without] 1 PASS
0.365
nondet_loop_bound_quartic_unsafe.c [OCRS][without] 1 PASS
0.37
nondet_loop_bound_unsafe.c [OCRS][without] 1 PASS
0.369
nonlinear_stratified.c [OCRS][without] 1 FAIL
0.369
nonlinear_stratified_unsafe.c [OCRS][without] 1 PASS
0.36
quartic_with_cube.c [OCRS][without] 1 PASS
0.348
quartic_with_cube_nonlinear.c [OCRS][without] 1 PASS
0.371
quartic_with_cube_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.386
quartic_with_cube_unsafe.c [OCRS][without] 1 PASS
0.353
quintic_with_quartic.c [OCRS][without] 1 PASS
0.365
quintic_with_quartic_nonlinear.c [OCRS][without] 1 PASS
0.371
quintic_with_quartic_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.379 (0.47)
quintic_with_quartic_unsafe.c [OCRS][without] 1 PASS
0.368
Total Below Time = 8.125 (was 8.25)
/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.719 (3.135)
degree2_FD_AllAux_FewAssm.c [OCRS][without] 1 PASS
5.563 (3.172)
degree2_FD_FewAux_FewAssm.c [OCRS][without] 1 PASS
0.724
degree2_FD_FewAux_FewAssm_NonLinAsrt.c [OCRS][without] 1 PASS
0.697
degree3.c [OCRS][without] 1 PASS
0.541
degree3_FD.c [OCRS][without] 1 PASS
0.714
degree4.c [OCRS][without] 1 PASS
0.401
Total Below Time = 12.877 (was 9.889)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c [OCRS][without] 1 PASS
0.386
loop_unsafe.c [OCRS][without] 1 PASS
0.42
simulated_lese_parser.c [OCRS][without] 1 PASS
0.329
simulated_lese_sentinel.c [OCRS][without] 1 PASS
0.347
Total Below Time = 1.482 (was 1.443)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c [OCRS][without] 1 PASS
PASS
PASS
0.352
Total Below Time = 0.352 (was 0.346)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c [OCRS][without] TIMEOUT
300.005
Total Below Time = 300.005 (was 300.008)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c [OCRS][without] 1 PASS
0.342
array_false-unreach-call2.c [OCRS][without] 1 PASS
0.36
array_false-unreach-call3.c [OCRS][without] 1 PASS
0.345
array_true-unreach-call1.c [OCRS][without] 1 FAIL
0.355
array_true-unreach-call2.c [OCRS][without] 1 FAIL
0.364
array_true-unreach-call3.c [OCRS][without] 1 PASS
0.346
array_true-unreach-call4.c [OCRS][without] 1 FAIL
0.348
const_false-unreach-call1.c [OCRS][without] 1 PASS
0.308
const_true-unreach-call1.c [OCRS][without] 1 PASS
0.321
diamond_false-unreach-call1.c [OCRS][without] 1 PASS
0.338
diamond_true-unreach-call1.c [OCRS][without] 1 PASS
0.336
diamond_true-unreach-call2.c [OCRS][without] 1 PASS
0.379
functions_false-unreach-call1.c [OCRS][without] 3 PASS
0.361
functions_true-unreach-call1.c [OCRS][without] 3 PASS
0.356
multivar_false-unreach-call1.c [OCRS][without] 1 PASS
0.335
multivar_true-unreach-call1.c [OCRS][without] 1 PASS
0.315
nested_false-unreach-call1.c [OCRS][without] 1 PASS
0.326
nested_true-unreach-call1.c [OCRS][without] 1 PASS
0.338
overflow_true-unreach-call1.c [OCRS][without] 1 PASS
0.315
phases_false-unreach-call1.c [OCRS][without] 1 PASS
0.329
phases_false-unreach-call2.c [OCRS][without] 1 PASS
0.324
phases_true-unreach-call1.c [OCRS][without] 1 PASS
0.329
phases_true-unreach-call2.c [OCRS][without] 1 PASS
0.324
simple_false-unreach-call1.c [OCRS][without] 1 PASS
0.308
simple_false-unreach-call2.c [OCRS][without] 1 PASS
0.316
simple_false-unreach-call3.c [OCRS][without] 1 PASS
0.315
simple_false-unreach-call4.c [OCRS][without] 1 PASS
0.334
simple_true-unreach-call1.c [OCRS][without] 1 PASS
0.317
simple_true-unreach-call2.c [OCRS][without] 1 PASS
0.307
simple_true-unreach-call3.c [OCRS][without] 1 PASS
0.318
simple_true-unreach-call4.c [OCRS][without] 1 PASS
0.325
underapprox_false-unreach-call1.c [OCRS][without] 1 PASS
0.326
underapprox_false-unreach-call2.c [OCRS][without] 1 PASS
0.336
underapprox_true-unreach-call1.c [OCRS][without] 1 FAIL
0.333
underapprox_true-unreach-call2.c [OCRS][without] 1 PASS
0.321
Total Below Time = 11.65 (was 11.633)
/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.887
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.458
down_true-unreach-call.c [OCRS][without] 1 PASS
0.324
fragtest_simple_true-unreach-call.c [OCRS][without] 1 PASS
0.393
half_2_true-unreach-call.c [OCRS][without] 1 PASS
0.345
heapsort_true-unreach-call.c [OCRS][without] 1 TIMEOUT
300.151 (2.351)
id_build_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.327
id_trans_false-unreach-call.c [OCRS][without] 1 FAIL
FAIL
FAIL
PASS
0.338
large_const_true-unreach-call.c [OCRS][without] 1 PASS
0.415
MADWiFi-encode_ie_ok_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.367
nested6_true-unreach-call.c [OCRS][without] 1 FAIL
FAIL
PASS
0.414
nested9_true-unreach-call.c [OCRS][without] 1 PASS
0.475
nest-if3_true-unreach-call.c [OCRS][without] 1 PASS
0.411
NetBSD_loop_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.339
sendmail-close-angle_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.382
seq_true-unreach-call.c [OCRS][without] 1 PASS
0.376
SpamAssassin-loop_true-unreach-call.c [OCRS][without] TIMEOUT
300.111 (1.2)
string_concat-noarr_true-unreach-call.c [OCRS][without] 1 PASS
0.347
up_true-unreach-call.c [OCRS][without] 1 PASS
0.325
Total Below Time = 607.185 (was 10.396)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c [OCRS][without] 1 PASS
0.323
bhmr2007_true-unreach-call.c [OCRS][without] 1 PASS
0.357
cggmp2005b_true-unreach-call.c [OCRS][without] 1 PASS
0.401
cggmp2005_true-unreach-call.c [OCRS][without] 1 PASS
0.322
cggmp2005_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.336
css2003_true-unreach-call.c [OCRS][without] 1 PASS
0.488
ddlm2013_true-unreach-call.c [OCRS][without] 1 PASS
0.387
gcnr2008_false-unreach-call.c [OCRS][without] 1 TIMEOUT
300.153 (0.904)
gj2007b_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
0.348
gj2007_true-unreach-call.c [OCRS][without] 1 PASS
0.35
gr2006_true-unreach-call.c [OCRS][without] 1 PASS
0.34
gsv2008_true-unreach-call.c [OCRS][without] 1 PASS
0.318
hhk2008_true-unreach-call.c [OCRS][without] 1 PASS
0.331
jm2006_true-unreach-call.c [OCRS][without] 1 PASS
0.345
jm2006_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.36
mcmillan2006_true-unreach-call.c [OCRS][without] 1 FAIL
0.384
Total Below Time = 305.543 (was 6.275)
/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.317
count_by_1_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.348
count_by_2_true-unreach-call.c [OCRS][without] 1 PASS
0.32
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.349
gauss_sum_true-unreach-call.c [OCRS][without] 1 PASS
0.341
half_true-unreach-call.c [OCRS][without] EXCEPTION
0.344 (0.388)
nested_true-unreach-call.c [OCRS][without] 1 PASS
0.391
Total Below Time = 2.734 (was 2.803)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c [OCRS][without] 1 PASS
0.429
array_true-unreach-call.c [OCRS][without] 1 FAIL
0.415
bubble_sort_false-unreach-call.c [OCRS][without] EXCEPTION
105.075 (139.227)
bubble_sort_true-unreach-call.c [OCRS][without] TIMEOUT
300.005
compact_false-unreach-call.c [OCRS][without] 1 PASS
0.371
count_up_down_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.321
count_up_down_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.326
eureka_01_false-unreach-call.c [OCRS][without] 1 PASS
2.195
eureka_01_true-unreach-call.c [OCRS][without] 1 FAIL
1.952
eureka_05_true-unreach-call.c [OCRS][without] 1 FAIL
1.109 (0.747)
for_bounded_loop1_false-unreach-call_true-termination.c [OCRS][without] 1 FAIL
FAIL
PASS
0.324
for_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.311
for_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.324
heavy_false-unreach-call.c [OCRS][without] 1 PASS
0.538
heavy_true-unreach-call.c [OCRS][without] 1 PASS
0.498
insertion_sort_false-unreach-call.c [OCRS][without] 1 PASS
2.16
insertion_sort_true-unreach-call.c [OCRS][without] 1 FAIL
0.747
invert_string_false-unreach-call.c [OCRS][without] 1 PASS
0.499
invert_string_true-unreach-call.c [OCRS][without] 1 FAIL
0.503
linear_sea.ch_true-unreach-call.c [OCRS][without] 1 FAIL
0.372
linear_search_false-unreach-call.c [OCRS][without] 1 EXCEPTION
0.419
lu.cmp_true-unreach-call.c [OCRS][without] TIMEOUT
300.267 (122.39)
ludcmp_false-unreach-call.c [OCRS][without] TIMEOUT
300.272 (121.244)
matrix_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.977 (0.813)
matrix_true-unreach-call_true-termination.c [OCRS][without] 1 FAIL
0.502
n.c11_true-unreach-call.c [OCRS][without] 3 FAIL
0.482
n.c24_false-unreach-call.c [OCRS][without] 3 PASS
23.139
n.c40_true-unreach-call.c [OCRS][without] 1 FAIL
0.366
nec11_false-unreach-call.c [OCRS][without] 1 PASS
0.376
nec20_false-unreach-call.c [OCRS][without] 1 PASS
0.364
nec40_true-unreach-call.c [OCRS][without] 1 FAIL
0.391
string_false-unreach-call.c [OCRS][without] 1 PASS
0.636
string_true-unreach-call.c [OCRS][without] 1 FAIL
0.652
sum01_bug02_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.369
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.339
sum01_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.364
sum01_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.326
sum03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.473
sum03_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.348
sum04_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.358
sum04_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.338
sum_array_false-unreach-call.c [OCRS][without] 1 PASS
0.647
sum_array_true-unreach-call.c [OCRS][without] 1 FAIL
0.706
terminator_01_false-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.326
terminator_02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.424
terminator_02_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.336
terminator_03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.325
terminator_03_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.322
trex01_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.465
trex01_true-unreach-call.c [OCRS][without] 3 PASS
0.802 (0.668)
trex02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.374
trex02_true-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.397
trex03_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.866
trex03_true-unreach-call.c [OCRS][without] 3 PASS
0.845
trex04_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.363
veris.c_NetBSD-libc__loop_true-unreach-call.c [OCRS][without] 1 PASS
0.337
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c [OCRS][without] 3 23.806
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c [OCRS][without] 1 PASS
0.368
verisec_NetBSD-libc__loop_false-unreach-call.c [OCRS][without] 1 PASS
0.345
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c [OCRS][without] 3 PASS
16.964
vogal_false-unreach-call.c [OCRS][without] 1 PASS
0.844
vogal_true-unreach-call.c [OCRS][without] 1 FAIL
0.86 (0.772)
while_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.312
while_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.318
while_infinite_loop_3_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.329
while_infinite_loop_4_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.312
Total Below Time = 1102.225 (was 779.065)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c [OCRS][without] TIMEOUT
300.033 (2.458)
Ackermann02_false-unreach-call_false-termination.c [OCRS][without] TIMEOUT
300.031 (2.347)
Ackermann03_true-unreach-call.c [OCRS][without] TIMEOUT
300.024 (2.455)
Ackermann04_true-unreach-call.c [OCRS][without] TIMEOUT
300.021 (2.482)
Addition01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.577
Addition02_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.566
Addition03_false-no-overflow.c [OCRS][without] 2 PASS
0.56
Addition03_true-unreach-call.c [OCRS][without] 2 PASS
0.581
BallRajamani-SPIN2000-Fig1_false-unreach-call.c [OCRS][without] 2 PASS
0.444
EvenOdd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.418
EvenOdd03_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.435
Fibonacci01_true-unreach-call.c [OCRS][without] EXCEPTION
0.945 (300.01)
Fibonacci02_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.944 (300.011)
Fibonacci03_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.955 (300.007)
Fibonacci04_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.979 (300.008)
Fibonacci05_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
1.0 (300.011)
gcd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.532
gcd02_true-unreach-call.c [OCRS][without] 2 FAIL
PASS
1.375 (1.213)
McCarthy91_false-unreach-call_false-termination.c [OCRS][without] 7 PASS
1.444 (1.158)
McCarthy91_true-unreach-call.c [OCRS][without] 7 FAIL
1.432 (1.115)
MultCommutative_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.682 (0.608)
Primes_true-unreach-call.c [OCRS][without] 3 FAIL
2.13
recHanoi01_true-unreach-call_true-termination.c [OCRS][without] 9 FAIL
5.831
recHanoi02_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.382
recHanoi03_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.387
Total Below Time = 1222.708 (was 1526.517)
/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.419
afterrec_2calls_true-unreach-call.c [OCRS][without] 2 PASS
PASS
0.376
afterrec_false-unreach-call.c [OCRS][without] 2 PASS
0.366
afterrec_true-unreach-call.c [OCRS][without] 2 PASS
0.346
fibo_10_false-unreach-call.c [OCRS][without] EXCEPTION
0.952 (300.005)
fibo_10_true-unreach-call.c [OCRS][without] EXCEPTION
0.949 (300.008)
fibo_15_false-unreach-call.c [OCRS][without] EXCEPTION
0.994 (300.009)
fibo_15_true-unreach-call.c [OCRS][without] EXCEPTION
1.001 (300.008)
fibo_20_false-unreach-call.c [OCRS][without] EXCEPTION
0.975 (300.008)
fibo_20_true-unreach-call.c [OCRS][without] EXCEPTION
0.942 (300.012)
fibo_25_false-unreach-call.c [OCRS][without] EXCEPTION
0.978 (300.009)
fibo_25_true-unreach-call.c [OCRS][without] EXCEPTION
0.952 (300.009)
fibo_2calls_10_false-unreach-call.c [OCRS][without] EXCEPTION
17.116 (133.0)
fibo_2calls_10_true-unreach-call.c [OCRS][without] EXCEPTION
17.268 (129.358)
fibo_2calls_15_false-unreach-call.c [OCRS][without] EXCEPTION
17.108 (129.059)
fibo_2calls_15_true-unreach-call.c [OCRS][without] EXCEPTION
17.078 (131.107)
fibo_2calls_20_false-unreach-call.c [OCRS][without] EXCEPTION
17.048 (128.561)
fibo_2calls_20_true-unreach-call.c [OCRS][without] EXCEPTION
17.247 (132.049)
fibo_2calls_25_false-unreach-call.c [OCRS][without] EXCEPTION
17.354 (128.895)
fibo_2calls_25_true-unreach-call.c [OCRS][without] EXCEPTION
17.34 (126.984)
fibo_2calls_2_false-unreach-call.c [OCRS][without] EXCEPTION
17.307 (131.283)
fibo_2calls_2_true-unreach-call.c [OCRS][without] EXCEPTION
17.914 (128.716)
fibo_2calls_4_false-unreach-call.c [OCRS][without] EXCEPTION
17.254 (128.613)
fibo_2calls_4_true-unreach-call.c [OCRS][without] EXCEPTION
17.382 (128.422)
fibo_2calls_5_false-unreach-call.c [OCRS][without] EXCEPTION
17.101 (130.842)
fibo_2calls_5_true-unreach-call.c [OCRS][without] EXCEPTION
17.204 (129.27)
fibo_2calls_6_false-unreach-call.c [OCRS][without] EXCEPTION
17.198 (132.124)
fibo_2calls_6_true-unreach-call.c [OCRS][without] EXCEPTION
17.325 (131.614)
fibo_2calls_8_false-unreach-call.c [OCRS][without] EXCEPTION
17.333 (128.874)
fibo_2calls_8_true-unreach-call.c [OCRS][without] EXCEPTION
17.093 (129.632)
fibo_5_false-unreach-call.c [OCRS][without] EXCEPTION
0.959 (300.009)
fibo_5_true-unreach-call.c [OCRS][without] EXCEPTION
0.954 (300.01)
fibo_7_false-unreach-call.c [OCRS][without] EXCEPTION
0.946 (300.008)
fibo_7_true-unreach-call.c [OCRS][without] EXCEPTION
0.938 (300.009)
id2_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.974
id2_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.978
id2_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.942
id2_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.983
id2_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.42
id2_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.409
id_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.578
id_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.584
id_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.58
id_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.577
id_i10_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.368
id_i10_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.363
id_i15_o15_false-unreach-call.c [OCRS][without] 2 PASS
0.379
id_i15_o15_true-unreach-call.c [OCRS][without] 2 PASS
0.4
id_i20_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.383
id_i20_o20_true-unreach-call.c [OCRS][without] 2 PASS
0.375
id_i25_o25_false-unreach-call.c [OCRS][without] 2 PASS
0.38
id_i25_o25_true-unreach-call.c [OCRS][without] 2 PASS
0.376
id_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.384
id_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.36
id_o1000_false-unreach-call.c [OCRS][without] 2 PASS
0.379
id_o100_false-unreach-call.c [OCRS][without] 2 PASS
0.369
id_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.375
id_o200_false-unreach-call.c [OCRS][without] 2 PASS
0.387
id_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.369
id_o3_false-unreach-call.c [OCRS][without] 2 PASS
0.379
sum_10x0_false-unreach-call.c [OCRS][without] 2 PASS
0.391
sum_10x0_true-unreach-call.c [OCRS][without] 2 PASS
0.387
sum_15x0_false-unreach-call.c [OCRS][without] 2 PASS
0.416
sum_15x0_true-unreach-call.c [OCRS][without] 2 PASS
0.378
sum_20x0_false-unreach-call.c [OCRS][without] 2 PASS
0.379
sum_20x0_true-unreach-call.c [OCRS][without] 2 PASS
0.378
sum_25x0_false-unreach-call.c [OCRS][without] 2 PASS
0.394
sum_25x0_true-unreach-call.c [OCRS][without] 2 PASS
0.39
sum_2x3_false-unreach-call.c [OCRS][without] 2 PASS
0.388
sum_2x3_true-unreach-call.c [OCRS][without] 2 PASS
0.381
sum_non_eq_false-unreach-call.c [OCRS][without] 2 PASS
0.431
sum_non_eq_true-unreach-call.c [OCRS][without] 2 PASS
0.43
sum_non_false-unreach-call.c [OCRS][without] 2 PASS
0.406
sum_non_true-unreach-call.c [OCRS][without] 2 PASS
0.373
Total Below Time = 342.29 (was 5958.283)
/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.373
rec-bhmr2007_true-unreach-call.c [OCRS][without] 2 PASS
0.39
rec-cggmp2005b_true-unreach-call.c [OCRS][without] 3 PASS
0.744
rec-cggmp2005_true-unreach-call.c [OCRS][without] 2 PASS
0.338
rec-cggmp2005_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.355
rec-css2003_true-unreach-call.c [OCRS][without] 2 PASS
0.623
rec-ddlm2013_true-unreach-call.c [OCRS][without] EXCEPTION
0.339 (0.442)
rec-gcnr2008_false-unreach-call.c [OCRS][without] 2 PASS
0.894
rec-gj2007b_true-unreach-call.c [OCRS][without] 2 FAIL
FAIL
0.38
rec-gj2007_true-unreach-call.c [OCRS][without] 2 FAIL
0.385
rec-gr2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.399
rec-gsv2008_true-unreach-call.c [OCRS][without] 2 PASS
0.354
rec-hhk2008_true-unreach-call.c [OCRS][without] 2 PASS
0.347
rec-jm2006_true-unreach-call.c [OCRS][without] 2 PASS
0.372
rec-jm2006_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.4
rec-mcmillan2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.409
Total Below Time = 7.102 (was 7.259)
/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.332
rec-count_by_1_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.356
rec-count_by_2_true-unreach-call.c [OCRS][without] 2 PASS
0.326
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.373
rec-gauss_sum_true-unreach-call.c [OCRS][without] 2 PASS
0.357
rec-half_true-unreach-call.c [OCRS][without] EXCEPTION
0.352 (0.398)
rec-nested_true-unreach-call.c [OCRS][without] 3 PASS
0.585
Total Below Time = 3.035 (was 3.097)
/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 FAIL
297.353
edit_distance_top_down.c [OCRS][without] 3 FAIL
50.309
log_log_n_solution.c [OCRS][without] 3 FAIL
0.436 (0.852)
log_n_solution.c [OCRS][without] 2 FAIL
0.45
multivariate_1.c [OCRS][without] TIMEOUT
300.012
multivariate_higher_order.c [OCRS][without] 7 FAIL
FAIL
FAIL
26.015
n_cubed_solution.c [OCRS][without] EXCEPTION
0.348
n_log_n_solution.c [OCRS][without] TIMEOUT
300.028 (1.857)
n_squared_two_base_case_even.c [OCRS][without] 2 PASS
0.376
n_squared_two_base_case_odd.c [OCRS][without] 2 PASS
0.393
pascals_dynamic.c [OCRS][without] 3 FAIL
19.841
pascals_iterative.c [OCRS][without] 1 FAIL
5.299 (6.181)
pascals_recursive.c [OCRS][without] TIMEOUT
300.005
squared_solution.c [OCRS][without] TIMEOUT
300.142 (10.697)
two_n_even.c [OCRS][without] 2 PASS
0.375
two_n_odd.c [OCRS][without] 2 PASS
0.384
two_to_n_over_two_even.c [OCRS][without] TIMEOUT
300.037 (44.77)
two_to_n_over_two_odd.c [OCRS][without] TIMEOUT
300.024 (45.103)
two_to_n_squared.c [OCRS][without] 5 FAIL
206.1 (135.402)
two_to_two_to_n.c [OCRS][without] 7 FAIL
1.698
Total Below Time = 2410.135 (was 1247.526)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c [OCRS][without] 1 PASS
0.325
exp_add_loop_rec.c [OCRS][without] 1 FAIL
0.363
exp_add_loop_variable.c [OCRS][without] 1 PASS
0.369
exp_with_linear_inner_loop.c [OCRS][without] 1 FAIL
0.405
linear_two_to_n.c [OCRS][without] 8 FAIL
1.544 (1.371)
loop_five_to_n.c [OCRS][without] 1 FAIL
0.347
non_loop_five_to_n.c [OCRS][without] 8 FAIL
10.559 (8.897)
power_log.c [OCRS][without] 1 PASS
0.441 (0.37)
power_log_modified.c [OCRS][without] 1 PASS
0.482 (0.391)
simple_exponential.c [OCRS][without] 1 PASS
0.384 (0.341)
simple_exponential_for.c [OCRS][without] 1 PASS
0.355
two_to_n_minus_n.c [OCRS][without] 8 FAIL
1.82
two_to_n_minus_n_loop.c [OCRS][without] 8 FAIL
2.907 (2.627)
Total Below Time = 20.301 (was 17.807)

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