[Version Information]
WALi-OpenNWA version: 52ce149de0398413fe56a8827baa93cb90d37366 (2018-05-16 18:55:10 -0500) "Adding assert(0) in case too many DuetRels are used"
duet version: 3d958d342ff1d3e92f995deff3282ad60c6544e0 (2018-06-20 12:31:36 -0400) "Merge pull request #9 from aeflores/Newton-ark2"
# Installed packages for 4.02.3+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.8.0  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
cil                20180523  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-mpfr                 1  Virtual package relying on library MPFR installatio
conf-ntl                  1  Virtual package relying on a NTL system installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
cppo                  1.6.4  Equivalent of the C preprocessor for OCaml programs
cppo_ocamlbuild       1.6.0  ocamlbuild support for cppo, OCaml-friendly source 
jbuilder         1.0+beta20  Fast, portable and opinionated build system
menhir             20180530  LR(1) parser generator
mlgmpidl            1.2.6-1  OCaml interface to the GMP library
ntl                20180523  Number Theory Library
num                       0  The Num library for arbitrary-precision integer and
oasis                0.4.11  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind             1.8.0  A library manager for OCaml
ocamlgraph            1.8.8  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.9  Generate OCaml modules from source files
OCRS             20180427v3  Recurrence solver based on operational calculus
ounit                 2.0.8  Unit testing framework loosely based on HUnit. It i
ppx_deriving          4.1.5  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.3  Compatibility Result module
Z3                    4.7.1 (pinned)  Z3 SMT solver

