[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.379
kmp.c [OCRS][without] 1 PASS
1.407 (1.172)
qsort.c [OCRS][without] 4 PASS
2.652 (2.018)
speed_pldi09_fig1.c [OCRS][without] 1 PASS
0.383
speed_pldi09_fig4_2.c [OCRS][without] 1 FAIL
0.42
speed_pldi09_fig4_4.c [OCRS][without] 1 PASS
0.454
speed_pldi09_fig4_5.c [OCRS][without] 1 PASS
0.378
speed_pldi10_ex1.c [OCRS][without] 1 PASS
3.767 (0.825)
speed_pldi10_ex3.c [OCRS][without] 1 PASS
0.459
speed_pldi10_ex4.c [OCRS][without] EXCEPTION
0.409
speed_popl10_fig2_1.c [OCRS][without] 1 PASS
0.391
speed_popl10_fig2_2.c [OCRS][without] 1 FAIL
0.376
speed_popl10_nested_multiple.c [OCRS][without] 1 PASS
0.43
speed_popl10_nested_single.c [OCRS][without] 1 PASS
0.398
speed_popl10_sequential_single.c [OCRS][without] 1 PASS
0.339
speed_popl10_simple_multiple.c [OCRS][without] 1 PASS
0.416
speed_popl10_simple_single_2.c [OCRS][without] 1 PASS
0.425
speed_popl10_simple_single.c [OCRS][without] 1 PASS
0.333
t07.c [OCRS][without] 1 PASS
0.358
t08.c [OCRS][without] 1 PASS
0.337
t09.c [OCRS][without] 1 PASS
0.359
t10.c [OCRS][without] 1 PASS
0.354
t11.c [OCRS][without] 1 PASS
0.393
t13.c [OCRS][without] 1 FAIL
0.407
t15.c [OCRS][without] 1 PASS
0.369
t16.c [OCRS][without] 1 PASS
0.366
t19.c [OCRS][without] 1 PASS
0.345
t20.c [OCRS][without] 1 PASS
0.349
t27.c [OCRS][without] 1 PASS
0.419
t28.c [OCRS][without] 1 PASS
0.376
t30.c [OCRS][without] 1 FAIL
0.36
t37.c [OCRS][without] 2 PASS
0.469
t39.c [OCRS][without] 2 PASS
0.476
t46.c [OCRS][without] 1 PASS
0.384 (0.347)
t47.c [OCRS][without] 1 PASS
0.361 (0.423)
Total Below Time = 20.298 (was 16.505)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c [OCRS][without] 2 PASS
PASS
0.389
qsort_full.c [OCRS][without] 4 TIMEOUT
300.004 (42.474)
rec1-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.34 (0.39)
rec1-param_unsafe.c [OCRS][without] 2 PASS
0.343
rec1_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.321
rec1_unsafe.c [OCRS][without] 2 PASS
0.328
rec2-param_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.343
rec2-param_unsafe.c [OCRS][without] 2 PASS
0.364
rec2_safe.c [OCRS][without] 2 PASS
PASS
PASS
0.339
rec2_unsafe.c [OCRS][without] 2 PASS
0.333
rec-test.c [OCRS][without] 2 PASS
0.326
sas03_bothbranches.c [OCRS][without] 7 PASS
1.272
sas03.c [OCRS][without] 2 PASS
0.782
simulated_lese_recursive.c [OCRS][without] 2 PASS
0.383
Total Below Time = 305.867 (was 48.564)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c [OCRS][without] 1 PASS
0.319
count_up_down_unsafe.c [OCRS][without] 1 PASS
0.317
divide.c [OCRS][without] 1 PASS
0.322
factor_unsafe.c [OCRS][without] TIMEOUT
300.004
for_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.308
for_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.312
interproc.c [OCRS][without] 1 PASS
0.304
mult.c [OCRS][without] 1 PASS
PASS
0.318
pointer_arith.c [OCRS][without] 1 PASS
PASS
PASS
PASS
0.31
quotient.c [OCRS][without] 3 PASS
0.405
subtract.c [OCRS][without] 1 PASS
0.319
sum01_bug02_sum01_bug02_base.case_unsafe.c [OCRS][without] 1 PASS
0.338
sum01_bug02_unsafe.c [OCRS][without] 1 PASS
0.379
sum01_real_safe.c [OCRS][without] 1 PASS
0.321
sum01_safe.c [OCRS][without] 1 PASS
0.325
sum01_unsafe.c [OCRS][without] 1 PASS
0.358
sum02_safe.c [OCRS][without] 1 PASS
0.338
sum03_safe.c [OCRS][without] 1 PASS
0.333
sum03_unsafe.c [OCRS][without] 1 PASS
0.396
sum04_safe.c [OCRS][without] 1 PASS
0.323
sum04_unsafe.c [OCRS][without] 1 PASS
0.352
terminator_02_safe.c [OCRS][without] 1 PASS
0.325
terminator_02_unsafe.c [OCRS][without] 1 PASS
0.353
terminator_03_safe.c [OCRS][without] 1 PASS
0.319
terminator_03_unsafe.c [OCRS][without] 1 PASS
0.325
token_ring01_safe.c [OCRS][without] TIMEOUT
300.007
token_ring01_unsafe.c [OCRS][without] TIMEOUT
300.007
toy_safe.c [OCRS][without] EXCEPTION
173.311
trex01_safe.c [OCRS][without] 1 PASS
0.734
trex01_unsafe.c [OCRS][without] 1 PASS
0.377
trex02_safe2.c [OCRS][without] 3 PASS
0.375
trex02_safe.c [OCRS][without] 3 PASS
0.39
trex02_unsafe.c [OCRS][without] 3 PASS
0.383
trex03_safe.c [OCRS][without] 1 PASS
0.449
trex03_unsafe.c [OCRS][without] 1 PASS
0.445
trex04_safe.c [OCRS][without] 1 PASS
0.345
while_infinite_loop_1_safe.c [OCRS][without] 1 PASS
0.315
while_infinite_loop_2_safe.c [OCRS][without] 1 PASS
0.314
while_infinite_loop_3_safe.c [OCRS][without] 1 PASS
0.308
Total Below Time = 1085.783 (was 1076.128)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c [OCRS][without] 3 PASS
0.455
blogger_simplified1.c [OCRS][without] 3 PASS
0.985
divided_difference2.c [OCRS][without] TIMEOUT
300.006
mult-proc.c [OCRS][without] 3 PASS
PASS
0.356
mult-proc-params.c [OCRS][without] 3 PASS
PASS
0.397
popall.c [OCRS][without] 1 PASS
PASS
PASS
PASS
PASS
0.417
simulated_scc.c [OCRS][without] 1 PASS
PASS
0.516
Total Below Time = 303.132 (was 303.029)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c [OCRS][without] 1 PASS
0.348
degree2_binomial.c [OCRS][without] 1 PASS
0.466
degree2_monomial.c [OCRS][without] 1 PASS
0.419
degree3_binomial.c [OCRS][without] 1 PASS
0.899
degree3_monomial.c [OCRS][without] 1 PASS
0.418
degree4_binomial.c [OCRS][without] 1 PASS
1.172 (1.057)
degree4_monomial.c [OCRS][without] 1 PASS
0.494
degree5_binomial.c [OCRS][without] 1 PASS
1.691 (1.941)
degree5_monomial.c [OCRS][without] 1 PASS
0.579
Total Below Time = 6.486 (was 6.522)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c [OCRS][without] 1 PASS
0.328
cubic_with_square_interproc.c [OCRS][without] 2 PASS
0.404
cubic_with_square_nonlinear.c [OCRS][without] 1 PASS
0.353
cubic_with_square_nonlinear_interproc.c [OCRS][without] 2 PASS
0.378
cubic_with_square_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.357
cubic_with_square_unsafe.c [OCRS][without] 1 PASS
0.348
multi-input.c [OCRS][without] 1 PASS
0.401
multi-input_unsafe.c [OCRS][without] 1 PASS
0.441
nondet_loop_bound.c [OCRS][without] 1 PASS
0.356
nondet_loop_bound_quartic.c [OCRS][without] 1 PASS
0.373
nondet_loop_bound_quartic_unsafe.c [OCRS][without] 1 PASS
0.361
nondet_loop_bound_unsafe.c [OCRS][without] 1 PASS
0.386
nonlinear_stratified.c [OCRS][without] 1 FAIL
0.355
nonlinear_stratified_unsafe.c [OCRS][without] 1 PASS
0.354
quartic_with_cube.c [OCRS][without] 1 PASS
0.357
quartic_with_cube_nonlinear.c [OCRS][without] 1 PASS
0.383
quartic_with_cube_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.388
quartic_with_cube_unsafe.c [OCRS][without] 1 PASS
0.351
quintic_with_quartic.c [OCRS][without] 1 PASS
0.366
quintic_with_quartic_nonlinear.c [OCRS][without] 1 PASS
0.383
quintic_with_quartic_nonlinear_unsafe.c [OCRS][without] 1 PASS
0.377 (0.469)
quintic_with_quartic_unsafe.c [OCRS][without] 1 PASS
0.363
Total Below Time = 8.163 (was 8.265)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c [OCRS][without] 1 PASS
0.519
degree2_FD_AllAux_AllAssm.c [OCRS][without] 1 PASS
3.727 (3.084)
degree2_FD_AllAux_FewAssm.c [OCRS][without] 1 PASS
5.448 (3.094)
degree2_FD_FewAux_FewAssm.c [OCRS][without] 1 PASS
0.718
degree2_FD_FewAux_FewAssm_NonLinAsrt.c [OCRS][without] 1 PASS
0.727
degree3.c [OCRS][without] 1 PASS
0.547
degree3_FD.c [OCRS][without] 1 PASS
0.759
degree4.c [OCRS][without] 1 PASS
0.401
Total Below Time = 12.846 (was 9.767)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c [OCRS][without] 1 PASS
0.384
loop_unsafe.c [OCRS][without] 1 PASS
0.407
simulated_lese_parser.c [OCRS][without] 1 PASS
0.323
simulated_lese_sentinel.c [OCRS][without] 1 PASS
0.348
Total Below Time = 1.462 (was 1.476)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c [OCRS][without] 1 PASS
PASS
PASS
0.34
Total Below Time = 0.34 (was 0.349)
/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.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.355
array_false-unreach-call3.c [OCRS][without] 1 PASS
0.346
array_true-unreach-call1.c [OCRS][without] 1 FAIL
0.349
array_true-unreach-call2.c [OCRS][without] 1 FAIL
0.373
array_true-unreach-call3.c [OCRS][without] 1 PASS
0.349
array_true-unreach-call4.c [OCRS][without] 1 FAIL
0.343
const_false-unreach-call1.c [OCRS][without] 1 PASS
0.327
const_true-unreach-call1.c [OCRS][without] 1 PASS
0.33
diamond_false-unreach-call1.c [OCRS][without] 1 PASS
0.341
diamond_true-unreach-call1.c [OCRS][without] 1 PASS
0.337
diamond_true-unreach-call2.c [OCRS][without] 1 PASS
0.377
functions_false-unreach-call1.c [OCRS][without] 3 PASS
0.371
functions_true-unreach-call1.c [OCRS][without] 3 PASS
0.362
multivar_false-unreach-call1.c [OCRS][without] 1 PASS
0.331
multivar_true-unreach-call1.c [OCRS][without] 1 PASS
0.333
nested_false-unreach-call1.c [OCRS][without] 1 PASS
0.338
nested_true-unreach-call1.c [OCRS][without] 1 PASS
0.338
overflow_true-unreach-call1.c [OCRS][without] 1 PASS
0.336
phases_false-unreach-call1.c [OCRS][without] 1 PASS
0.334
phases_false-unreach-call2.c [OCRS][without] 1 PASS
0.343
phases_true-unreach-call1.c [OCRS][without] 1 PASS
0.338
phases_true-unreach-call2.c [OCRS][without] 1 PASS
0.343
simple_false-unreach-call1.c [OCRS][without] 1 PASS
0.313
simple_false-unreach-call2.c [OCRS][without] 1 PASS
0.321
simple_false-unreach-call3.c [OCRS][without] 1 PASS
0.312
simple_false-unreach-call4.c [OCRS][without] 1 PASS
0.324
simple_true-unreach-call1.c [OCRS][without] 1 PASS
0.325
simple_true-unreach-call2.c [OCRS][without] 1 PASS
0.321
simple_true-unreach-call3.c [OCRS][without] 1 PASS
0.314
simple_true-unreach-call4.c [OCRS][without] 1 PASS
0.318
underapprox_false-unreach-call1.c [OCRS][without] 1 PASS
0.322
underapprox_false-unreach-call2.c [OCRS][without] 1 PASS
0.329
underapprox_true-unreach-call1.c [OCRS][without] 1 FAIL
0.34
underapprox_true-unreach-call2.c [OCRS][without] 1 PASS
0.315
Total Below Time = 11.785 (was 11.637)
/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.826
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.482 (0.422)
down_true-unreach-call.c [OCRS][without] 1 PASS
0.324
fragtest_simple_true-unreach-call.c [OCRS][without] 1 PASS
0.378
half_2_true-unreach-call.c [OCRS][without] 1 PASS
0.348
heapsort_true-unreach-call.c [OCRS][without] 1 TIMEOUT
300.154 (2.338)
id_build_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.331
id_trans_false-unreach-call.c [OCRS][without] 1 FAIL
FAIL
FAIL
PASS
0.353
large_const_true-unreach-call.c [OCRS][without] 1 PASS
0.421
MADWiFi-encode_ie_ok_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.372
nested6_true-unreach-call.c [OCRS][without] 1 FAIL
FAIL
PASS
0.426
nested9_true-unreach-call.c [OCRS][without] 1 PASS
0.453
nest-if3_true-unreach-call.c [OCRS][without] 1 PASS
0.411
NetBSD_loop_true-unreach-call.c [OCRS][without] 1 PASS
PASS
0.334
sendmail-close-angle_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.392
seq_true-unreach-call.c [OCRS][without] 1 PASS
0.387
SpamAssassin-loop_true-unreach-call.c [OCRS][without] TIMEOUT
300.119 (1.233)
string_concat-noarr_true-unreach-call.c [OCRS][without] 1 PASS
0.345
up_true-unreach-call.c [OCRS][without] 1 PASS
0.336
Total Below Time = 607.192 (was 10.342)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c [OCRS][without] 1 PASS
0.329
bhmr2007_true-unreach-call.c [OCRS][without] 1 PASS
0.372
cggmp2005b_true-unreach-call.c [OCRS][without] 1 PASS
0.392
cggmp2005_true-unreach-call.c [OCRS][without] 1 PASS
0.324
cggmp2005_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.323
css2003_true-unreach-call.c [OCRS][without] 1 PASS
0.488
ddlm2013_true-unreach-call.c [OCRS][without] 1 PASS
0.388
gcnr2008_false-unreach-call.c [OCRS][without] 1 TIMEOUT
300.146 (0.876)
gj2007b_true-unreach-call.c [OCRS][without] 1 PASS
FAIL
0.338
gj2007_true-unreach-call.c [OCRS][without] 1 PASS
0.328
gr2006_true-unreach-call.c [OCRS][without] 1 PASS
0.352
gsv2008_true-unreach-call.c [OCRS][without] 1 PASS
0.323
hhk2008_true-unreach-call.c [OCRS][without] 1 PASS
0.327
jm2006_true-unreach-call.c [OCRS][without] 1 PASS
0.361
jm2006_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.36
mcmillan2006_true-unreach-call.c [OCRS][without] 1 FAIL
0.375
Total Below Time = 305.526 (was 6.282)
/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.312
count_by_1_variant_true-unreach-call.c [OCRS][without] 1 PASS
0.333
count_by_2_true-unreach-call.c [OCRS][without] 1 PASS
0.323
count_by_k_true-unreach-call.c [OCRS][without] 1 PASS
0.348
count_by_nondet_true-unreach-call.c [OCRS][without] 1 FAIL
0.33
gauss_sum_true-unreach-call.c [OCRS][without] 1 PASS
0.331
half_true-unreach-call.c [OCRS][without] EXCEPTION
0.348
nested_true-unreach-call.c [OCRS][without] 1 PASS
0.391
Total Below Time = 2.716 (was 2.697)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c [OCRS][without] 1 PASS
0.415
array_true-unreach-call.c [OCRS][without] 1 FAIL
0.403
bubble_sort_false-unreach-call.c [OCRS][without] EXCEPTION
104.541 (138.953)
bubble_sort_true-unreach-call.c [OCRS][without] TIMEOUT
300.004
compact_false-unreach-call.c [OCRS][without] 1 PASS
0.366
count_up_down_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.32
count_up_down_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.328
eureka_01_false-unreach-call.c [OCRS][without] 1 PASS
2.169
eureka_01_true-unreach-call.c [OCRS][without] 1 FAIL
1.961
eureka_05_true-unreach-call.c [OCRS][without] 1 FAIL
1.061 (0.738)
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.319
for_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.33
heavy_false-unreach-call.c [OCRS][without] 1 PASS
0.541
heavy_true-unreach-call.c [OCRS][without] 1 PASS
0.515
insertion_sort_false-unreach-call.c [OCRS][without] 1 PASS
2.176
insertion_sort_true-unreach-call.c [OCRS][without] 1 FAIL
0.746
invert_string_false-unreach-call.c [OCRS][without] 1 PASS
0.511
invert_string_true-unreach-call.c [OCRS][without] 1 FAIL
0.502
linear_sea.ch_true-unreach-call.c [OCRS][without] 1 FAIL
0.374
linear_search_false-unreach-call.c [OCRS][without] 1 EXCEPTION
0.41
lu.cmp_true-unreach-call.c [OCRS][without] TIMEOUT
300.274 (124.699)
ludcmp_false-unreach-call.c [OCRS][without] TIMEOUT
300.253 (123.047)
matrix_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.975 (0.811)
matrix_true-unreach-call_true-termination.c [OCRS][without] 1 FAIL
0.519
n.c11_true-unreach-call.c [OCRS][without] 3 FAIL
0.466
n.c24_false-unreach-call.c [OCRS][without] 3 PASS
23.71
n.c40_true-unreach-call.c [OCRS][without] 1 FAIL
0.381
nec11_false-unreach-call.c [OCRS][without] 1 PASS
0.375
nec20_false-unreach-call.c [OCRS][without] 1 PASS
0.355
nec40_true-unreach-call.c [OCRS][without] 1 FAIL
0.353
string_false-unreach-call.c [OCRS][without] 1 PASS
0.653
string_true-unreach-call.c [OCRS][without] 1 FAIL
0.643
sum01_bug02_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.375
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.348
sum01_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.363
sum01_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.342
sum03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.494
sum03_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.367
sum04_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.363
sum04_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.317
sum_array_false-unreach-call.c [OCRS][without] 1 PASS
0.655
sum_array_true-unreach-call.c [OCRS][without] 1 FAIL
0.714
terminator_01_false-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.321
terminator_02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.405
terminator_02_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.353
terminator_03_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.34
terminator_03_true-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.331
trex01_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.467
trex01_true-unreach-call.c [OCRS][without] 3 PASS
0.807 (0.66)
trex02_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.387
trex02_true-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.435 (0.381)
trex03_false-unreach-call_true-termination.c [OCRS][without] 3 PASS
0.848
trex03_true-unreach-call.c [OCRS][without] 3 PASS
0.854
trex04_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.379
veris.c_NetBSD-libc__loop_true-unreach-call.c [OCRS][without] 1 PASS
0.357
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c [OCRS][without] 3 24.039
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c [OCRS][without] 1 PASS
0.359
verisec_NetBSD-libc__loop_false-unreach-call.c [OCRS][without] 1 PASS
0.357
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c [OCRS][without] 3 PASS
17.122
vogal_false-unreach-call.c [OCRS][without] 1 PASS
0.865 (0.776)
vogal_true-unreach-call.c [OCRS][without] 1 FAIL
0.855 (0.763)
while_infinite_loop_1_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.313
while_infinite_loop_2_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.312
while_infinite_loop_3_true-unreach-call_false-termination.c [OCRS][without] 1 PASS
0.324
while_infinite_loop_4_false-unreach-call_true-termination.c [OCRS][without] 1 PASS
0.334
Total Below Time = 1102.792 (was 782.567)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c [OCRS][without] TIMEOUT
300.021 (2.419)
Ackermann02_false-unreach-call_false-termination.c [OCRS][without] TIMEOUT
300.02 (2.267)
Ackermann03_true-unreach-call.c [OCRS][without] TIMEOUT
300.021 (2.453)
Ackermann04_true-unreach-call.c [OCRS][without] TIMEOUT
300.021 (2.423)
Addition01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.566
Addition02_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.582
Addition03_false-no-overflow.c [OCRS][without] 2 PASS
0.558
Addition03_true-unreach-call.c [OCRS][without] 2 PASS
0.574
BallRajamani-SPIN2000-Fig1_false-unreach-call.c [OCRS][without] 2 PASS
0.455
EvenOdd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.443
EvenOdd03_false-unreach-call_false-termination.c [OCRS][without] 2 PASS
0.423
Fibonacci01_true-unreach-call.c [OCRS][without] EXCEPTION
0.99 (300.01)
Fibonacci02_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.947 (300.009)
Fibonacci03_true-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.953 (300.011)
Fibonacci04_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.969 (300.007)
Fibonacci05_false-unreach-call_true-termination.c [OCRS][without] EXCEPTION
0.953 (300.009)
gcd01_true-unreach-call_true-termination.c [OCRS][without] 2 PASS
0.541
gcd02_true-unreach-call.c [OCRS][without] 2 FAIL
PASS
1.351 (1.196)
McCarthy91_false-unreach-call_false-termination.c [OCRS][without] 7 PASS
1.457 (1.158)
McCarthy91_true-unreach-call.c [OCRS][without] 7 FAIL
1.465 (1.1)
MultCommutative_true-unreach-call_true-termination.c [OCRS][without] 2 FAIL
0.691 (0.602)
Primes_true-unreach-call.c [OCRS][without] 3 FAIL
2.13
recHanoi01_true-unreach-call_true-termination.c [OCRS][without] 9 FAIL
5.728
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.374
Total Below Time = 1222.61 (was 1526.397)
/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.427
afterrec_2calls_true-unreach-call.c [OCRS][without] 2 PASS
PASS
0.359
afterrec_false-unreach-call.c [OCRS][without] 2 PASS
0.361
afterrec_true-unreach-call.c [OCRS][without] 2 PASS
0.357
fibo_10_false-unreach-call.c [OCRS][without] EXCEPTION
0.938 (300.01)
fibo_10_true-unreach-call.c [OCRS][without] EXCEPTION
0.952 (300.005)
fibo_15_false-unreach-call.c [OCRS][without] EXCEPTION
0.913 (300.007)
fibo_15_true-unreach-call.c [OCRS][without] EXCEPTION
0.948 (300.01)
fibo_20_false-unreach-call.c [OCRS][without] EXCEPTION
0.976 (300.007)
fibo_20_true-unreach-call.c [OCRS][without] EXCEPTION
0.984 (300.009)
fibo_25_false-unreach-call.c [OCRS][without] EXCEPTION
0.978 (300.011)
fibo_25_true-unreach-call.c [OCRS][without] EXCEPTION
0.951 (300.004)
fibo_2calls_10_false-unreach-call.c [OCRS][without] EXCEPTION
17.427 (130.986)
fibo_2calls_10_true-unreach-call.c [OCRS][without] EXCEPTION
17.503 (132.236)
fibo_2calls_15_false-unreach-call.c [OCRS][without] EXCEPTION
17.516 (133.203)
fibo_2calls_15_true-unreach-call.c [OCRS][without] EXCEPTION
17.352 (132.365)
fibo_2calls_20_false-unreach-call.c [OCRS][without] EXCEPTION
17.395 (132.041)
fibo_2calls_20_true-unreach-call.c [OCRS][without] EXCEPTION
17.542 (132.029)
fibo_2calls_25_false-unreach-call.c [OCRS][without] EXCEPTION
17.599 (133.236)
fibo_2calls_25_true-unreach-call.c [OCRS][without] EXCEPTION
17.672 (131.876)
fibo_2calls_2_false-unreach-call.c [OCRS][without] EXCEPTION
17.552 (132.704)
fibo_2calls_2_true-unreach-call.c [OCRS][without] EXCEPTION
17.51 (129.424)
fibo_2calls_4_false-unreach-call.c [OCRS][without] EXCEPTION
17.495 (129.732)
fibo_2calls_4_true-unreach-call.c [OCRS][without] EXCEPTION
17.619 (132.81)
fibo_2calls_5_false-unreach-call.c [OCRS][without] EXCEPTION
17.424 (132.273)
fibo_2calls_5_true-unreach-call.c [OCRS][without] EXCEPTION
17.34 (129.816)
fibo_2calls_6_false-unreach-call.c [OCRS][without] EXCEPTION
17.444 (129.033)
fibo_2calls_6_true-unreach-call.c [OCRS][without] EXCEPTION
17.314 (130.649)
fibo_2calls_8_false-unreach-call.c [OCRS][without] EXCEPTION
17.334 (131.054)
fibo_2calls_8_true-unreach-call.c [OCRS][without] EXCEPTION
17.297 (128.719)
fibo_5_false-unreach-call.c [OCRS][without] EXCEPTION
0.96 (300.01)
fibo_5_true-unreach-call.c [OCRS][without] EXCEPTION
0.956 (300.008)
fibo_7_false-unreach-call.c [OCRS][without] EXCEPTION
0.945 (300.01)
fibo_7_true-unreach-call.c [OCRS][without] EXCEPTION
0.936 (300.011)
id2_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.98
id2_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
1.01
id2_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.94
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.428
id2_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.417
id_b2_o3_true-unreach-call.c [OCRS][without] 2 PASS
0.574
id_b3_o2_false-unreach-call.c [OCRS][without] 2 PASS
0.574
id_b3_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.57
id_b5_o10_true-unreach-call.c [OCRS][without] 2 PASS
0.584
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.358
id_i15_o15_false-unreach-call.c [OCRS][without] 2 PASS
0.37
id_i15_o15_true-unreach-call.c [OCRS][without] 2 PASS
0.371
id_i20_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.399
id_i20_o20_true-unreach-call.c [OCRS][without] 2 PASS
0.376
id_i25_o25_false-unreach-call.c [OCRS][without] 2 PASS
0.377
id_i25_o25_true-unreach-call.c [OCRS][without] 2 PASS
0.373
id_i5_o5_false-unreach-call.c [OCRS][without] 2 PASS
0.373
id_i5_o5_true-unreach-call.c [OCRS][without] 2 PASS
0.358
id_o1000_false-unreach-call.c [OCRS][without] 2 PASS
0.364
id_o100_false-unreach-call.c [OCRS][without] 2 PASS
0.374
id_o10_false-unreach-call.c [OCRS][without] 2 PASS
0.373
id_o200_false-unreach-call.c [OCRS][without] 2 PASS
0.373
id_o20_false-unreach-call.c [OCRS][without] 2 PASS
0.375
id_o3_false-unreach-call.c [OCRS][without] 2 PASS
0.378
sum_10x0_false-unreach-call.c [OCRS][without] 2 PASS
0.386
sum_10x0_true-unreach-call.c [OCRS][without] 2 PASS
0.377
sum_15x0_false-unreach-call.c [OCRS][without] 2 PASS
0.407
sum_15x0_true-unreach-call.c [OCRS][without] 2 PASS
0.39
sum_20x0_false-unreach-call.c [OCRS][without] 2 PASS
0.402
sum_20x0_true-unreach-call.c [OCRS][without] 2 PASS
0.391
sum_25x0_false-unreach-call.c [OCRS][without] 2 PASS
0.399
sum_25x0_true-unreach-call.c [OCRS][without] 2 PASS
0.374
sum_2x3_false-unreach-call.c [OCRS][without] 2 PASS
0.391
sum_2x3_true-unreach-call.c [OCRS][without] 2 PASS
0.381
sum_non_eq_false-unreach-call.c [OCRS][without] 2 PASS
0.426
sum_non_eq_true-unreach-call.c [OCRS][without] 2 PASS
0.423
sum_non_false-unreach-call.c [OCRS][without] 2 PASS
0.398
sum_non_true-unreach-call.c [OCRS][without] 2 PASS
0.396
Total Below Time = 345.823 (was 5984.114)
/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.372
rec-bhmr2007_true-unreach-call.c [OCRS][without] 2 PASS
0.407
rec-cggmp2005b_true-unreach-call.c [OCRS][without] 3 PASS
0.742
rec-cggmp2005_true-unreach-call.c [OCRS][without] 2 PASS
0.338
rec-cggmp2005_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.354
rec-css2003_true-unreach-call.c [OCRS][without] 2 PASS
0.659
rec-ddlm2013_true-unreach-call.c [OCRS][without] EXCEPTION
0.351 (0.439)
rec-gcnr2008_false-unreach-call.c [OCRS][without] 2 PASS
0.869
rec-gj2007b_true-unreach-call.c [OCRS][without] 2 FAIL
FAIL
0.39
rec-gj2007_true-unreach-call.c [OCRS][without] 2 FAIL
0.377
rec-gr2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.374
rec-gsv2008_true-unreach-call.c [OCRS][without] 2 PASS
0.344
rec-hhk2008_true-unreach-call.c [OCRS][without] 2 PASS
0.359
rec-jm2006_true-unreach-call.c [OCRS][without] 2 PASS
0.349
rec-jm2006_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.387
rec-mcmillan2006_true-unreach-call.c [OCRS][without] 2 FAIL
0.411
Total Below Time = 7.083 (was 7.141)
/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.336
rec-count_by_1_variant_true-unreach-call.c [OCRS][without] 2 PASS
0.336
rec-count_by_2_true-unreach-call.c [OCRS][without] 2 PASS
0.33
rec-count_by_k_true-unreach-call.c [OCRS][without] 2 PASS
0.363
rec-count_by_nondet_true-unreach-call.c [OCRS][without] 2 FAIL
0.387
rec-gauss_sum_true-unreach-call.c [OCRS][without] 2 PASS
0.351
rec-half_true-unreach-call.c [OCRS][without] EXCEPTION
0.334 (0.394)
rec-nested_true-unreach-call.c [OCRS][without] 3 PASS
0.596
Total Below Time = 3.033 (was 3.121)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c [OCRS][without] 2 PASS
0.519
edit_distance_bottom_up.c [OCRS][without] 3 TIMEOUT
300.006
edit_distance_top_down.c [OCRS][without] 3 FAIL
50.732
log_log_n_solution.c [OCRS][without] 3 FAIL
0.428 (0.845)
log_n_solution.c [OCRS][without] 2 FAIL
0.462
multivariate_1.c [OCRS][without] TIMEOUT
300.008
multivariate_higher_order.c [OCRS][without] 7 FAIL
FAIL
FAIL
26.524
n_cubed_solution.c [OCRS][without] EXCEPTION
0.342
n_log_n_solution.c [OCRS][without] TIMEOUT
300.028 (1.832)
n_squared_two_base_case_even.c [OCRS][without] 2 PASS
0.379
n_squared_two_base_case_odd.c [OCRS][without] 2 PASS
0.39
pascals_dynamic.c [OCRS][without] 3 FAIL
20.036
pascals_iterative.c [OCRS][without] 1 FAIL
5.43 (6.146)
pascals_recursive.c [OCRS][without] TIMEOUT
300.005
squared_solution.c [OCRS][without] TIMEOUT
300.138 (10.459)
two_n_even.c [OCRS][without] 2 PASS
0.381
two_n_odd.c [OCRS][without] 2 PASS
0.383
two_to_n_over_two_even.c [OCRS][without] TIMEOUT
300.033 (44.919)
two_to_n_over_two_odd.c [OCRS][without] TIMEOUT
300.024 (44.654)
two_to_n_squared.c [OCRS][without] 5 FAIL
206.495 (133.851)
two_to_two_to_n.c [OCRS][without] 7 FAIL
1.678 (1.525)
Total Below Time = 2414.421 (was 1242.478)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c [OCRS][without] 1 PASS
0.308
exp_add_loop_rec.c [OCRS][without] 1 FAIL
0.365
exp_add_loop_variable.c [OCRS][without] 1 PASS
0.346
exp_with_linear_inner_loop.c [OCRS][without] 1 FAIL
0.415
linear_two_to_n.c [OCRS][without] 8 FAIL
1.574 (1.335)
loop_five_to_n.c [OCRS][without] 1 FAIL
0.35
non_loop_five_to_n.c [OCRS][without] 8 FAIL
10.24 (8.664)
power_log.c [OCRS][without] 1 PASS
0.418 (0.376)
power_log_modified.c [OCRS][without] 1 PASS
0.48 (0.387)
simple_exponential.c [OCRS][without] 1 PASS
0.346
simple_exponential_for.c [OCRS][without] 1 PASS
0.358
two_to_n_minus_n.c [OCRS][without] 8 FAIL
1.824
two_to_n_minus_n_loop.c [OCRS][without] 8 FAIL
2.752
Total Below Time = 19.776 (was 17.482)

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