Test Name Output Duet Output No. of Rounds Result Run Time (Prev.) Duet Result
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below duet 1 PASS
0.783 PASS
above 4 PASS
0.831 (0.728)
kmp.c below duet EXCEPTION
0.632
above EXCEPTION
0.641
qsort.c below duet 7 PASS
1.502 (0.876) FAIL
above 4 FAIL
2.218 (0.864)
speed_pldi09_fig1.c below duet 1 PASS
0.95 (0.787) PASS
above 4 PASS
1.045 (0.777)
speed_pldi09_fig4_2.c below duet 1 PASS
0.893 (0.806) PASS
above 4 PASS
0.954 (0.811)
speed_pldi09_fig4_4.c below duet 1 PASS
0.888 (0.727) PASS
above 4 PASS
0.988 (0.733)
speed_pldi09_fig4_5.c below duet 1 PASS
0.798 PASS
above 4 PASS
0.862 (0.754)
speed_pldi10_ex1.c below duet 1 PASS
1.879 (1.052) PASS
above 4 PASS
2.675 (1.035)
speed_pldi10_ex3.c below duet 1 PASS
0.863 (0.716) PASS
above 4 PASS
1.032 (0.683)
speed_pldi10_ex4.c below duet 1 PASS
0.903 (0.775) PASS
above 4 PASS
1.086 (0.742)
speed_popl10_fig2_1.c below duet 1 PASS
0.797 (0.682) PASS
above 4 PASS
0.912 (0.692)
speed_popl10_fig2_2.c below duet 1 FAIL
0.733 FAIL
above 4 FAIL
0.759 (0.657)
speed_popl10_nested_multiple.c below duet 1 PASS
0.906 (0.781) PASS
above 4 PASS
1.054 (0.763)
speed_popl10_nested_single.c below duet 1 FAIL
1.035 (0.92) FAIL
above 4 FAIL
1.162 (0.911)
speed_popl10_sequential_single.c below duet 1 PASS
0.89 (0.801) PASS
above 4 PASS
0.953 (0.806)
speed_popl10_simple_multiple.c below duet 1 PASS
0.883 (0.775) PASS
above 4 PASS
0.982 (0.743)
speed_popl10_simple_single_2.c below duet 1 PASS
1.016 (0.851) PASS
above 4 PASS
1.18 (0.839)
speed_popl10_simple_single.c below duet 1 PASS
0.768 PASS
above 4 PASS
0.809 (0.706)
t07.c below duet 1 PASS
0.87 (0.728) PASS
above 4 PASS
0.93 (0.706)
t08.c below duet 1 PASS
0.802 (0.724) PASS
above 4 PASS
0.892 (0.705)
t09.c below duet 1 PASS
0.837 PASS
above 4 PASS
0.886 (0.75)
t10.c below duet 1 PASS
0.708 PASS
above 4 PASS
0.737 (0.65)
t11.c below duet 1 PASS
0.793 (0.689) PASS
above 4 PASS
0.923 (0.679)
t13.c below duet 1 FAIL
0.829 (0.7) FAIL
above 4 FAIL
0.927 (0.714)
t15.c below duet 1 PASS
0.783 (0.688) PASS
above 4 PASS
0.905 (0.689)
t16.c below duet 1 PASS
0.897 (0.812) PASS
above 4 PASS
0.979 (0.799)
t19.c below duet 1 PASS
0.766 (0.679) PASS
above 4 PASS
0.841 (0.694)
t20.c below duet 1 PASS
0.777 (0.696) PASS
above 4 PASS
0.818 (0.665)
t27.c below duet 1 PASS
0.853 (0.677) PASS
above 4 PASS
0.997 (0.7)
t28.c below duet 1 PASS
0.867 (0.748) PASS
above 4 PASS
0.998 (0.752)
t30.c below duet 1 FAIL
0.709 FAIL
above 4 FAIL
0.756 (0.662)
t37.c below duet 2 PASS
1.032 (0.731) FAIL
above 4 PASS
1.166 (0.725)
t39.c below duet 2 PASS
0.964 (0.713) FAIL
above 4 PASS
1.068 (0.729)
t46.c below duet 1 PASS
0.82 (0.725) PASS
above 4 PASS
0.944 (0.704)
t47.c below duet 1 FAIL
0.76 (0.664) FAIL
above 4 FAIL
0.897 (0.644)
Total Below Time = 31.186 (was 26.113)
Above Time = 35.807 (was 25.852)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below duet 2 PASS
PASS
0.815 (0.658) PASS
PASS
above 4 PASS
PASS
0.923 (0.661)
qsort_full.c below duet 4 PASS
PASS
PASS
PASS
PASS
PASS
2.925 (1.929) PASS
PASS
PASS
PASS
PASS
PASS
above 4 FAIL
PASS
PASS
PASS
PASS
PASS
4.491 (1.916)
rec1-param_safe.c below duet 2 PASS
PASS
PASS
0.778 (0.65) PASS
FAIL
PASS
above 4 PASS
PASS
PASS
0.863 (0.65)
rec1-param_unsafe.c below duet 2 OKAY
0.75 (0.633) PASS
above 4 OKAY
0.826 (0.631)
rec1_safe.c below duet 2 PASS
PASS
PASS
0.782 (0.652) PASS
FAIL
PASS
above 4 PASS
PASS
PASS
0.822 (0.639)
rec1_unsafe.c below duet 2 OKAY
0.732 (0.641) PASS
above 4 OKAY
0.79 (0.643)
rec2-param_safe.c below duet 2 PASS
PASS
PASS
0.789 (0.652) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.871 (0.666)
rec2-param_unsafe.c below duet 2 OKAY
0.737 (0.659) PASS
above 4 OKAY
0.791 (0.643)
rec2_safe.c below duet 2 PASS
PASS
PASS
0.8 (0.656) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.83 (0.637)
rec2_unsafe.c below duet 2 OKAY
0.757 (0.648) PASS
above 4 OKAY
0.769 (0.633)
rec-test.c below duet 2 PASS
0.742 (0.643) FAIL
above 4 PASS
0.801 (0.622)
sas03_bothbranches.c below duet 7 PASS
1.086 (0.662) PASS
above 4 FAIL
1.228 (0.637)
sas03.c below duet 2 PASS
1.107 (0.681) PASS
above 4 PASS
1.268 (0.671)
simulated_lese_recursive.c below duet 2 PASS
0.777 (0.625) PASS
above 4 PASS
0.841 (0.614)
Total Below Time = 13.577 (was 10.389)
Above Time = 16.114 (was 10.263)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below duet 1 PASS
0.481 (0.415) PASS
above 4 PASS
0.503 (0.422)
count_up_down_unsafe.c below duet 1 OKAY
0.477 (0.426) PASS
above 4 OKAY
0.511 (0.431)
divide.c below duet 1 PASS
0.517 (0.461) PASS
above 4 PASS
0.569 (0.444)
factor_unsafe.c below duet 1 OKAY
0.494 (0.438) PASS
above 4 OKAY
0.523 (0.453)
for_infinite_loop_1_safe.c below duet 1 PASS
0.436 (0.38) PASS
above 0 PASS
0.477 (0.381)
for_infinite_loop_2_safe.c below duet 1 PASS
0.418 PASS
above 0 PASS
0.461 (0.384)
interproc.c below duet 1 PASS
0.621 PASS
above 4 PASS
0.632
mult.c below duet 1 PASS
PASS
0.504 (0.456) PASS
PASS
above 4 PASS
PASS
0.548 (0.424)
pointer_arith.c below duet 1 PASS
PASS
PASS
PASS
0.404 (0.338) PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
0.378 (0.338)
quotient.c below duet 3 PASS
0.896 (0.697) PASS
above 4 PASS
1.047 (0.704)
subtract.c below duet 1 PASS
0.39 (0.343) PASS
above 4 PASS
0.443 (0.344)
sum01_bug02_sum01_bug02_base.case_unsafe.c below duet 1 OKAY
0.529 (0.48) PASS
above 4 OKAY
0.58 (0.471)
sum01_bug02_unsafe.c below duet 1 OKAY
0.672 (0.534) PASS
above 4 OKAY
0.737 (0.531)
sum01_real_safe.c below duet 1 PASS
0.505 (0.453) PASS
above 4 PASS
0.552 (0.44)
sum01_safe.c below duet 1 PASS
0.487 PASS
above 4 PASS
0.521 (0.437)
sum01_unsafe.c below duet 1 OKAY
0.628 (0.513) PASS
above 4 OKAY
0.703 (0.522)
sum02_safe.c below duet 1 PASS
0.476 PASS
above 4 PASS
0.542 (0.436)
sum03_safe.c below duet 1 PASS
0.467 (0.411) PASS
above 0 PASS
0.5 (0.407)
sum03_unsafe.c below duet 1 OKAY
0.628 (0.507) PASS
above 0 OKAY
0.73 (0.495)
sum04_safe.c below duet 1 PASS
0.531 (0.456) PASS
above 4 PASS
0.568 (0.468)
sum04_unsafe.c below duet 1 OKAY
0.622 (0.522) PASS
above 4 OKAY
0.691 (0.51)
terminator_02_safe.c below duet 1 PASS
0.394 PASS
above 4 PASS
0.434 (0.387)
terminator_02_unsafe.c below duet 1 OKAY
0.423 (0.369) PASS
above 4 OKAY
0.468 (0.367)
terminator_03_safe.c below duet 1 PASS
0.418 PASS
above 4 PASS
0.471 (0.371)
terminator_03_unsafe.c below duet 1 OKAY
0.433 (0.365) PASS
above 4 OKAY
0.461 (0.388)
token_ring01_safe.c below duet 4 FAIL
36.877 (1.449) FAIL
above 4 FAIL
94.343 (1.437)
token_ring01_unsafe.c below duet 4 OKAY
51.585 (2.445) PASS
above 4 OKAY
207.962 (2.419)
toy_safe.c below duet TIMEOUT
300.035 (5.981) FAIL
above TIMEOUT
300.034 (5.927)
trex01_safe.c below duet 1 PASS
1.048 (0.947) PASS
above 4 PASS
1.133 (0.96)
trex01_unsafe.c below duet 1 OKAY
1.073 (0.927) PASS
above 4 OKAY
1.088 (0.939)
trex02_safe2.c below duet 3 PASS
0.872 (0.714) PASS
above 4 PASS
0.991 (0.71)
trex02_safe.c below duet 3 PASS
0.785 (0.673) PASS
above 4 PASS
0.889 (0.665)
trex02_unsafe.c below duet 3 OKAY
0.787 (0.667) PASS
above 4 OKAY
0.879 (0.657)
trex03_safe.c below duet 1 PASS
0.526 (0.429) PASS
above 4 PASS
0.614 (0.433)
trex03_unsafe.c below duet 1 OKAY
0.511 (0.434) PASS
above 4 OKAY
0.59 (0.413)
trex04_safe.c below duet 1 PASS
0.776 (0.698) PASS
above 4 PASS
0.808 (0.706)
while_infinite_loop_1_safe.c below duet 1 PASS
0.374 (0.327) PASS
above 0 PASS
0.399 (0.326)
while_infinite_loop_2_safe.c below duet 1 PASS
0.388 (0.317) PASS
above 0 PASS
0.4 (0.335)
while_infinite_loop_3_safe.c below duet 1 PASS
0.666 PASS
above 4 PASS
0.656
Total Below Time = 409.154 (was 27.842)
Above Time = 624.836 (was 27.724)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below duet 3 PASS
0.831 (0.637) PASS
above 4 FAIL
0.891 (0.624)
blogger_simplified1.c below duet 3 PASS
1.706 (1.269) PASS
above 4 PASS
2.39 (1.274)
divided_difference2.c below duet EXCEPTION
0.92
above 4 PASS
PASS
PASS
4.292 (3.233)
mult-proc.c below duet 3 PASS
PASS
0.81 (0.686) PASS
PASS
above 4 PASS
PASS
0.904 (0.71)
mult-proc-params.c below duet 3 PASS
PASS
0.855 (0.694) PASS
PASS
above 4 PASS
PASS
0.99 (0.696)
popall.c below duet 1 PASS
PASS
PASS
PASS
PASS
0.886 (0.666) PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
1.024 (0.642)
simulated_scc.c below duet 1 PASS
PASS
1.134 (0.919) PASS
PASS
above 4 PASS
PASS
1.294 (0.898)
Total Below Time = 7.142 (was 5.804)
Above Time = 11.785 (was 8.077)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below duet 1 PASS
0.808 PASS
above 4 PASS
0.858 (0.75)
degree2_binomial.c below duet 1 PASS
1.272 (1.081) PASS
above 4 PASS
1.424 (1.049)
degree2_monomial.c below duet 1 PASS
1.128 (0.99) PASS
above 4 PASS
1.195 (0.988)
degree3_binomial.c below duet 1 PASS
2.332 (1.702) PASS
above 4 PASS
2.905 (1.719)
degree3_monomial.c below duet 1 PASS
1.633 (1.429) PASS
above 4 PASS
1.75 (1.426)
degree4_binomial.c below duet 1 PASS
4.365 (2.94) PASS
above 4 PASS
5.983 (2.953)
degree4_monomial.c below duet 1 PASS
2.387 (2.103) PASS
above 4 PASS
2.655 (2.047)
degree5_binomial.c below duet 1 PASS
11.792 (5.202) PASS
above 4 PASS
19.196 (5.197)
degree5_monomial.c below duet 1 PASS
3.541 (2.994) PASS
above 4 PASS
3.996 (3.027)
Total Below Time = 29.258 (was 19.207)
Above Time = 39.962 (was 19.156)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below duet 1 PASS
0.527 (0.46) PASS
above 4 PASS
0.596 (0.455)
cubic_with_square_interproc.c below duet 2 PASS
0.854 (0.64) FAIL
above 4 PASS
0.914 (0.631)
cubic_with_square_nonlinear.c below duet 1 PASS
0.55 (0.471) PASS
above 4 PASS
0.571 (0.466)
cubic_with_square_nonlinear_interproc.c below duet 2 PASS
0.779 (0.652) FAIL
above 4 PASS
0.863 (0.63)
cubic_with_square_nonlinear_unsafe.c below duet 1 OKAY
0.533 (0.478) PASS
above 4 OKAY
0.608 (0.484)
cubic_with_square_unsafe.c below duet 1 OKAY
0.555 (0.476) PASS
above 4 OKAY
0.611 (0.45)
multi-input.c below duet 1 PASS
0.7 (0.481) PASS
above 4 PASS
0.869 (0.478)
multi-input_unsafe.c below duet 1 OKAY
0.75 (0.49) PASS
above 4 OKAY
0.917 (0.482)
nondet_loop_bound.c below duet 1 PASS
0.518 (0.452) PASS
above 4 PASS
0.56 (0.467)
nondet_loop_bound_quartic.c below duet 1 PASS
0.521 (0.455) PASS
above 4 PASS
0.569 (0.451)
nondet_loop_bound_quartic_unsafe.c below duet 1 OKAY
0.549 (0.458) PASS
above 4 OKAY
0.59 (0.448)
nondet_loop_bound_unsafe.c below duet 1 OKAY
0.527 (0.455) PASS
above 4 OKAY
0.554 (0.441)
nonlinear_stratified.c below duet 1 PASS
190.45 (0.75) PASS
above 4 PASS
189.957 (0.73)
nonlinear_stratified_unsafe.c below duet 1 TIMEOUT
300.004 (0.734) TIMEOUT
above 4 TIMEOUT
300.005 (0.776)
quartic_with_cube.c below duet 1 PASS
0.597 (0.483) PASS
above 4 PASS
0.668 (0.483)
quartic_with_cube_nonlinear.c below duet 1 PASS
0.571 (0.484) PASS
above 4 PASS
0.637 (0.461)
quartic_with_cube_nonlinear_unsafe.c below duet 1 OKAY
0.58 (0.454) PASS
above 4 OKAY
0.672 (0.463)
quartic_with_cube_unsafe.c below duet 1 OKAY
0.507 (0.46) PASS
above 4 OKAY
0.555 (0.45)
quintic_with_quartic.c below duet 1 PASS
0.678 (0.459) PASS
above 4 PASS
0.847 (0.445)
quintic_with_quartic_nonlinear.c below duet 1 PASS
0.731 (0.522) PASS
above 4 PASS
0.859 (0.516)
quintic_with_quartic_nonlinear_unsafe.c below duet 1 OKAY
0.763 (0.551) PASS
above 4 OKAY
0.899 (0.503)
quintic_with_quartic_unsafe.c below duet 1 OKAY
0.691 (0.461) PASS
above 4 OKAY
0.823 (0.467)
Total Below Time = 502.935 (was 11.326)
Above Time = 504.144 (was 11.177)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below duet 1 PASS
1.427 (0.708) PASS
above 4 PASS
1.988 (0.687)
degree2_FD_AllAux_AllAssm.c below duet 1 PASS
5.198 (1.476) PASS
above 4 PASS
9.158 (1.409)
degree2_FD_AllAux_FewAssm.c below duet 1 PASS
4.931 (1.395) PASS
above 4 PASS
8.605 (1.357)
degree2_FD_FewAux_FewAssm.c below duet 1 PASS
1.908 (0.735) PASS
above 4 PASS
2.977 (0.718)
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below duet 1 PASS
1.895 (0.732) PASS
above 4 PASS
2.964 (0.709)
degree3.c below duet 1 PASS
1.611 (0.711) PASS
above 4 PASS
2.54 (0.68)
degree3_FD.c below duet 1 PASS
1.875 (0.788) PASS
above 4 PASS
3.044 (0.805)
degree4.c below duet 1 PASS
1.384 (1.152) PASS
above 4 PASS
1.531 (1.133)
Total Below Time = 20.229 (was 7.697)
Above Time = 32.807 (was 7.498)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below duet EXCEPTION
0.317
above EXCEPTION
0.324
loop_unsafe.c below duet EXCEPTION
0.32
above EXCEPTION
0.32
simulated_lese_parser.c below duet 1 PASS
0.804 PASS
above 4 PASS
0.842 (0.74)
simulated_lese_sentinel.c below duet 1 PASS
0.805 PASS
above 4 PASS
0.815
Total Below Time = 2.246 (was 2.123)
Above Time = 2.301 (was 2.116)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below duet 1 PASS
PASS
PASS
0.605 (0.502) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.627 (0.506)
Total Below Time = 0.605 (was 0.502)
Above Time = 0.627 (was 0.506)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below duet TIMEOUT
300.013 (2.871) TIMEOUT
above TIMEOUT
300.014 (2.786)
Total Below Time = 300.013 (was 2.871)
Above Time = 300.014 (was 2.786)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below duet 1 OKAY
0.553 (0.461) PASS
above 4 OKAY
0.572 (0.455)
array_false-unreach-call2.c below duet 1 OKAY
0.533 (0.467) PASS
above 4 OKAY
0.557 (0.457)
array_false-unreach-call3.c below duet 1 OKAY
0.605 PASS
above 4 OKAY
0.66 (0.553)
array_true-unreach-call1.c below duet 1 FAIL
0.511 (0.454) FAIL
above 4 FAIL
0.542 (0.45)
array_true-unreach-call2.c below duet 1 FAIL
0.515 FAIL
above 4 FAIL
0.55 (0.465)
array_true-unreach-call3.c below duet 1 PASS
0.547 PASS
above 4 PASS
0.569 (0.51)
array_true-unreach-call4.c below duet 1 FAIL
0.501 FAIL
above 4 FAIL
0.562 (0.47)
const_false-unreach-call1.c below duet 1 OKAY
0.498 (0.441) PASS
above 4 OKAY
0.512 (0.445)
const_true-unreach-call1.c below duet 1 PASS
0.472 PASS
above 4 PASS
0.535 (0.45)
diamond_false-unreach-call1.c below duet 1 OKAY
0.525 (0.469) PASS
above 4 OKAY
0.597 (0.476)
diamond_true-unreach-call1.c below duet 1 PASS
0.532 (0.481) PASS
above 4 PASS
0.561 (0.466)
diamond_true-unreach-call2.c below duet 1 PASS
0.557 (0.462) PASS
above 4 PASS
0.598 (0.493)
functions_false-unreach-call1.c below duet 3 OKAY
0.799 (0.686) PASS
above 4 OKAY
0.898 (0.68)
functions_true-unreach-call1.c below duet 3 PASS
0.806 (0.673) PASS
above 4 PASS
0.936 (0.685)
multivar_false-unreach-call1.c below duet 1 OKAY
0.389 (0.352) PASS
above 4 OKAY
0.43 (0.354)
multivar_true-unreach-call1.c below duet 1 PASS
0.411 (0.356) PASS
above 4 PASS
0.434 (0.369)
nested_false-unreach-call1.c below duet 1 OKAY
0.803 PASS
above 4 OKAY
0.883 (0.722)
nested_true-unreach-call1.c below duet 1 PASS
0.825 (0.739) PASS
above 4 PASS
0.897 (0.747)
overflow_true-unreach-call1.c below duet 1 PASS
0.451 (0.399) PASS
above 4 PASS
0.482 (0.39)
phases_false-unreach-call1.c below duet 1 OKAY
0.62 (0.497) PASS
above 4 OKAY
0.664 (0.488)
phases_false-unreach-call2.c below duet 1 OKAY
0.578 (0.489) PASS
above 4 OKAY
0.636 (0.482)
phases_true-unreach-call1.c below duet 1 PASS
0.589 (0.496) PASS
above 4 PASS
0.646 (0.504)
phases_true-unreach-call2.c below duet 1 FAIL
0.59 (0.489) FAIL
above 4 FAIL
0.656 (0.493)
simple_false-unreach-call1.c below duet 1 OKAY
0.481 PASS
above 4 OKAY
0.53 (0.448)
simple_false-unreach-call2.c below duet 1 OKAY
0.394 (0.35) PASS
above 4 OKAY
0.429 (0.345)
simple_false-unreach-call3.c below duet 1 OKAY
0.452 PASS
above 4 OKAY
0.506 (0.407)
simple_false-unreach-call4.c below duet 1 OKAY
0.481 PASS
above 4 OKAY
0.562 (0.446)
simple_true-unreach-call1.c below duet 1 PASS
0.497 (0.445) PASS
above 4 PASS
0.507 (0.45)
simple_true-unreach-call2.c below duet 1 PASS
0.389 (0.353) PASS
above 4 PASS
0.417 (0.336)
simple_true-unreach-call3.c below duet 1 PASS
0.489 (0.421) PASS
above 4 PASS
0.505 (0.434)
simple_true-unreach-call4.c below duet 1 PASS
0.478 (0.433) PASS
above 4 PASS
0.51 (0.433)
underapprox_false-unreach-call1.c below duet 1 OKAY
0.514 (0.456) PASS
above 4 OKAY
0.552 (0.45)
underapprox_false-unreach-call2.c below duet 1 OKAY
0.506 (0.441) PASS
above 4 OKAY
0.511 (0.449)
underapprox_true-unreach-call1.c below duet 1 PASS
0.509 PASS
above 4 PASS
0.563 (0.452)
underapprox_true-unreach-call2.c below duet 1 PASS
0.514 (0.436) PASS
above 4 PASS
0.554 (0.445)
Total Below Time = 18.914 (was 16.755)
Above Time = 20.523 (was 16.699)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below duet 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
2.614 (2.235) PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
2.877 (2.256)
apache-get-tag_true-unreach-call.c below duet 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
1.183 (0.849) PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
1.302 (0.855)
down_true-unreach-call.c below duet 1 PASS
0.557 (0.477) PASS
above 4 PASS
0.591 (0.457)
fragtest_simple_true-unreach-call.c below duet 1 PASS
0.989 (0.889) PASS
above 4 PASS
1.126 (0.847)
half_2_true-unreach-call.c below duet 1 PASS
0.705 (0.598) PASS
above 4 PASS
0.78 (0.609)
heapsort_true-unreach-call.c below duet 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
5.905 (1.067) PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
10.387 (1.054)
id_build_true-unreach-call.c below duet 1 PASS
PASS
0.974 (0.851) PASS
PASS
above 4 PASS
PASS
1.009 (0.859)
id_trans_false-unreach-call.c below duet 1 OKAY
0.635 (0.549) PASS
above 4 OKAY
0.704 (0.547)
id_trans_true-unreach-call.c below duet 1 PASS
PASS
PASS
0.707 (0.61) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.732 (0.621)
large_const_true-unreach-call.c below duet 1 PASS
0.658 (0.571) PASS
above 4 PASS
0.742 (0.55)
MADWiFi-encode_ie_ok_true-unreach-call.c below duet 1 PASS
PASS
0.842 PASS
PASS
above 4 PASS
PASS
0.89 (0.742)
nested6_true-unreach-call.c below duet 1 PASS
PASS
PASS
2.025 (1.821) PASS
PASS
PASS
above 4 PASS
PASS
PASS
2.23 (1.827)
nested9_true-unreach-call.c below duet 1 PASS
3.256 PASS
above 4 PASS
3.543 (2.953)
nest-if3_true-unreach-call.c below duet 1 PASS
0.836 (0.719) PASS
above 4 PASS
0.954 (0.725)
NetBSD_loop_true-unreach-call.c below duet 1 PASS
PASS
0.634 (0.549) PASS
PASS
above 4 PASS
PASS
0.68 (0.548)
sendmail-close-angle_true-unreach-call.c below duet 1 PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
1.046 (0.809) PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
above 4 PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
1.094 (0.836)
seq_true-unreach-call.c below duet 1 PASS
1.01 (0.838) PASS
above 4 PASS
1.093 (0.858)
SpamAssassin-loop_true-unreach-call.c below duet 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
5.854 (2.074) PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
9.116 (2.048)
string_concat-noarr_true-unreach-call.c below duet 1 PASS
1.094 PASS
above 4 PASS
1.182 (0.99)
up_true-unreach-call.c below duet 1 PASS
0.665 (0.567) PASS
above 4 PASS
0.731 (0.559)
Total Below Time = 32.189 (was 20.822)
Above Time = 41.763 (was 20.741)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below duet 1 PASS
0.601 (0.521) PASS
above 4 PASS
0.629 (0.528)
bhmr2007_true-unreach-call.c below duet 1 PASS
0.547 (0.464) PASS
above 4 PASS
0.602 (0.479)
cggmp2005b_true-unreach-call.c below duet 1 PASS
1.074 PASS
above 4 PASS
1.23 (0.946)
cggmp2005_true-unreach-call.c below duet 1 PASS
0.518 (0.444) PASS
above 4 PASS
0.524 (0.465)
cggmp2005_variant_true-unreach-call.c below duet 1 PASS
0.491 PASS
above 4 PASS
0.553 (0.433)
css2003_true-unreach-call.c below duet 1 PASS
0.644 PASS
above 4 PASS
0.699 (0.583)
ddlm2013_true-unreach-call.c below duet 1 PASS
0.629 (0.517) PASS
above 4 PASS
0.724 (0.516)
gcnr2008_false-unreach-call.c below duet 1 OKAY
1.051 (0.762) PASS
above 4 OKAY
1.275 (0.746)
gj2007b_true-unreach-call.c below duet 1 PASS
FAIL
0.539 (0.453) PASS
FAIL
above 4 PASS
FAIL
0.564 (0.449)
gj2007_true-unreach-call.c below duet 1 PASS
0.608 (0.477) PASS
above 4 PASS
0.69 (0.493)
gr2006_true-unreach-call.c below duet 1 PASS
0.591 (0.497) PASS
above 4 PASS
0.668 (0.483)
gsv2008_true-unreach-call.c below duet 1 PASS
0.506 (0.437) PASS
above 4 PASS
0.546 (0.443)
hhk2008_true-unreach-call.c below duet 1 PASS
0.514 (0.46) PASS
above 4 PASS
0.544 (0.466)
jm2006_true-unreach-call.c below duet 1 PASS
0.514 PASS
above 4 PASS
0.56 (0.465)
jm2006_variant_true-unreach-call.c below duet 1 PASS
0.553 PASS
above 4 PASS
0.601 (0.494)
mcmillan2006_true-unreach-call.c below duet 1 FAIL
0.714 (0.629) FAIL
above 4 FAIL
0.795 (0.611)
Total Below Time = 10.094 (was 8.661)
Above Time = 11.204 (was 8.6)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below duet 1 PASS
0.503 (0.425) PASS
above 4 PASS
0.528 (0.433)
count_by_1_variant_true-unreach-call.c below duet 1 PASS
0.531 (0.477) PASS
above 4 PASS
0.558 (0.472)
count_by_2_true-unreach-call.c below duet 1 PASS
0.494 (0.427) PASS
above 4 PASS
0.537 (0.441)
count_by_k_true-unreach-call.c below duet 1 PASS
0.503 (0.424) PASS
above 4 PASS
0.539 (0.425)
count_by_nondet_true-unreach-call.c below duet 1 FAIL
0.541 (0.481) FAIL
above 4 FAIL
0.562 (0.482)
gauss_sum_true-unreach-call.c below duet 1 PASS
0.51 (0.449) PASS
above 4 PASS
0.551 (0.436)
half_true-unreach-call.c below duet 1 FAIL
0.533 FAIL
above 4 FAIL
0.597 (0.455)
nested_true-unreach-call.c below duet 1 PASS
1.025 (0.9) PASS
above 4 PASS
1.094 (0.925)
Total Below Time = 4.64 (was 4.077)
Above Time = 4.966 (was 4.069)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below duet 1 OKAY
0.473 (0.405) PASS
above 4 OKAY
0.507 (0.419)
array_true-unreach-call.c below duet 1 FAIL
0.455 FAIL
above 4 FAIL
0.486 (0.398)
bubble_sort_false-unreach-call.c below duet 4 OKAY
UNSOUND
3.73 (2.068) PASS
FAIL
above 4 OKAY
UNSOUND
15.801 (1.988)
bubble_sort_true-unreach-call.c below duet 1 2.177
above 4 2.4 (1.98)
compact_false-unreach-call.c below duet EXCEPTION
0.353
above EXCEPTION
0.323
count_up_down_false-unreach-call_true-termination.c below duet 1 OKAY
0.483 (0.413) PASS
above 4 OKAY
0.509 (0.406)
count_up_down_true-unreach-call_true-termination.c below duet 1 PASS
0.479 (0.417) PASS
above 4 PASS
0.52 (0.42)
eureka_01_false-unreach-call.c below duet EXCEPTION
0.331
above EXCEPTION
0.321
eureka_01_true-unreach-call.c below duet EXCEPTION
0.376 (0.326)
above EXCEPTION
0.347
eureka_05_true-unreach-call.c below duet EXCEPTION
0.651
above EXCEPTION
0.642
for_bounded_loop1_false-unreach-call_true-termination.c below duet 1 OKAY
0.505 (0.438) PASS
above 4 OKAY
0.532 (0.447)
for_bounded_loop1_true-unreach-call_true-termination.c below duet 1 PASS
PASS
0.569 (0.498) PASS
PASS
above 4 PASS
PASS
0.591 (0.503)
for_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.43 PASS
above 0 PASS
0.453 (0.391)
for_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.433 PASS
above 0 PASS
0.46 (0.382)
heavy_false-unreach-call.c below duet 1 OKAY
1.557 (1.365) PASS
above 4 OKAY
1.645 (1.37)
heavy_true-unreach-call.c below duet 1 PASS
1.535 (1.381) PASS
above 4 PASS
1.653 (1.393)
insertion_sort_false-unreach-call.c below duet 1 OKAY
1.279 (1.023) PASS
above 4 OKAY
1.497 (0.98)
insertion_sort_true-unreach-call.c below duet 1 FAIL
1.029 FAIL
above 4 FAIL
1.163 (0.946)
invert_string_false-unreach-call.c below duet 1 OKAY
0.839 (0.695) PASS
above 4 OKAY
0.927 (0.693)
invert_string_true-unreach-call.c below duet 1 FAIL
1.017 (0.873) FAIL
above 4 FAIL
1.144 (0.879)
linear_sea.ch_true-unreach-call.c below duet 1 FAIL
0.851 FAIL
above 4 FAIL
0.904 (0.805)
linear_search_false-unreach-call.c below duet 1 OKAY
0.928 (0.823) PASS
above 4 OKAY
0.939 (0.819)
lu.cmp_true-unreach-call.c below duet 3 PASS
8.004 (6.164) PASS
above 4 PASS
10.671 (6.128)
ludcmp_false-unreach-call.c below duet 3 OKAY
7.421 (5.726) PASS
above 4 OKAY
10.077 (5.695)
matrix_false-unreach-call_true-termination.c below duet 1 OKAY
1.374 (1.165) PASS
above 4 OKAY
1.562 (1.14)
matrix_true-unreach-call_true-termination.c below duet 1 FAIL
0.591 (0.503) FAIL
above 4 FAIL
0.685 (0.515)
n.c11_true-unreach-call.c below duet EXCEPTION
0.603
above EXCEPTION
0.617
n.c24_false-unreach-call.c below duet EXCEPTION
0.627
above EXCEPTION
0.613
n.c40_true-unreach-call.c below duet EXCEPTION
0.315
above EXCEPTION
0.318
nec11_false-unreach-call.c below duet EXCEPTION
0.623
above EXCEPTION
0.615
nec20_false-unreach-call.c below duet EXCEPTION
0.6
above EXCEPTION
0.61
nec40_true-unreach-call.c below duet EXCEPTION
0.329
above EXCEPTION
0.329
string_false-unreach-call.c below duet 1 OKAY
1.47 (1.262) PASS
above 4 OKAY
1.662 (1.26)
string_true-unreach-call.c below duet 1 FAIL
1.484 (1.268) FAIL
above 4 FAIL
1.622 (1.278)
sum01_bug02_false-unreach-call_true-termination.c below duet 1 OKAY
0.633 (0.521) PASS
above 4 OKAY
0.767 (0.522)
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below duet 1 OKAY
0.55 (0.48) PASS
above 4 OKAY
0.579 (0.489)
sum01_false-unreach-call_true-termination.c below duet 1 OKAY
0.636 (0.504) PASS
above 4 OKAY
0.701 (0.526)
sum01_true-unreach-call_true-termination.c below duet 1 PASS
0.506 PASS
above 4 PASS
0.549 (0.46)
sum03_false-unreach-call_true-termination.c below duet 1 OKAY
0.588 (0.449) PASS
above 0 OKAY
0.683 (0.469)
sum03_true-unreach-call_false-termination.c below duet 1 PASS
0.556 (0.495) PASS
above 4 PASS
0.599 (0.492)
sum04_false-unreach-call_true-termination.c below duet 1 OKAY
0.606 (0.528) PASS
above 4 OKAY
0.67 (0.501)
sum04_true-unreach-call_true-termination.c below duet 1 PASS
0.51 PASS
above 4 PASS
0.551 (0.477)
sum_array_false-unreach-call.c below duet 1 OKAY
0.95 (0.801) PASS
above 4 OKAY
1.024 (0.79)
sum_array_true-unreach-call.c below duet 1 FAIL
0.957 (0.79) FAIL
above 4 FAIL
1.058 (0.814)
terminator_01_false-unreach-call_false-termination.c below duet 1 OKAY
0.398 (0.356) PASS
above 4 OKAY
0.418 (0.341)
terminator_02_false-unreach-call_true-termination.c below duet 1 OKAY
0.711 PASS
above 4 OKAY
0.704
terminator_02_true-unreach-call_true-termination.c below duet 2 PASS
0.744 (0.649) PASS
above 4 PASS
0.837 (0.662)
terminator_03_false-unreach-call_true-termination.c below duet 1 OKAY
0.428 (0.366) PASS
above 4 OKAY
0.481 (0.376)
terminator_03_true-unreach-call_true-termination.c below duet 1 PASS
0.433 (0.387) PASS
above 4 PASS
0.467 (0.369)
trex01_false-unreach-call_true-termination.c below duet 3 OKAY
1.275 (1.104) PASS
above 4 OKAY
1.498 (1.098)
trex01_true-unreach-call.c below duet 3 PASS
1.451 (1.282) PASS
above 4 PASS
1.718 (1.264)
trex02_false-unreach-call_true-termination.c below duet 3 OKAY
0.798 (0.681) PASS
above 4 OKAY
0.898 (0.655)
trex02_true-unreach-call_true-termination.c below duet 3 PASS
0.794 (0.706) PASS
above 4 PASS
0.926 (0.681)
trex03_false-unreach-call_true-termination.c below duet 3 OKAY
0.929 (0.713) PASS
above 4 OKAY
1.152 (0.712)
trex03_true-unreach-call.c below duet 3 PASS
0.936 (0.735) PASS
above 4 PASS
1.191 (0.73)
trex04_true-unreach-call_false-termination.c below duet 1 PASS
0.908 PASS
above 4 PASS
1.04 (0.87)
veris.c_NetBSD-libc__loop_true-unreach-call.c below duet 1 PASS
0.71 PASS
above 4 PASS
0.745 (0.637)
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below duet EXCEPTION
0.638
above EXCEPTION
0.637
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below duet 1 PASS
0.549 PASS
above 4 PASS
0.578 (0.49)
verisec_NetBSD-libc__loop_false-unreach-call.c below duet 1 OKAY
0.687 PASS
above 4 OKAY
0.752 (0.652)
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below duet EXCEPTION
0.614
above EXCEPTION
0.626
vogal_false-unreach-call.c below duet 1 OKAY
2.159 (1.856) PASS
above 4 OKAY
2.332 (1.851)
vogal_true-unreach-call.c below duet 1 FAIL
1.931 (1.722) FAIL
above 4 FAIL
2.141 (1.678)
while_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.371 (0.337) PASS
above 0 PASS
0.378 (0.317)
while_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.376 (0.335) PASS
above 0 PASS
0.397 (0.322)
while_infinite_loop_3_true-unreach-call_false-termination.c below duet 1 PASS
0.666 PASS
above 4 PASS
0.667
while_infinite_loop_4_false-unreach-call_true-termination.c below duet 1 OKAY
0.659 PASS
above 4 OKAY
0.646
Total Below Time = 69.578 (was 58.824)
Above Time = 91.555 (was 58.302)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below duet 7 PASS
1.431 (0.793) FAIL
above 4 FAIL
1.524 (0.792)
Ackermann02_false-unreach-call_false-termination.c below duet 7 OKAY
1.345 (0.73) PASS
above 4 OKAY
1.497 (0.722)
Ackermann03_true-unreach-call.c below duet 7 FAIL
1.416 (0.842) FAIL
above 4 FAIL
1.549 (0.807)
Ackermann04_true-unreach-call.c below duet 7 FAIL
1.469 (0.84) FAIL
above 4 FAIL
1.502 (0.787)
Addition01_true-unreach-call_true-termination.c below duet 2 PASS
1.129 (0.766) PASS
above 4 PASS
1.229 (0.761)
Addition02_false-unreach-call_false-termination.c below duet 2 OKAY
1.033 (0.706) PASS
above 4 OKAY
1.118 (0.681)
Addition03_false-no-overflow.c below duet 2 PASS
1.024 (0.735) PASS
above 4 PASS
1.129 (0.714)
Addition03_true-unreach-call.c below duet 2 PASS
1.064 (0.742) PASS
above 4 PASS
1.181 (0.69)
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below duet 2 OKAY
0.828 (0.655) PASS
above 4 OKAY
0.921 (0.638)
EvenOdd01_true-unreach-call_true-termination.c below duet 2 PASS
0.973 (0.771) FAIL
above 4 PASS
1.053 (0.745)
EvenOdd03_false-unreach-call_false-termination.c below duet 2 OKAY
0.947 (0.786) PASS
above 4 OKAY
1.024 (0.716)
Fibonacci01_true-unreach-call.c below duet 7 FAIL
1.263 (0.749) FAIL
above 4 FAIL
1.275 (0.71)
Fibonacci02_true-unreach-call_true-termination.c below duet 7 FAIL
1.238 (0.653) FAIL
above 4 FAIL
1.184 (0.683)
Fibonacci03_true-unreach-call_true-termination.c below duet 7 FAIL
1.249 (0.737) FAIL
above 4 FAIL
1.225 (0.731)
Fibonacci04_false-unreach-call_true-termination.c below duet 7 OKAY
1.232 (0.69) PASS
above 4 OKAY
1.363 (0.716)
Fibonacci05_false-unreach-call_true-termination.c below duet 7 OKAY
1.238 (0.686) PASS
above 4 OKAY
1.215 (0.705)
gcd01_true-unreach-call_true-termination.c below duet 2 PASS
1.025 (0.836) FAIL
above 4 PASS
1.113 (0.788)
gcd02_true-unreach-call.c below duet 2 FAIL
PASS
1.264 (0.901) FAIL
PASS
above 4 FAIL
PASS
1.399 (0.916)
McCarthy91_false-unreach-call_false-termination.c below duet 7 OKAY
1.094 (0.714) PASS
above 4 OKAY
1.114 (0.712)
McCarthy91_true-unreach-call.c below duet 7 PASS
1.102 (0.701) FAIL
above 4 FAIL
1.072 (0.69)
MultCommutative_true-unreach-call_true-termination.c below duet 2 FAIL
1.077 (0.81) FAIL
above 4 FAIL
1.226 (0.808)
Primes_true-unreach-call.c below duet 3 FAIL
2.116 (1.134) FAIL
above 4 FAIL
2.975 (1.134)
recHanoi01_true-unreach-call_true-termination.c below duet TIMEOUT
300.026 (0.78) FAIL
above 4 FAIL
2.203 (0.776)
recHanoi02_true-unreach-call_true-termination.c below duet 2 FAIL
0.839 (0.692) FAIL
above 4 FAIL
0.895 (0.687)
recHanoi03_true-unreach-call_true-termination.c below duet 2 FAIL
0.854 (0.692) FAIL
above 4 FAIL
0.925 (0.686)
Total Below Time = 328.276 (was 19.141)
Above Time = 32.911 (was 18.795)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below duet 1 OKAY
UNSOUND
0.846 (0.654) PASS
FAIL
above 4 OKAY
UNSOUND
0.79 (0.655)
afterrec_2calls_true-unreach-call.c below duet 1 PASS
PASS
0.797 (0.665) PASS
PASS
above 4 PASS
PASS
0.814 (0.673)
afterrec_false-unreach-call.c below duet 1 OKAY
0.67 PASS
above 4 OKAY
0.67
afterrec_true-unreach-call.c below duet 1 PASS
0.683 PASS
above 4 PASS
0.698 (0.627)
fibo_10_false-unreach-call.c below duet 7 OKAY
1.236 (0.678) PASS
above 4 OKAY
1.095 (0.664)
fibo_10_true-unreach-call.c below duet 7 FAIL
1.216 (0.672) FAIL
above 4 FAIL
1.12 (0.677)
fibo_15_false-unreach-call.c below duet 7 OKAY
1.255 (0.68) PASS
above 4 OKAY
1.149 (0.649)
fibo_15_true-unreach-call.c below duet 7 FAIL
1.225 (0.675) FAIL
above 4 FAIL
1.14 (0.652)
fibo_20_false-unreach-call.c below duet 7 OKAY
1.223 (0.678) PASS
above 4 OKAY
1.123 (0.686)
fibo_20_true-unreach-call.c below duet 7 FAIL
1.229 (0.681) FAIL
above 4 FAIL
1.131 (0.673)
fibo_25_false-unreach-call.c below duet 7 OKAY
1.224 (0.669) PASS
above 4 OKAY
1.082 (0.674)
fibo_25_true-unreach-call.c below duet 7 FAIL
1.22 (0.676) FAIL
above 4 FAIL
1.12 (0.676)
fibo_2calls_10_false-unreach-call.c below duet 8 OKAY
15.204 (0.741) PASS
above 4 OKAY
42.912 (0.769)
fibo_2calls_10_true-unreach-call.c below duet 8 FAIL
15.233 (0.763) FAIL
above 4 FAIL
43.344 (0.733)
fibo_2calls_15_false-unreach-call.c below duet 8 OKAY
15.251 (0.753) PASS
above 4 OKAY
43.284 (0.748)
fibo_2calls_15_true-unreach-call.c below duet 8 FAIL
15.061 (0.77) FAIL
above 4 FAIL
40.59 (0.734)
fibo_2calls_20_false-unreach-call.c below duet 8 OKAY
15.18 (0.756) PASS
above 4 OKAY
43.678 (0.732)
fibo_2calls_20_true-unreach-call.c below duet 8 FAIL
15.093 (0.734) FAIL
above 4 FAIL
43.185 (0.719)
fibo_2calls_25_false-unreach-call.c below duet 8 OKAY
15.269 (0.752) PASS
above 4 OKAY
42.929 (0.754)
fibo_2calls_25_true-unreach-call.c below duet 8 FAIL
15.369 (0.763) FAIL
above 4 FAIL
42.354 (0.719)
fibo_2calls_2_false-unreach-call.c below duet 8 OKAY
15.217 (0.738) PASS
above 4 OKAY
41.276 (0.734)
fibo_2calls_2_true-unreach-call.c below duet 8 FAIL
15.118 (0.755) FAIL
above 4 PASS
42.204 (0.741)
fibo_2calls_4_false-unreach-call.c below duet 8 OKAY
15.068 (0.752) PASS
above 4 OKAY
40.869 (0.72)
fibo_2calls_4_true-unreach-call.c below duet 8 FAIL
15.245 (0.748) FAIL
above 4 FAIL
43.595 (0.753)
fibo_2calls_5_false-unreach-call.c below duet 8 OKAY
15.252 (0.76) PASS
above 4 OKAY
43.23 (0.76)
fibo_2calls_5_true-unreach-call.c below duet 8 FAIL
15.207 (0.754) FAIL
above 4 FAIL
42.131 (0.755)
fibo_2calls_6_false-unreach-call.c below duet 8 OKAY
15.206 (0.729) PASS
above 4 OKAY
42.114 (0.759)
fibo_2calls_6_true-unreach-call.c below duet 8 FAIL
15.309 (0.747) FAIL
above 4 FAIL
40.738 (0.75)
fibo_2calls_8_false-unreach-call.c below duet 8 OKAY
15.249 (0.754) PASS
above 4 OKAY
42.469 (0.749)
fibo_2calls_8_true-unreach-call.c below duet 8 FAIL
15.247 (0.759) FAIL
above 4 FAIL
41.178 (0.744)
fibo_5_false-unreach-call.c below duet 7 OKAY
1.217 (0.663) PASS
above 4 OKAY
1.134 (0.657)
fibo_5_true-unreach-call.c below duet 7 FAIL
1.241 (0.69) FAIL
above 4 FAIL
1.103 (0.665)
fibo_7_false-unreach-call.c below duet 7 OKAY
1.248 (0.682) PASS
above 4 OKAY
1.108 (0.687)
fibo_7_true-unreach-call.c below duet 7 FAIL
1.205 (0.686) FAIL
above 4 FAIL
1.098 (0.649)
id2_b2_o3_true-unreach-call.c below duet 2 PASS
1.01 (0.746) FAIL
above 4 PASS
1.217 (0.732)
id2_b3_o2_false-unreach-call.c below duet 2 OKAY
1.04 (0.754) PASS
above 4 OKAY
1.167 (0.732)
id2_b3_o5_true-unreach-call.c below duet 2 PASS
0.995 (0.741) FAIL
above 4 PASS
1.213 (0.704)
id2_b5_o10_true-unreach-call.c below duet 2 PASS
1.007 (0.7) FAIL
above 4 PASS
1.226 (0.69)
id2_i5_o5_false-unreach-call.c below duet 2 OKAY
0.879 (0.709) PASS
above 4 OKAY
0.939 (0.685)
id2_i5_o5_true-unreach-call.c below duet 2 PASS
0.874 (0.69) PASS
above 4 PASS
0.952 (0.703)
id_b2_o3_true-unreach-call.c below duet 2 PASS
0.921 (0.67) FAIL
above 4 PASS
1.072 (0.669)
id_b3_o2_false-unreach-call.c below duet 2 OKAY
0.906 (0.662) PASS
above 4 OKAY
1.071 (0.633)
id_b3_o5_true-unreach-call.c below duet 2 PASS
0.932 (0.662) FAIL
above 4 PASS
1.103 (0.676)
id_b5_o10_true-unreach-call.c below duet 2 PASS
0.888 (0.638) FAIL
above 4 PASS
1.085 (0.656)
id_i10_o10_false-unreach-call.c below duet 2 OKAY
0.778 (0.654) PASS
above 4 OKAY
0.868 (0.642)
id_i10_o10_true-unreach-call.c below duet 2 PASS
0.766 (0.662) PASS
above 4 PASS
0.87 (0.644)
id_i15_o15_false-unreach-call.c below duet 2 OKAY
0.795 (0.659) PASS
above 4 OKAY
0.867 (0.653)
id_i15_o15_true-unreach-call.c below duet 2 PASS
0.791 (0.647) PASS
above 4 PASS
0.853 (0.637)
id_i20_o20_false-unreach-call.c below duet 2 OKAY
0.79 (0.669) PASS
above 4 OKAY
0.879 (0.659)
id_i20_o20_true-unreach-call.c below duet 2 PASS
0.763 (0.65) PASS
above 4 PASS
0.865 (0.647)
id_i25_o25_false-unreach-call.c below duet 2 OKAY
0.773 (0.663) PASS
above 4 OKAY
0.861 (0.632)
id_i25_o25_true-unreach-call.c below duet 2 PASS
0.779 (0.66) PASS
above 4 PASS
0.835 (0.663)
id_i5_o5_false-unreach-call.c below duet 2 OKAY
0.779 (0.647) PASS
above 4 OKAY
0.862 (0.66)
id_i5_o5_true-unreach-call.c below duet 2 PASS
0.775 (0.662) PASS
above 4 PASS
0.872 (0.653)
id_o1000_false-unreach-call.c below duet 2 OKAY
0.785 (0.632) PASS
above 4 OKAY
0.86 (0.64)
id_o100_false-unreach-call.c below duet 2 OKAY
0.777 (0.67) PASS
above 4 OKAY
0.865 (0.634)
id_o10_false-unreach-call.c below duet 2 OKAY
0.784 (0.667) PASS
above 4 OKAY
0.857 (0.664)
id_o200_false-unreach-call.c below duet 2 OKAY
0.779 (0.638) PASS
above 4 OKAY
0.875 (0.649)
id_o20_false-unreach-call.c below duet 2 OKAY
0.791 (0.64) PASS
above 4 OKAY
0.853 (0.647)
id_o3_false-unreach-call.c below duet 2 OKAY
0.789 (0.648) PASS
above 4 OKAY
0.865 (0.637)
sum_10x0_false-unreach-call.c below duet 2 OKAY
0.822 (0.649) PASS
above 4 OKAY
0.866 (0.66)
sum_10x0_true-unreach-call.c below duet 2 PASS
0.814 (0.659) PASS
above 4 PASS
0.896 (0.642)
sum_15x0_false-unreach-call.c below duet 2 OKAY
0.804 (0.651) PASS
above 4 OKAY
0.865 (0.674)
sum_15x0_true-unreach-call.c below duet 2 PASS
0.793 (0.653) PASS
above 4 PASS
0.867 (0.656)
sum_20x0_false-unreach-call.c below duet 2 OKAY
0.807 (0.665) PASS
above 4 OKAY
0.893 (0.646)
sum_20x0_true-unreach-call.c below duet 2 PASS
0.836 (0.661) PASS
above 4 PASS
0.88 (0.633)
sum_25x0_false-unreach-call.c below duet 2 OKAY
0.813 (0.654) PASS
above 4 OKAY
0.894 (0.638)
sum_25x0_true-unreach-call.c below duet 2 PASS
0.79 (0.648) PASS
above 4 PASS
0.887 (0.657)
sum_2x3_false-unreach-call.c below duet 2 OKAY
0.8 (0.661) PASS
above 4 OKAY
0.886 (0.65)
sum_2x3_true-unreach-call.c below duet 2 PASS
0.796 (0.652) PASS
above 4 PASS
0.898 (0.674)
sum_non_eq_false-unreach-call.c below duet 2 OKAY
0.829 (0.654) PASS
above 4 OKAY
0.894 (0.654)
sum_non_eq_true-unreach-call.c below duet 2 PASS
0.826 (0.672) PASS
above 4 PASS
0.894 (0.639)
sum_non_false-unreach-call.c below duet 2 OKAY
0.821 (0.655) PASS
above 4 OKAY
0.885 (0.651)
sum_non_true-unreach-call.c below duet 2 PASS
0.798 (0.657) PASS
above 4 PASS
0.882 (0.655)
Total Below Time = 324.808 (was 50.884)
Above Time = 815.694 (was 50.345)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-lit
rec-afnp2014_true-unreach-call.c below duet 2 PASS
0.815 (0.678) FAIL
above 4 PASS
0.875 (0.647)
rec-bhmr2007_true-unreach-call.c below duet 2 PASS
0.813 (0.641) FAIL
above 4 PASS
0.902 (0.625)
rec-cggmp2005b_true-unreach-call.c below duet 3 PASS
1.231 (0.711) FAIL
above 4 FAIL
1.839 (0.727)
rec-cggmp2005_true-unreach-call.c below duet 2 PASS
0.746 (0.621) FAIL
above 4 PASS
0.854 (0.634)
rec-cggmp2005_variant_true-unreach-call.c below duet 2 PASS
0.776 (0.635) FAIL
above 4 PASS
0.864 (0.657)
rec-css2003_true-unreach-call.c below duet 2 PASS
0.827 (0.643) PASS
above 4 PASS
0.907 (0.641)
rec-ddlm2013_true-unreach-call.c below duet 2 FAIL
0.869 (0.674) FAIL
above 4 FAIL
0.98 (0.67)
rec-gcnr2008_false-unreach-call.c below duet 2 OKAY
1.057 (0.713) PASS
above 4 OKAY
1.167 (0.705)
rec-gj2007b_true-unreach-call.c below duet 2 FAIL
FAIL
0.803 (0.664) FAIL
FAIL
above 4 FAIL
FAIL
0.885 (0.646)
rec-gj2007_true-unreach-call.c below duet 2 FAIL
0.805 (0.621) FAIL
above 4 FAIL
0.897 (0.623)
rec-gr2006_true-unreach-call.c below duet 2 FAIL
0.805 (0.641) FAIL
above 4 FAIL
0.887 (0.644)
rec-gsv2008_true-unreach-call.c below duet 2 PASS
0.765 (0.656) FAIL
above 4 PASS
0.838 (0.651)
rec-hhk2008_true-unreach-call.c below duet 2 PASS
0.867 (0.744) FAIL
above 4 PASS
0.916 (0.735)
rec-jm2006_true-unreach-call.c below duet 2 PASS
0.826 (0.654) PASS
above 4 PASS
0.892 (0.659)
rec-jm2006_variant_true-unreach-call.c below duet 2 PASS
0.863 (0.663) PASS
above 4 PASS
0.957 (0.671)
rec-mcmillan2006_true-unreach-call.c below duet 2 FAIL
0.963 (0.716) FAIL
above 4 FAIL
1.041 (0.716)
Total Below Time = 13.831 (was 10.675)
Above Time = 15.701 (was 10.651)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-new
rec-count_by_1_true-unreach-call.c below duet 2 PASS
0.745 (0.637) FAIL
above 4 PASS
0.816 (0.634)
rec-count_by_1_variant_true-unreach-call.c below duet 2 PASS
0.747 (0.667) PASS
above 4 PASS
0.817 (0.621)
rec-count_by_2_true-unreach-call.c below duet 2 PASS
0.734 (0.631) FAIL
above 4 PASS
0.799 (0.637)
rec-count_by_k_true-unreach-call.c below duet 2 FAIL
0.772 (0.636) FAIL
above 4 FAIL
0.86 (0.641)
rec-count_by_nondet_true-unreach-call.c below duet 2 FAIL
0.766 (0.632) FAIL
above 4 FAIL
0.824 (0.626)
rec-gauss_sum_true-unreach-call.c below duet 2 PASS
0.778 (0.652) FAIL
above 4 PASS
0.85 (0.612)
rec-half_true-unreach-call.c below duet 2 FAIL
0.808 (0.67) FAIL
above 4 FAIL
0.913 (0.632)
rec-nested_true-unreach-call.c below duet 3 PASS
1.025 (0.676) FAIL
above 4 FAIL
1.194 (0.675)
Total Below Time = 6.375 (was 5.201)
Above Time = 7.073 (was 5.078)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below duet 2 PASS
0.869 (0.643) FAIL
above 4 PASS
0.989 (0.654)
cubic_polynomial_unsafe.c below duet 2 OKAY
0.857 (0.641) PASS
above 4 OKAY
0.939 (0.65)
edit_distance_bottom_up.c below duet 3 FAIL
4.295 (2.547) FAIL
above 4 FAIL
9.817 (2.696)
edit_distance_top_down.c below duet 3 FAIL
3.76 (2.011) FAIL
above 4 FAIL
42.668 (2.223)
log_log_n_solution.c below duet 3 FAIL
0.875 (0.667) FAIL
above 4 FAIL
0.957 (0.64)
log_log_n_solution_unsafe.c below duet 3 OKAY
0.864 (0.653) PASS
above 4 OKAY
0.918 (0.654)
log_n_solution.c below duet 2 FAIL
0.79 (0.635) FAIL
above 4 FAIL
0.875 (0.613)
log_n_solution_unsafe.c below duet 2 OKAY
0.79 (0.636) PASS
above 4 OKAY
0.846 (0.649)
multivariate_1.c below duet 4 FAIL
1.325 (0.686) TIMEOUT
above 4 FAIL
1.751 (0.64)
multivariate_1_unsafe.c below duet 4 OKAY
1.317 (0.674) TIMEOUT
above 4 OKAY
1.776 (0.681)
multivariate_higher_order.c below duet 7 FAIL
FAIL
FAIL
2.224 (0.754) FAIL
FAIL
FAIL
above 4 FAIL
FAIL
FAIL
6.008 (0.77)
multivariate_higher_order_unsafe.c below duet 7 OKAY
OKAY
OKAY
2.201 (0.772) PASS
PASS
PASS
above 4 OKAY
OKAY
OKAY
5.926 (0.767)
n_cubed_solution.c below duet TIMEOUT
300.049 (0.873) FAIL
above 4 FAIL
1.646 (0.861)
n_cubed_solution_unsafe.c below duet TIMEOUT
300.043 (0.844) PASS
above 4 OKAY
1.627 (0.844)
n_log_n_solution.c below duet 5 FAIL
1.038 (0.634) FAIL
above 4 FAIL
1.196 (0.647)
n_log_n_solution_unsafe.c below duet 5 OKAY
1.024 (0.654) PASS
above 4 OKAY
1.146 (0.666)
n_squared_two_base_case_even.c below duet 2 PASS
0.848 (0.66) FAIL
above 4 PASS
0.962 (0.65)
n_squared_two_base_case_even_unsafe.c below duet 2 OKAY
0.826 (0.657) PASS
above 4 OKAY
0.961 (0.65)
n_squared_two_base_case_odd.c below duet 2 PASS
0.85 (0.643) FAIL
above 4 PASS
0.946 (0.644)
n_squared_two_base_case_odd_unsafe.c below duet 2 OKAY
0.826 (0.648) PASS
above 4 OKAY
0.998 (0.655)
pascals_dynamic.c below duet 3 FAIL
1.562 (1.229) FAIL
above 4 FAIL
2.441 (1.227)
pascals_dynamic_unsafe.c below duet 3 OKAY
1.572 (1.209) PASS
above 4 OKAY
2.467 (1.227)
pascals_iterative.c below duet 1 FAIL
1.996 (1.589) FAIL
above 4 FAIL
2.28 (1.583)
pascals_iterative_unsafe.c below duet 1 OKAY
1.945 (1.581) PASS
above 4 OKAY
2.237 (1.607)
pascals_recursive.c below duet 9 FAIL
1.989 (0.712) FAIL
above 4 FAIL
1.399 (0.71)
pascals_recursive_unsafe.c below duet 9 OKAY
2.026 (0.706) PASS
above 4 OKAY
1.453 (0.709)
squared_solution.c below duet 4 FAIL
0.92 (0.653) FAIL
above 4 FAIL
1.145 (0.652)
squared_solution_unsafe.c below duet 4 OKAY
0.94 (0.666) PASS
above 4 OKAY
1.148 (0.642)
two_n_even.c below duet 2 PASS
0.783 (0.659) PASS
above 4 PASS
0.881 (0.666)
two_n_even_unsafe.c below duet 2 OKAY
0.794 (0.639) PASS
above 4 OKAY
0.879 (0.656)
two_n_odd.c below duet 2 PASS
0.787 (0.654) PASS
above 4 PASS
0.887 (0.667)
two_n_odd_unsafe.c below duet 2 OKAY
0.791 (0.653) PASS
above 4 OKAY
0.887 (0.672)
two_to_n_over_two_even.c below duet 7 FAIL
1.411 (0.65) FAIL
above 4 FAIL
1.125 (0.655)
two_to_n_over_two_even_unsafe.c below duet 7 OKAY
1.415 (0.651) PASS
above 4 OKAY
1.123 (0.68)
two_to_n_over_two_odd.c below duet 7 FAIL
1.409 (0.677) FAIL
above 4 FAIL
1.109 (0.648)
two_to_n_over_two_odd_unsafe.c below duet 7 OKAY
1.413 (0.671) PASS
above 4 OKAY
1.119 (0.678)
two_to_n_squared.c below duet 5 FAIL
8.346 (0.844) FAIL
above 4 FAIL
3.792 (0.843)
two_to_n_squared_unsafe.c below duet 5 OKAY
8.299 (0.839) PASS
above 4 OKAY
3.888 (0.854)
two_to_two_to_n.c below duet 7 FAIL
1.138 (0.658) FAIL
above 4 FAIL
1.225 (0.643)
two_to_two_to_n_unsafe.c below duet 7 OKAY
1.163 (0.663) PASS
above 4 OKAY
1.23 (0.652)
Total Below Time = 666.37 (was 33.535)
Above Time = 115.667 (was 33.925)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below duet 1 PASS
0.497 (0.443) PASS
above 4 PASS
0.546 (0.437)
adding_and_mult_unsafe.c below duet 1 OKAY
0.516 (0.435) PASS
above 4 OKAY
0.536 (0.423)
binary_search_array_tree.c below duet 1 FAIL
FAIL
1.258 (1.041) FAIL
FAIL
above 4 FAIL
FAIL
1.389 (1.022)
exp_add_linear.c below duet 1 PASS
1.077 (0.96) PASS
above 4 PASS
1.186 (0.932)
exp_add_linear_unsafe.c below duet 1 OKAY
1.085 (0.979) PASS
above 4 OKAY
1.162 (0.971)
exp_add_loop_rec.c below duet 1 FAIL
0.933 FAIL
above 4 FAIL
1.022 (0.923)
exp_add_loop_rec_unsafe.c below duet 1 OKAY
0.957 PASS
above 4 OKAY
1.015 (0.872)
exp_add_loop_variable.c below duet 1 PASS
1.111 (0.969) PASS
above 4 PASS
1.152 (0.97)
exp_add_loop_variable_unsafe.c below duet 1 OKAY
1.088 (0.948) PASS
above 4 OKAY
1.168 (0.927)
exp_with_linear_inner_loop.c below duet 1 FAIL
1.526 (1.313) FAIL
above 4 FAIL
1.673 (1.314)
exp_with_linear_inner_loop_unsafe.c below duet 1 OKAY
1.537 (1.333) PASS
above 4 OKAY
1.686 (1.318)
halving_log1.c below duet 1 FAIL
0.957 (0.778) FAIL
above 4 FAIL
1.095 (0.761)
linear_two_to_n.c below duet 7 FAIL
1.392 (0.884) FAIL
above 4 FAIL
1.542 (0.881)
linear_two_to_n_unsafe.c below duet 7 OKAY
1.397 (0.898) PASS
above 4 OKAY
1.573 (0.875)
loop_five_to_n.c below duet 1 PASS
0.966 (0.877) PASS
above 4 PASS
1.076 (0.864)
loop_five_to_n_unsafe.c below duet 1 OKAY
1.005 (0.891) PASS
above 4 OKAY
1.025 (0.892)
non_loop_five_to_n.c below duet 7 FAIL
2.11 (0.907) FAIL
above 4 FAIL
3.01 (0.921)
non_loop_five_to_n_unsafe.c below duet 7 OKAY
2.233 (0.905) PASS
above 4 OKAY
3.159 (0.908)
power_log_modified.c below duet 1 PASS
1.07 (0.854) PASS
above 4 PASS
1.198 (0.898)
simple_exponential.c below duet 1 PASS
0.999 (0.893) PASS
above 4 PASS
1.036 (0.902)
simple_exponential_for.c below duet 1 PASS
1.06 PASS
above 4 PASS
1.116 (0.929)
simple_exponential_for_unsafe.c below duet 1 OKAY
1.111 (0.962) PASS
above 4 OKAY
1.147 (0.945)
simple_exponential_unsafe.c below duet 1 OKAY
0.964 PASS
above 4 OKAY
1.06 (0.863)
two_to_n_minus_n.c below duet 7 FAIL
1.559 (0.902) FAIL
above 4 FAIL
1.754 (0.884)
two_to_n_minus_n_loop.c below duet 7 FAIL
1.843 (1.059) FAIL
above 4 FAIL
1.937 (1.01)
two_to_n_minus_n_loop_unsafe.c below duet 7 OKAY
1.876 (1.006) PASS
above 4 OKAY
1.912 (1.027)
two_to_n_minus_n_unsafe.c below duet 7 OKAY
1.582 (0.904) PASS
above 4 OKAY
1.756 (0.886)
Total Below Time = 33.709 (was 24.79)
Above Time = 37.931 (was 24.555)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below duet 3 PASS
0.921 (0.767) PASS
PASS
PASS
above 4 PASS
1.093 (0.802)
02.c below duet 3 FAIL
1.004 (0.829) FAIL
PASS
PASS
above 4 FAIL
1.233 (0.826)
03.c below duet 1 PASS
1.312 (1.178) PASS
PASS
above 4 PASS
1.438 (1.138)
04.c below duet 1 PASS
0.475 (0.431) PASS
PASS
PASS
above 4 PASS
0.512 (0.423)
05.c below duet 3 PASS
1.124 (0.946) PASS
PASS
PASS
above 4 PASS
1.432 (0.952)
06.c below duet 3 PASS
1.805 (1.306) PASS
PASS
PASS
above 4 PASS
2.588 (1.32)
07.c below duet 3 PASS
1.001 (0.843) PASS
PASS
PASS
above 4 PASS
1.136 (0.861)
08.c below duet 3 PASS
1.978 (1.633) PASS
PASS
PASS
above 4 PASS
2.731 (1.603)
09.c below duet 3 PASS
1.734 (1.393) PASS
PASS
PASS
above 4 PASS
2.144 (1.406)
10.c below duet 3 FAIL
1.099 (0.842) FAIL
PASS
PASS
above 4 FAIL
1.488 (0.813)
11.c below duet 1 PASS
0.562 PASS
PASS
PASS
above 4 PASS
0.616 (0.505)
12.c below duet 3 PASS
1.522 (1.161) PASS
PASS
PASS
above 4 PASS
1.929 (1.159)
13.c below duet 3 PASS
0.965 (0.835) PASS
PASS
PASS
above 4 PASS
1.151 (0.812)
14.c below duet 3 PASS
PASS
0.998 (0.852) PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.106 (0.838)
15.c below duet 1 PASS
0.843 PASS
PASS
PASS
above 4 PASS
0.899
16.c below duet 1 PASS
0.82 (0.718) PASS
PASS
PASS
above 4 PASS
0.908 (0.707)
17.c below duet 1 PASS
1.36 PASS
PASS
PASS
above 4 PASS
1.451 (1.199)
18.c below duet 1 PASS
0.897 PASS
PASS
PASS
above 4 PASS
0.964 (0.855)
19.c below duet 1 PASS
0.932 (0.787) PASS
PASS
PASS
above 4 PASS
1.012 (0.79)
20.c below duet 3 PASS
PASS
FAIL
1.182 (0.964) PASS
PASS
FAIL
PASS
PASS
above 4 PASS
PASS
FAIL
1.378 (0.946)
21.c below duet 3 PASS
0.971 (0.799) PASS
PASS
PASS
above 4 PASS
1.12 (0.825)
22.c below duet 3 PASS
PASS
1.181 (0.932) PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.419 (0.938)
23.c below duet 1 PASS
0.852 PASS
PASS
PASS
above 4 PASS
0.873 (0.789)
24.c below duet 1 PASS
1.678 PASS
PASS
PASS
above 4 PASS
1.819 (1.531)
25.c below duet 3 PASS
1.709 (1.382) PASS
PASS
PASS
above 4 PASS
2.099 (1.415)
26.c below duet 3 PASS
20.0 (1.467) PASS
PASS
PASS
above 4 PASS
51.078 (1.464)
27.c below duet 1 PASS
1.328 (1.175) PASS
PASS
PASS
above 4 PASS
1.422 (1.207)
28.c below duet 3 PASS
1.158 (0.979) PASS
PASS
PASS
above 4 PASS
1.32 (1.012)
29.c below duet 3 PASS
2.305 (1.931) PASS
PASS
PASS
above 4 PASS
2.692 (1.923)
30.c below duet 1 PASS
0.564 PASS
PASS
PASS
above 4 PASS
0.616 (0.509)
31.c below duet 3 PASS
PASS
3.135 (2.602) PASS
PASS
PASS
PASS
above 4 PASS
PASS
3.931 (2.577)
32.c below duet 1 FAIL
0.855 FAIL
PASS
PASS
above 4 FAIL
0.965 (0.787)
33.c below duet 3 PASS
1.689 (1.178) PASS
PASS
PASS
above 4 PASS
2.486 (1.204)
34.c below duet 1 FAIL
0.925 FAIL
PASS
PASS
above 4 FAIL
0.958 (0.854)
35.c below duet 1 PASS
0.82 PASS
PASS
PASS
above 4 PASS
0.874
36.c below duet 3 PASS
2.49 (1.77) PASS
PASS
PASS
above 4 PASS
3.945 (1.716)
37.c below duet 3 FAIL
1.0 (0.868) FAIL
PASS
PASS
above 4 FAIL
1.122 (0.857)
38.c below duet 1 FAIL
0.87 FAIL
PASS
PASS
above 4 FAIL
0.932 (0.808)
39.c below duet 3 PASS
PASS
1.085 (0.907) PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.206 (0.902)
40.c below duet 3 PASS
1.24 (0.991) PASS
PASS
PASS
above 4 PASS
1.617 (0.979)
41.c below duet 1 PASS
0.943 (0.837) PASS
PASS
PASS
above 4 PASS
0.978 (0.822)
42.c below duet 3 PASS
1.111 (0.854) PASS
PASS
PASS
above 4 PASS
1.445 (0.866)
43.c below duet 3 PASS
1.001 (0.799) PASS
PASS
PASS
above 4 PASS
1.248 (0.788)
44.c below duet 1 PASS
0.847 PASS
PASS
PASS
above 4 PASS
0.949 (0.799)
45.c below duet 3 PASS
1.978 (1.257) PASS
PASS
PASS
above 4 PASS
2.805 (1.229)
46.c below duet 3 PASS
1.59 (1.005) PASS
PASS
PASS
above 4 PASS
2.366 (0.965)
Total Below Time = 75.859 (was 47.525)
Above Time = 119.494 (was 47.349)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below duet 1 PASS
0.948 PASS
PASS
PASS
above 4 PASS
1.045 (0.883)
AGHKTW2017_foo.c below duet 1 PASS
1.038 (0.939) PASS
PASS
PASS
above 4 PASS
1.117 (0.928)
AGHKTW2017_loginSafe.c below duet 1 PASS
1.198 (1.054) PASS
PASS
PASS
above 4 PASS
1.412 (1.028)
AGHKTW2017_loopAndBranch_safe.c below duet 1 PASS
1.035 PASS
PASS
PASS
above 4 PASS
1.157 (0.977)
AGHKTW2017_loopAndBranch_unsafe.c below duet 1 OKAY
1.028 PASS
FAIL
FAIL
above 4 OKAY
1.139 (0.95)
BCK2011_gauss.c below duet 1 PASS
0.77 (0.635) PASS
PASS
PASS
above 4 PASS
0.856 (0.67)
BCK2011_strength_reduction.c below duet 1 PASS
1.1 (0.916) PASS
PASS
PASS
above 4 PASS
1.229 (0.97)
BCK2011_strength_reduction_linear.c below duet 1 PASS
1.067 (0.947) PASS
PASS
PASS
above 4 PASS
1.141 (0.916)
CFD17-add-const_product.c below duet 1 PASS
0.504 (0.439) PASS
above 4 PASS
0.548 (0.443)
CFD17-add-const_product-syntax.c below duet 1 PASS
0.778 (0.604) PASS
above 4 PASS
0.944 (0.611)
CFD17-add-const_self-comp.c below duet 1 FAIL
0.711 (0.592) FAIL
above 4 FAIL
0.769 (0.577)
collatz_product-syntax.c below duet 1 FAIL
4.061 (2.76) FAIL
above 4 FAIL
5.262 (2.784)
collatz_self-comp.c below duet 1 FAIL
1.337 (1.089) FAIL
above 4 FAIL
1.74 (1.06)
fibonacci_information_flow.c below duet 1 PASS
1.074 (0.942) PASS
PASS
PASS
above 4 PASS
1.209 (0.941)
halving_log1_product.c below duet 1 PASS
0.579 (0.487) PASS
above 4 PASS
0.669 (0.507)
halving_log1_product-syntax.c below duet 1 FAIL
0.926 (0.712) FAIL
above 4 FAIL
1.059 (0.705)
halving_log1_self-comp.c below duet 1 FAIL
0.812 (0.663) FAIL
above 4 FAIL
0.848 (0.652)
loop_splitting_test_safe.c below duet 1 PASS
PASS
0.681 (0.477) PASS
PASS
above 4 PASS
PASS
0.791 (0.476)
TA2005_fib2.c below duet 1 PASS
0.826 (0.655) PASS
PASS
PASS
above 4 PASS
1.035 (0.66)
TA2005_fib.c below duet 1 PASS
0.618 (0.51) PASS
PASS
PASS
above 4 PASS
0.702 (0.51)
top-level-if-add-const_product.c below duet 1 PASS
2.237 (1.627) PASS
above 4 PASS
2.843 (1.633)
top-level-if-add-const_self-comp.c below duet 1 FAIL
1.135 (0.891) FAIL
above 4 FAIL
1.267 (0.857)
Total Below Time = 24.463 (was 19.74)
Above Time = 28.782 (was 19.738)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/canonical2017
Total Below Time = 0.0 (was 0.0)
Above Time = 0.0 (was 0.0)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below duet 1 PASS
1.098 (0.927) PASS
above 4 PASS
1.293 (0.916)
c3_cleanup_better.c below duet 3 PASS
PASS
2.453 (1.854) PASS
PASS
above 4 PASS
PASS
2.939 (1.866)
c3_cleanup.c below duet 3 PASS
PASS
2.417 (1.844) PASS
PASS
above 4 PASS
PASS
2.883 (1.881)
c3_intermediate.c below duet 3 PASS
PASS
PASS
2.277 (1.746) PASS
PASS
PASS
above 4 PASS
PASS
PASS
2.716 (1.762)
c3_noinv.c below duet 3 FAIL
2.153 (1.652) FAIL
above 4 FAIL
2.497 (1.614)
doublers.c below duet 1 FAIL
1.392 (1.167) FAIL
above 4 FAIL
1.547 (1.196)
doublers_easier.c below duet 3 FAIL
1.795 (1.198) FAIL
above 4 FAIL
2.233 (1.189)
doublers_easy.c below duet 1 FAIL
1.95 FAIL
above 4 FAIL
2.203 (1.705)
exp_mult.c below duet 1 FAIL
0.95 (0.847) FAIL
above 4 FAIL
0.998 (0.826)
fig1_rotation_unsafe.c below duet 1 OKAY
0.554 (0.319) PASS
above EXCEPTION
0.305
guessing_game.c below duet 3 FAIL
0.846 (0.675) FAIL
above 4 FAIL
0.969 (0.669)
not_P_solvable.c below duet 1 PASS
0.473 PASS
above 4 PASS
0.536 (0.423)
Total Below Time = 18.358 (was 14.502)
Above Time = 21.119 (was 14.345)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below duet 1 PASS
PASS
PASS
FAIL
0.858 (0.732) PASS
PASS
PASS
FAIL
above 4 PASS
PASS
PASS
FAIL
0.909 (0.754)
maxequals_linear_1.c below duet 1 PASS
0.842 (0.739) PASS
above 4 PASS
0.952 (0.752)
maxequals_linear_2.c below duet 1 FAIL
0.917 (0.747) FAIL
above 4 FAIL
1.029 (0.755)
maxequals_linear_3.c below duet 1 FAIL
0.844 (0.765) FAIL
above 4 FAIL
0.902 (0.784)
maxequals_linear_4.c below duet 1 PASS
0.862 PASS
above 4 PASS
0.894 (0.759)
maxequals_linear_5.c below duet 1 PASS
0.84 (0.761) PASS
above 4 PASS
0.883 (0.776)
maxequals_linear_6.c below duet 1 FAIL
0.858 FAIL
above 4 FAIL
0.868 (0.789)
maxequals_matrix1.c below duet 3 FAIL
1.391 (0.881) FAIL
above 4 FAIL
2.023 (0.863)
maxequals_matrix2.c below duet 3 FAIL
1.614 (0.855) FAIL
above 4 FAIL
2.004 (0.843)
maxequals_quadratic1.c below duet 1 FAIL
0.86 FAIL
above 4 FAIL
0.92 (0.777)
maxequals_quadratic2.c below duet 1 PASS
0.872 (0.773) PASS
above 4 PASS
0.894 (0.776)
maxequals_stratified1.c below duet 3 PASS
3.228 (0.866) PASS
above 4 PASS
4.624 (0.857)
maxequals_stratified2.c below duet 3 PASS
2.508 (0.872) PASS
above 4 PASS
4.545 (0.838)
maxequals_stratified3.c below duet 3 FAIL
3.368 (0.875) FAIL
above 4 FAIL
4.641 (0.841)
nine.c below duet 1 PASS
PASS
FAIL
0.835 (0.744) PASS
PASS
FAIL
above 4 PASS
PASS
FAIL
0.867 (0.741)
nine_nondecreasing.c below duet 1 PASS
PASS
PASS
0.919 (0.749) PASS
PASS
PASS
above 4 PASS
PASS
PASS
1.044 (0.737)
sum_interval_1.c below duet 1 FAIL
FAIL
0.767 (0.669) FAIL
FAIL
above 4 FAIL
FAIL
0.856 (0.669)
sum_interval_2.c below duet 1 FAIL
FAIL
0.82 (0.687) FAIL
FAIL
above 4 FAIL
FAIL
0.899 (0.699)
sum_interval_3.c below duet 1 FAIL
FAIL
0.806 (0.662) FAIL
FAIL
above 4 FAIL
FAIL
0.893 (0.66)
TrackingObjectFields.c below duet TIMEOUT
300.017 (2.068)
above 4 124.431 (2.028)
TrackingObjectFields_inlined.c below duet 1 5.171 (4.059)
above 4 6.258 (4.037)
Total Below Time = 329.197 (was 20.861)
Above Time = 161.336 (was 20.735)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below duet 1 PASS
0.652 (0.517) PASS
above 4 PASS
0.743 (0.524)
bobble2_varloop.c below duet 1 PASS
0.581 (0.482) PASS
above 4 PASS
0.645 (0.464)
bobble3.c below duet 1 FAIL
0.569 (0.49) FAIL
above 4 FAIL
0.617 (0.481)
bobble4.c below duet 1 PASS
0.631 (0.526) PASS
above 4 PASS
0.725 (0.518)
bobble5.c below duet 1 PASS
0.656 (0.537) PASS
above 4 PASS
0.744 (0.525)
bobble.c below duet 1 PASS
0.626 (0.529) PASS
above 4 PASS
0.735 (0.535)
inchworm2.c below duet 1 PASS
128.552 (113.526) FAIL
above 4 FAIL
119.322
inchworm3.c below duet 1 PASS
119.867 PASS
above 4 PASS
113.723
inchworm4.c below duet 1 PASS
128.336 PASS
above 4 PASS
82.37 (102.488)
inchworm5.c below duet 1 PASS
0.724 PASS
above 4 PASS
0.547 (0.44)
inchworm6_unsafe.c below duet 1 OKAY
0.561 (0.478) PASS
above 4 OKAY
0.616 (0.487)
inchworm.c below duet 1 FAIL
108.905 PASS
above 4 FAIL
105.142 (119.717)
leapdiff2.c below duet 1 PASS
0.885 (0.787) PASS
above 4 PASS
0.668 (0.455)
leapfrog_annotated.c below duet 1 FAIL
0.622 (0.506) FAIL
above 4 FAIL
0.674 (0.507)
leapfrog_annotated_disjunction.c below duet 1 PASS
0.652 (0.545) PASS
above 4 PASS
0.722 (0.56)
leapfrog_asymmetric2.c below duet 1 FAIL
0.69 (0.562) FAIL
above 4 FAIL
0.745 (0.568)
leapfrog_asymmetric3.c below duet 1 FAIL
0.577 (0.49) FAIL
above 4 FAIL
0.667 (0.498)
leapfrog_asymmetric.c below duet 1 FAIL
0.546 (0.474) FAIL
above 4 FAIL
0.628 (0.459)
leapfrog.c below duet 1 FAIL
0.558 (0.451) FAIL
above 4 FAIL
0.587 (0.449)
leapfrog_materialized.c below duet 1 FAIL
0.624 (0.536) FAIL
above 4 FAIL
0.677 (0.511)
leapfrog_verbose.c below duet 1 FAIL
0.674 (0.573) FAIL
above 4 FAIL
0.769 (0.56)
leapspin.c below duet 1 PASS
0.497 (0.434) PASS
above 4 PASS
0.541 (0.431)
leapsum2.c below duet 1 FAIL
0.528 (0.463) FAIL
above 4 FAIL
0.585 (0.466)
leapthree.c below duet 1 FAIL
0.547 (0.485) FAIL
above 4 FAIL
0.646 (0.481)
microbobble2.c below duet 1 PASS
0.533 (0.482) PASS
above 4 PASS
0.581 (0.474)
microbobble3.c below duet 1 PASS
0.551 (0.465) PASS
above 4 PASS
0.605 (0.469)
microbobble_asymmetric.c below duet 1 PASS
0.517 (0.446) PASS
above 4 PASS
0.538 (0.454)
microbobble.c below duet 1 PASS
0.537 (0.464) PASS
above 4 PASS
0.571 (0.463)
simple_bl2.c below duet 1 PASS
0.592 (0.5) PASS
above 4 PASS
0.654 (0.498)
simple_bl3.c below duet 1 FAIL
0.579 (0.497) FAIL
above 4 FAIL
0.621 (0.498)
simple_bl.c below duet 1 FAIL
0.574 (0.475) FAIL
above 4 FAIL
0.616 (0.482)
Total Below Time = 501.943 (was 484.143)
Above Time = 438.024 (was 469.558)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below duet 1 PASS
PASS
0.771 PASS
PASS
above 4 PASS
PASS
0.805
binval_example_2_unsafe.c below duet 1 OKAY
0.779 PASS
above 4 OKAY
0.76
binval_example_3_unsafe.c below duet 1 OKAY
0.754 PASS
above 4 OKAY
0.756
binval_example_4.c below duet 1 PASS
PASS
PASS
0.819 (0.653) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.784 (0.642)
binval_example_4_unsafe.c below duet 1 OKAY
0.725 (0.659) PASS
above 4 OKAY
0.729 (0.659)
binval_example_5.c below duet 1 FAIL
FAIL
PASS
1.014 (0.794) FAIL
FAIL
PASS
above 4 FAIL
FAIL
PASS
1.084 (0.802)
binval_example_5_unsafe.c below duet 1 OKAY
0.931 (0.791) PASS
above 4 OKAY
1.026 (0.794)
Total Below Time = 5.793 (was 5.118)
Above Time = 5.944 (was 5.098)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/ethereum
array2_memory_contract.c below duet 1 1.6 (1.326)
above 4 1.724 (1.326)
array3_memory_contract.c below duet 1 1.6 (1.081)
above 4 2.143 (1.101)
array4_memory_contract.c below duet 1 1.952 (1.499)
above 4 2.232 (1.481)
arraylength_memory_contract.c below duet 1 0.791
above 4 0.779
array_memory_contract.c below duet 1 1.065 (0.941)
above 4 1.144 (0.95)
GovernMental.c below duet 1 37.058 (16.226)
above 4 38.364 (15.876)
HelloWorld.c below duet 1 0.65
above 4 0.648
linear2_memory_contract.c below duet 1 1.327 (1.095)
above 4 1.397 (1.123)
linear2_no_memory_contract.c below duet 1 1.253 (1.06)
above 4 1.415 (1.043)
linear3_no_memory_contract.c below duet 1 1.341 (1.177)
above 4 1.517 (1.143)
Linear.c below duet 1 0.981
above 4 1.077 (0.894)
linear_memory_contract.c below duet 1 0.987 (0.882)
above 4 1.072 (0.899)
linear_no_memory_contract.c below duet 1 1.016 (0.865)
above 4 1.078 (0.887)
nested2_memory_contract.c below duet 1 1.517 (1.265)
above 4 1.792 (1.299)
nested2_no_memory_contract.c below duet 1 1.609 (1.323)
above 4 1.802 (1.313)
nested_memory_contract.c below duet 1 1.492 (1.289)
above 4 1.651 (1.291)
nested_no_memory_contract.c below duet 1 1.433 (1.218)
above 4 1.587 (1.205)
Total Below Time = 57.672 (was 33.502)
Above Time = 61.422 (was 33.191)

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