[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.817 PASS
above 4 PASS
0.86
kmp.c below duet EXCEPTION
0.62
above EXCEPTION
0.632
qsort.c below duet 7 PASS
1.562 FAIL
above 4 FAIL
2.203
speed_pldi09_fig1.c below duet 1 PASS
0.936 PASS
above 4 PASS
1.034
speed_pldi09_fig4_2.c below duet 1 PASS
0.878 PASS
above 4 PASS
0.953
speed_pldi09_fig4_4.c below duet 1 PASS
0.86 PASS
above 4 PASS
0.976
speed_pldi09_fig4_5.c below duet 1 PASS
0.796 PASS
above 4 PASS
0.892
speed_pldi10_ex1.c below duet 1 PASS
1.865 PASS
above 4 PASS
2.712
speed_pldi10_ex3.c below duet 1 PASS
0.837 PASS
above 4 PASS
1.049
speed_pldi10_ex4.c below duet 1 PASS
0.921 PASS
above 4 PASS
1.057
speed_popl10_fig2_1.c below duet 1 PASS
0.815 PASS
above 4 PASS
0.926
speed_popl10_fig2_2.c below duet 1 FAIL
0.751 FAIL
above 4 FAIL
0.812
speed_popl10_nested_multiple.c below duet 1 PASS
0.909 PASS
above 4 PASS
1.024
speed_popl10_nested_single.c below duet 1 FAIL
1.026 FAIL
above 4 FAIL
1.157
speed_popl10_sequential_single.c below duet 1 PASS
0.892 PASS
above 4 PASS
0.974
speed_popl10_simple_multiple.c below duet 1 PASS
0.888 PASS
above 4 PASS
1.01
speed_popl10_simple_single_2.c below duet 1 PASS
0.989 PASS
above 4 PASS
1.19
speed_popl10_simple_single.c below duet 1 PASS
0.742 PASS
above 4 PASS
0.781
t07.c below duet 1 PASS
0.833 PASS
above 4 PASS
0.904
t08.c below duet 1 PASS
0.798 PASS
above 4 PASS
0.885
t09.c below duet 1 PASS
0.831 PASS
above 4 PASS
0.876
t10.c below duet 1 PASS
0.719 PASS
above 4 PASS
0.775
t11.c below duet 1 PASS
0.779 PASS
above 4 PASS
0.918
t13.c below duet 1 FAIL
0.82 FAIL
above 4 FAIL
0.887
t15.c below duet 1 PASS
0.812 PASS
above 4 PASS
0.897
t16.c below duet 1 PASS
0.891 PASS
above 4 PASS
0.975
t19.c below duet 1 PASS
0.768 PASS
above 4 PASS
0.847
t20.c below duet 1 PASS
0.788 PASS
above 4 PASS
0.86
t27.c below duet 1 PASS
0.835 PASS
above 4 PASS
0.976
t28.c below duet 1 PASS
0.884 PASS
above 4 PASS
1.006
t30.c below duet 1 FAIL
0.71 FAIL
above 4 FAIL
0.746
t37.c below duet 2 PASS
1.014 FAIL
above 4 PASS
1.207
t39.c below duet 2 PASS
0.956 FAIL
above 4 PASS
1.084
t46.c below duet 1 PASS
0.821 PASS
above 4 PASS
0.926
t47.c below duet 1 FAIL
0.794 FAIL
above 4 FAIL
0.892
Total Below Time = 31.157 (was 31.122)
Above Time = 35.903 (was 35.843)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below duet 2 PASS
PASS
0.816 PASS
PASS
above 4 PASS
PASS
0.893
qsort_full.c below duet 4 PASS
PASS
PASS
PASS
PASS
PASS
2.935 PASS
PASS
PASS
PASS
PASS
PASS
above 4 FAIL
PASS
PASS
PASS
PASS
PASS
4.546
rec1-param_safe.c below duet 2 PASS
PASS
PASS
0.79 PASS
FAIL
PASS
above 4 PASS
PASS
PASS
0.881
rec1-param_unsafe.c below duet 2 OKAY
0.753 PASS
above 4 OKAY
0.798
rec1_safe.c below duet 2 PASS
PASS
PASS
0.813 PASS
FAIL
PASS
above 4 PASS
PASS
PASS
0.822
rec1_unsafe.c below duet 2 OKAY
0.741 PASS
above 4 OKAY
0.805
rec2-param_safe.c below duet 2 PASS
PASS
PASS
0.807 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.861
rec2-param_unsafe.c below duet 2 OKAY
0.734 PASS
above 4 OKAY
0.83
rec2_safe.c below duet 2 PASS
PASS
PASS
0.766 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.83
rec2_unsafe.c below duet 2 OKAY
0.736 PASS
above 4 OKAY
0.782
rec-test.c below duet 2 PASS
0.76 FAIL
above 4 PASS
0.815
sas03_bothbranches.c below duet 7 PASS
1.081 PASS
above 4 FAIL
1.189
sas03.c below duet 2 PASS
1.118 PASS
above 4 PASS
1.299
simulated_lese_recursive.c below duet 2 PASS
0.783 PASS
above 4 PASS
0.871
Total Below Time = 13.633 (was 13.601)
Above Time = 16.222 (was 16.193)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below duet 1 PASS
0.484 PASS
above 4 PASS
0.53
count_up_down_unsafe.c below duet 1 OKAY
0.446 PASS
above 4 OKAY
0.507
divide.c below duet 1 PASS
0.49 PASS
above 4 PASS
0.537
factor_unsafe.c below duet 1 OKAY
0.512 PASS
above 4 OKAY
0.545
for_infinite_loop_1_safe.c below duet 1 PASS
0.424 PASS
above 0 PASS
0.452
for_infinite_loop_2_safe.c below duet 1 PASS
0.442 PASS
above 0 PASS
0.477
interproc.c below duet 1 PASS
0.619 PASS
above 4 PASS
0.66
mult.c below duet 1 PASS
PASS
0.503 PASS
PASS
above 4 PASS
PASS
0.529
pointer_arith.c below duet 1 PASS
PASS
PASS
PASS
0.406 PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
0.409
quotient.c below duet 3 PASS
0.906 PASS
above 4 PASS
1.093
subtract.c below duet 1 PASS
0.399 PASS
above 4 PASS
0.439
sum01_bug02_sum01_bug02_base.case_unsafe.c below duet 1 OKAY
0.548 PASS
above 4 OKAY
0.585
sum01_bug02_unsafe.c below duet 1 OKAY
0.641 PASS
above 4 OKAY
0.743
sum01_real_safe.c below duet 1 PASS
0.516 PASS
above 4 PASS
0.547
sum01_safe.c below duet 1 PASS
0.489 PASS
above 4 PASS
0.511
sum01_unsafe.c below duet 1 OKAY
0.628 PASS
above 4 OKAY
0.712
sum02_safe.c below duet 1 PASS
0.5 PASS
above 4 PASS
0.543
sum03_safe.c below duet 1 PASS
0.464 PASS
above 0 PASS
0.5
sum03_unsafe.c below duet 1 OKAY
0.631 PASS
above 0 OKAY
0.706
sum04_safe.c below duet 1 PASS
0.526 PASS
above 4 PASS
0.565
sum04_unsafe.c below duet 1 OKAY
0.596 PASS
above 4 OKAY
0.69
terminator_02_safe.c below duet 1 PASS
0.409 PASS
above 4 PASS
0.434
terminator_02_unsafe.c below duet 1 OKAY
0.422 PASS
above 4 OKAY
0.477
terminator_03_safe.c below duet 1 PASS
0.42 PASS
above 4 PASS
0.463
terminator_03_unsafe.c below duet 1 OKAY
0.433 PASS
above 4 OKAY
0.464
token_ring01_safe.c below duet 4 FAIL
36.188 FAIL
above 4 FAIL
95.156
token_ring01_unsafe.c below duet 4 OKAY
51.887 PASS
above 4 OKAY
206.955
toy_safe.c below duet TIMEOUT
300.042 FAIL
above TIMEOUT
300.046
trex01_safe.c below duet 1 PASS
1.058 PASS
above 4 PASS
1.109
trex01_unsafe.c below duet 1 OKAY
1.026 PASS
above 4 OKAY
1.133
trex02_safe2.c below duet 3 PASS
0.832 PASS
above 4 PASS
0.952
trex02_safe.c below duet 3 PASS
0.78 PASS
above 4 PASS
0.887
trex02_unsafe.c below duet 3 OKAY
0.777 PASS
above 4 OKAY
0.886
trex03_safe.c below duet 1 PASS
0.516 PASS
above 4 PASS
0.606
trex03_unsafe.c below duet 1 OKAY
0.52 PASS
above 4 OKAY
0.595
trex04_safe.c below duet 1 PASS
0.764 PASS
above 4 PASS
0.827
while_infinite_loop_1_safe.c below duet 1 PASS
0.377 PASS
above 0 PASS
0.401
while_infinite_loop_2_safe.c below duet 1 PASS
0.374 PASS
above 0 PASS
0.39
while_infinite_loop_3_safe.c below duet 1 PASS
0.68 PASS
above 4 PASS
0.681
Total Below Time = 408.675 (was 409.033)
Above Time = 624.742 (was 620.85)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below duet 3 PASS
0.821 PASS
above 4 FAIL
0.911
blogger_simplified1.c below duet 3 PASS
1.702 PASS
above 4 PASS
2.365
divided_difference2.c below duet 3 PASS
PASS
PASS
3.735 PASS
PASS
PASS
above 4 PASS
PASS
PASS
4.318
mult-proc.c below duet 3 PASS
PASS
0.799 PASS
PASS
above 4 PASS
PASS
0.924
mult-proc-params.c below duet 3 PASS
PASS
0.841 PASS
PASS
above 4 PASS
PASS
0.975
popall.c below duet 1 PASS
PASS
PASS
PASS
PASS
0.891 PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
1.034
simulated_scc.c below duet 1 PASS
PASS
1.152 PASS
PASS
above 4 PASS
PASS
1.286
Total Below Time = 9.941 (was 10.002)
Above Time = 11.813 (was 11.838)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below duet 1 PASS
0.815 PASS
above 4 PASS
0.837
degree2_binomial.c below duet 1 PASS
1.266 PASS
above 4 PASS
1.489
degree2_monomial.c below duet 1 PASS
1.139 PASS
above 4 PASS
1.226
degree3_binomial.c below duet 1 PASS
2.337 PASS
above 4 PASS
2.927
degree3_monomial.c below duet 1 PASS
1.621 PASS
above 4 PASS
1.767
degree4_binomial.c below duet 1 PASS
4.479 PASS
above 4 PASS
6.094
degree4_monomial.c below duet 1 PASS
2.412 PASS
above 4 PASS
2.642
degree5_binomial.c below duet 1 PASS
11.896 PASS
above 4 PASS
18.989
degree5_monomial.c below duet 1 PASS
3.561 PASS
above 4 PASS
3.919
Total Below Time = 29.526 (was 29.416)
Above Time = 39.89 (was 39.93)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below duet 1 PASS
0.548 PASS
above 4 PASS
0.584
cubic_with_square_interproc.c below duet 2 PASS
0.838 FAIL
above 4 PASS
0.941
cubic_with_square_nonlinear.c below duet 1 PASS
0.571 PASS
above 4 PASS
0.593
cubic_with_square_nonlinear_interproc.c below duet 2 PASS
0.777 FAIL
above 4 PASS
0.846
cubic_with_square_nonlinear_unsafe.c below duet 1 OKAY
0.544 PASS
above 4 OKAY
0.594
cubic_with_square_unsafe.c below duet 1 OKAY
0.556 PASS
above 4 OKAY
0.596
multi-input.c below duet 1 PASS
0.699 PASS
above 4 PASS
0.872
multi-input_unsafe.c below duet 1 OKAY
0.731 PASS
above 4 OKAY
0.902
nondet_loop_bound.c below duet 1 PASS
0.511 PASS
above 4 PASS
0.572
nondet_loop_bound_quartic.c below duet 1 PASS
0.538 PASS
above 4 PASS
0.579
nondet_loop_bound_quartic_unsafe.c below duet 1 OKAY
0.552 PASS
above 4 OKAY
0.603
nondet_loop_bound_unsafe.c below duet 1 OKAY
0.521 PASS
above 4 OKAY
0.551
nonlinear_stratified.c below duet 1 PASS
189.412 PASS
above 4 PASS
189.584
nonlinear_stratified_unsafe.c below duet 1 TIMEOUT
300.007 TIMEOUT
above 4 TIMEOUT
300.007
quartic_with_cube.c below duet 1 PASS
0.57 PASS
above 4 PASS
0.66
quartic_with_cube_nonlinear.c below duet 1 PASS
0.568 PASS
above 4 PASS
0.637
quartic_with_cube_nonlinear_unsafe.c below duet 1 OKAY
0.583 PASS
above 4 OKAY
0.656
quartic_with_cube_unsafe.c below duet 1 OKAY
0.504 PASS
above 4 OKAY
0.543
quintic_with_quartic.c below duet 1 PASS
0.682 PASS
above 4 PASS
0.818
quintic_with_quartic_nonlinear.c below duet 1 PASS
0.744 PASS
above 4 PASS
0.89
quintic_with_quartic_nonlinear_unsafe.c below duet 1 OKAY
0.735 PASS
above 4 OKAY
0.903
quintic_with_quartic_unsafe.c below duet 1 OKAY
0.648 PASS
above 4 OKAY
0.826
Total Below Time = 501.839 (was 501.452)
Above Time = 503.757 (was 504.177)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below duet 1 PASS
1.39 PASS
above 4 PASS
2.101
degree2_FD_AllAux_AllAssm.c below duet 1 PASS
5.127 PASS
above 4 PASS
9.198
degree2_FD_AllAux_FewAssm.c below duet 1 PASS
4.933 PASS
above 4 PASS
8.854
degree2_FD_FewAux_FewAssm.c below duet 1 PASS
1.908 PASS
above 4 PASS
3.005
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below duet 1 PASS
1.929 PASS
above 4 PASS
3.028
degree3.c below duet 1 PASS
1.641 PASS
above 4 PASS
2.494
degree3_FD.c below duet 1 PASS
1.91 PASS
above 4 PASS
2.993
degree4.c below duet 1 PASS
1.363 PASS
above 4 PASS
1.488
Total Below Time = 20.201 (was 20.162)
Above Time = 33.161 (was 32.729)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below duet EXCEPTION
0.323
above EXCEPTION
0.323
loop_unsafe.c below duet EXCEPTION
0.329
above EXCEPTION
0.329
simulated_lese_parser.c below duet 1 PASS
0.814 PASS
above 4 PASS
0.826
simulated_lese_sentinel.c below duet 1 PASS
0.803 PASS
above 4 PASS
0.806
Total Below Time = 2.269 (was 2.24)
Above Time = 2.284 (was 2.296)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below duet 1 PASS
PASS
PASS
0.597 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.67
Total Below Time = 0.597 (was 0.6)
Above Time = 0.67 (was 0.649)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below duet TIMEOUT
300.02 TIMEOUT
above TIMEOUT
300.013
Total Below Time = 300.02 (was 300.025)
Above Time = 300.013 (was 300.015)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below duet 1 OKAY
0.51 PASS
above 4 OKAY
0.543
array_false-unreach-call2.c below duet 1 OKAY
0.514 PASS
above 4 OKAY
0.549
array_false-unreach-call3.c below duet 1 OKAY
0.585 PASS
above 4 OKAY
0.636
array_true-unreach-call1.c below duet 1 FAIL
0.509 FAIL
above 4 FAIL
0.534
array_true-unreach-call2.c below duet 1 FAIL
0.506 FAIL
above 4 FAIL
0.536
array_true-unreach-call3.c below duet 1 PASS
0.542 PASS
above 4 PASS
0.594
array_true-unreach-call4.c below duet 1 FAIL
0.544 FAIL
above 4 FAIL
0.555
const_false-unreach-call1.c below duet 1 OKAY
0.492 PASS
above 4 OKAY
0.529
const_true-unreach-call1.c below duet 1 PASS
0.489 PASS
above 4 PASS
0.524
diamond_false-unreach-call1.c below duet 1 OKAY
0.528 PASS
above 4 OKAY
0.582
diamond_true-unreach-call1.c below duet 1 PASS
0.539 PASS
above 4 PASS
0.589
diamond_true-unreach-call2.c below duet 1 PASS
0.568 PASS
above 4 PASS
0.618
functions_false-unreach-call1.c below duet 3 OKAY
0.796 PASS
above 4 OKAY
0.883
functions_true-unreach-call1.c below duet 3 PASS
0.818 PASS
above 4 PASS
0.925
multivar_false-unreach-call1.c below duet 1 OKAY
0.419 PASS
above 4 OKAY
0.442
multivar_true-unreach-call1.c below duet 1 PASS
0.411 PASS
above 4 PASS
0.445
nested_false-unreach-call1.c below duet 1 OKAY
0.848 PASS
above 4 OKAY
0.885
nested_true-unreach-call1.c below duet 1 PASS
0.837 PASS
above 4 PASS
0.896
overflow_true-unreach-call1.c below duet 1 PASS
0.453 PASS
above 4 PASS
0.465
phases_false-unreach-call1.c below duet 1 OKAY
0.585 PASS
above 4 OKAY
0.678
phases_false-unreach-call2.c below duet 1 OKAY
0.583 PASS
above 4 OKAY
0.646
phases_true-unreach-call1.c below duet 1 PASS
0.564 PASS
above 4 PASS
0.663
phases_true-unreach-call2.c below duet 1 FAIL
0.589 FAIL
above 4 FAIL
0.653
simple_false-unreach-call1.c below duet 1 OKAY
0.487 PASS
above 4 OKAY
0.512
simple_false-unreach-call2.c below duet 1 OKAY
0.397 PASS
above 4 OKAY
0.416
simple_false-unreach-call3.c below duet 1 OKAY
0.468 PASS
above 4 OKAY
0.493
simple_false-unreach-call4.c below duet 1 OKAY
0.486 PASS
above 4 OKAY
0.527
simple_true-unreach-call1.c below duet 1 PASS
0.479 PASS
above 4 PASS
0.515
simple_true-unreach-call2.c below duet 1 PASS
0.389 PASS
above 4 PASS
0.404
simple_true-unreach-call3.c below duet 1 PASS
0.488 PASS
above 4 PASS
0.51
simple_true-unreach-call4.c below duet 1 PASS
0.488 PASS
above 4 PASS
0.521
underapprox_false-unreach-call1.c below duet 1 OKAY
0.514 PASS
above 4 OKAY
0.536
underapprox_false-unreach-call2.c below duet 1 OKAY
0.493 PASS
above 4 OKAY
0.523
underapprox_true-unreach-call1.c below duet 1 PASS
0.521 PASS
above 4 PASS
0.536
underapprox_true-unreach-call2.c below duet 1 PASS
0.486 PASS
above 4 PASS
0.544
Total Below Time = 18.925 (was 18.901)
Above Time = 20.407 (was 20.519)
/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.712 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.865
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.175 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.253
down_true-unreach-call.c below duet 1 PASS
0.543 PASS
above 4 PASS
0.606
fragtest_simple_true-unreach-call.c below duet 1 PASS
1.009 PASS
above 4 PASS
1.123
half_2_true-unreach-call.c below duet 1 PASS
0.697 PASS
above 4 PASS
0.755
heapsort_true-unreach-call.c below duet 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
5.967 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.249
id_build_true-unreach-call.c below duet 1 PASS
PASS
0.974 PASS
PASS
above 4 PASS
PASS
1.02
id_trans_false-unreach-call.c below duet 1 OKAY
0.643 PASS
above 4 OKAY
0.687
id_trans_true-unreach-call.c below duet 1 PASS
PASS
PASS
0.714 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.734
large_const_true-unreach-call.c below duet 1 PASS
0.668 PASS
above 4 PASS
0.792
MADWiFi-encode_ie_ok_true-unreach-call.c below duet 1 PASS
PASS
0.829 PASS
PASS
above 4 PASS
PASS
0.888
nested6_true-unreach-call.c below duet 1 PASS
PASS
PASS
2.051 PASS
PASS
PASS
above 4 PASS
PASS
PASS
2.192
nested9_true-unreach-call.c below duet 1 PASS
3.196 PASS
above 4 PASS
3.549
nest-if3_true-unreach-call.c below duet 1 PASS
0.858 PASS
above 4 PASS
0.941
NetBSD_loop_true-unreach-call.c below duet 1 PASS
PASS
0.632 PASS
PASS
above 4 PASS
PASS
0.684
sendmail-close-angle_true-unreach-call.c below duet 1 PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
1.038 PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
above 4 PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
1.089
seq_true-unreach-call.c below duet 1 PASS
0.989 PASS
above 4 PASS
1.088
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.878 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
8.872
string_concat-noarr_true-unreach-call.c below duet 1 PASS
1.1 PASS
above 4 PASS
1.157
up_true-unreach-call.c below duet 1 PASS
0.662 PASS
above 4 PASS
0.726
Total Below Time = 32.335 (was 32.134)
Above Time = 41.27 (was 41.349)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below duet 1 PASS
0.596 PASS
above 4 PASS
0.612
bhmr2007_true-unreach-call.c below duet 1 PASS
0.555 PASS
above 4 PASS
0.592
cggmp2005b_true-unreach-call.c below duet 1 PASS
1.113 PASS
above 4 PASS
1.24
cggmp2005_true-unreach-call.c below duet 1 PASS
0.514 PASS
above 4 PASS
0.525
cggmp2005_variant_true-unreach-call.c below duet 1 PASS
0.501 PASS
above 4 PASS
0.535
css2003_true-unreach-call.c below duet 1 PASS
0.661 PASS
above 4 PASS
0.71
ddlm2013_true-unreach-call.c below duet 1 PASS
0.63 PASS
above 4 PASS
0.736
gcnr2008_false-unreach-call.c below duet 1 OKAY
1.083 PASS
above 4 OKAY
1.308
gj2007b_true-unreach-call.c below duet 1 PASS
FAIL
0.548 PASS
FAIL
above 4 PASS
FAIL
0.588
gj2007_true-unreach-call.c below duet 1 PASS
0.602 PASS
above 4 PASS
0.688
gr2006_true-unreach-call.c below duet 1 PASS
0.592 PASS
above 4 PASS
0.687
gsv2008_true-unreach-call.c below duet 1 PASS
0.511 PASS
above 4 PASS
0.532
hhk2008_true-unreach-call.c below duet 1 PASS
0.519 PASS
above 4 PASS
0.551
jm2006_true-unreach-call.c below duet 1 PASS
0.523 PASS
above 4 PASS
0.549
jm2006_variant_true-unreach-call.c below duet 1 PASS
0.569 PASS
above 4 PASS
0.599
mcmillan2006_true-unreach-call.c below duet 1 FAIL
0.722 FAIL
above 4 FAIL
0.765
Total Below Time = 10.239 (was 10.161)
Above Time = 11.217 (was 11.271)
/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.505 PASS
above 4 PASS
0.508
count_by_1_variant_true-unreach-call.c below duet 1 PASS
0.509 PASS
above 4 PASS
0.55
count_by_2_true-unreach-call.c below duet 1 PASS
0.496 PASS
above 4 PASS
0.529
count_by_k_true-unreach-call.c below duet 1 PASS
0.5 PASS
above 4 PASS
0.55
count_by_nondet_true-unreach-call.c below duet 1 FAIL
0.53 FAIL
above 4 FAIL
0.568
gauss_sum_true-unreach-call.c below duet 1 PASS
0.506 PASS
above 4 PASS
0.555
half_true-unreach-call.c below duet 1 FAIL
0.532 FAIL
above 4 FAIL
0.584
nested_true-unreach-call.c below duet 1 PASS
1.034 PASS
above 4 PASS
1.071
Total Below Time = 4.612 (was 4.64)
Above Time = 4.915 (was 4.991)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below duet 1 OKAY
0.48 PASS
above 4 OKAY
0.495
array_true-unreach-call.c below duet 1 FAIL
0.449 FAIL
above 4 FAIL
0.509
bubble_sort_false-unreach-call.c below duet 4 OKAY
UNSOUND
3.821 PASS
FAIL
above 4 OKAY
UNSOUND
16.023
bubble_sort_true-unreach-call.c below duet 1 2.208
above 4 2.353
compact_false-unreach-call.c below duet EXCEPTION
0.318
above EXCEPTION
0.324 (0.385)
count_up_down_false-unreach-call_true-termination.c below duet 1 OKAY
0.481 PASS
above 4 OKAY
0.505
count_up_down_true-unreach-call_true-termination.c below duet 1 PASS
0.465 PASS
above 4 PASS
0.504
eureka_01_false-unreach-call.c below duet EXCEPTION
0.347
above EXCEPTION
0.327
eureka_01_true-unreach-call.c below duet EXCEPTION
0.348
above EXCEPTION
0.344
eureka_05_true-unreach-call.c below duet EXCEPTION
0.617
above EXCEPTION
0.622
for_bounded_loop1_false-unreach-call_true-termination.c below duet 1 OKAY
0.481 PASS
above 4 OKAY
0.521
for_bounded_loop1_true-unreach-call_true-termination.c below duet 1 PASS
PASS
0.582 PASS
PASS
above 4 PASS
PASS
0.607
for_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.448 PASS
above 0 PASS
0.473
for_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.442 PASS
above 0 PASS
0.458
heavy_false-unreach-call.c below duet 1 OKAY
1.564 PASS
above 4 OKAY
1.589
heavy_true-unreach-call.c below duet 1 PASS
1.484 PASS
above 4 PASS
1.631
insertion_sort_false-unreach-call.c below duet 1 OKAY
1.255 PASS
above 4 OKAY
1.503
insertion_sort_true-unreach-call.c below duet 1 FAIL
1.044 FAIL
above 4 FAIL
1.174
invert_string_false-unreach-call.c below duet 1 OKAY
0.851 PASS
above 4 OKAY
0.932
invert_string_true-unreach-call.c below duet 1 FAIL
1.009 FAIL
above 4 FAIL
1.135
linear_sea.ch_true-unreach-call.c below duet 1 FAIL
0.868 FAIL
above 4 FAIL
0.937
linear_search_false-unreach-call.c below duet 1 OKAY
0.928 PASS
above 4 OKAY
0.983
lu.cmp_true-unreach-call.c below duet 3 PASS
8.078 PASS
above 4 PASS
10.744
ludcmp_false-unreach-call.c below duet 3 OKAY
7.427 PASS
above 4 OKAY
10.227
matrix_false-unreach-call_true-termination.c below duet 1 OKAY
1.398 PASS
above 4 OKAY
1.52
matrix_true-unreach-call_true-termination.c below duet 1 FAIL
0.611 FAIL
above 4 FAIL
0.667
n.c11_true-unreach-call.c below duet EXCEPTION
0.591
above EXCEPTION
0.603
n.c24_false-unreach-call.c below duet EXCEPTION
0.622
above EXCEPTION
0.617
n.c40_true-unreach-call.c below duet EXCEPTION
0.327
above EXCEPTION
0.326
nec11_false-unreach-call.c below duet EXCEPTION
0.601
above EXCEPTION
0.624
nec20_false-unreach-call.c below duet EXCEPTION
0.617
above EXCEPTION
0.608
nec40_true-unreach-call.c below duet EXCEPTION
0.323
above EXCEPTION
0.309
string_false-unreach-call.c below duet 1 OKAY
1.495 PASS
above 4 OKAY
1.651
string_true-unreach-call.c below duet 1 FAIL
1.516 FAIL
above 4 FAIL
1.638
sum01_bug02_false-unreach-call_true-termination.c below duet 1 OKAY
0.688 PASS
above 4 OKAY
0.782
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below duet 1 OKAY
0.537 PASS
above 4 OKAY
0.557
sum01_false-unreach-call_true-termination.c below duet 1 OKAY
0.619 PASS
above 4 OKAY
0.687
sum01_true-unreach-call_true-termination.c below duet 1 PASS
0.517 PASS
above 4 PASS
0.544
sum03_false-unreach-call_true-termination.c below duet 1 OKAY
0.585 PASS
above 0 OKAY
0.684
sum03_true-unreach-call_false-termination.c below duet 1 PASS
0.541 PASS
above 4 PASS
0.603
sum04_false-unreach-call_true-termination.c below duet 1 OKAY
0.6 PASS
above 4 OKAY
0.691
sum04_true-unreach-call_true-termination.c below duet 1 PASS
0.528 PASS
above 4 PASS
0.552
sum_array_false-unreach-call.c below duet 1 OKAY
0.942 PASS
above 4 OKAY
1.068
sum_array_true-unreach-call.c below duet 1 FAIL
0.935 FAIL
above 4 FAIL
1.076
terminator_01_false-unreach-call_false-termination.c below duet 1 OKAY
0.408 PASS
above 4 OKAY
0.426
terminator_02_false-unreach-call_true-termination.c below duet 1 OKAY
0.716 PASS
above 4 OKAY
0.695
terminator_02_true-unreach-call_true-termination.c below duet 2 PASS
0.714 PASS
above 4 PASS
0.862
terminator_03_false-unreach-call_true-termination.c below duet 1 OKAY
0.422 PASS
above 4 OKAY
0.447
terminator_03_true-unreach-call_true-termination.c below duet 1 PASS
0.414 PASS
above 4 PASS
0.472
trex01_false-unreach-call_true-termination.c below duet 3 OKAY
1.291 PASS
above 4 OKAY
1.492
trex01_true-unreach-call.c below duet 3 PASS
1.427 PASS
above 4 PASS
1.705
trex02_false-unreach-call_true-termination.c below duet 3 OKAY
0.76 PASS
above 4 OKAY
0.891
trex02_true-unreach-call_true-termination.c below duet 3 PASS
0.799 PASS
above 4 PASS
0.925
trex03_false-unreach-call_true-termination.c below duet 3 OKAY
0.927 PASS
above 4 OKAY
1.176
trex03_true-unreach-call.c below duet 3 PASS
0.94 PASS
above 4 PASS
1.196
trex04_true-unreach-call_false-termination.c below duet 1 PASS
0.929 PASS
above 4 PASS
1.067
veris.c_NetBSD-libc__loop_true-unreach-call.c below duet 1 PASS
0.734 PASS
above 4 PASS
0.744
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below duet EXCEPTION
0.642
above EXCEPTION
0.647
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below duet 1 PASS
0.56 PASS
above 4 PASS
0.593
verisec_NetBSD-libc__loop_false-unreach-call.c below duet 1 OKAY
0.724 PASS
above 4 OKAY
0.776
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below duet EXCEPTION
0.639
above EXCEPTION
0.674
vogal_false-unreach-call.c below duet 1 OKAY
2.15 PASS
above 4 OKAY
2.28
vogal_true-unreach-call.c below duet 1 FAIL
1.952 FAIL
above 4 FAIL
2.087
while_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.371 PASS
above 0 PASS
0.404
while_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.378 PASS
above 0 PASS
0.395
while_infinite_loop_3_true-unreach-call_false-termination.c below duet 1 PASS
0.654 PASS
above 4 PASS
0.658
while_infinite_loop_4_false-unreach-call_true-termination.c below duet 1 OKAY
0.663 PASS
above 4 OKAY
0.664
Total Below Time = 69.802 (was 69.388)
Above Time = 92.003 (was 92.214)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below duet 7 PASS
1.433 FAIL
above 4 FAIL
1.535
Ackermann02_false-unreach-call_false-termination.c below duet 7 OKAY
1.324 PASS
above 4 OKAY
1.515
Ackermann03_true-unreach-call.c below duet 7 FAIL
1.44 FAIL
above 4 FAIL
1.546
Ackermann04_true-unreach-call.c below duet 7 FAIL
1.446 FAIL
above 4 FAIL
1.545
Addition01_true-unreach-call_true-termination.c below duet 2 PASS
1.12 PASS
above 4 PASS
1.191
Addition02_false-unreach-call_false-termination.c below duet 2 OKAY
0.989 PASS
above 4 OKAY
1.113
Addition03_false-no-overflow.c below duet 2 PASS
1.065 PASS
above 4 PASS
1.147
Addition03_true-unreach-call.c below duet 2 PASS
1.042 PASS
above 4 PASS
1.14
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below duet 2 OKAY
0.84 PASS
above 4 OKAY
0.945
EvenOdd01_true-unreach-call_true-termination.c below duet 2 PASS
0.95 FAIL
above 4 PASS
1.026
EvenOdd03_false-unreach-call_false-termination.c below duet 2 OKAY
0.931 PASS
above 4 OKAY
1.0
Fibonacci01_true-unreach-call.c below duet 7 FAIL
1.244 FAIL
above 4 FAIL
1.209
Fibonacci02_true-unreach-call_true-termination.c below duet 7 FAIL
1.239 FAIL
above 4 FAIL
1.133
Fibonacci03_true-unreach-call_true-termination.c below duet 7 FAIL
1.261 FAIL
above 4 FAIL
1.208
Fibonacci04_false-unreach-call_true-termination.c below duet 7 OKAY
1.245 PASS
above 4 OKAY
1.314
Fibonacci05_false-unreach-call_true-termination.c below duet 7 OKAY
1.259 PASS
above 4 OKAY
1.216
gcd01_true-unreach-call_true-termination.c below duet 2 PASS
1.005 FAIL
above 4 PASS
1.12
gcd02_true-unreach-call.c below duet 2 FAIL
PASS
1.235 FAIL
PASS
above 4 FAIL
PASS
1.478
McCarthy91_false-unreach-call_false-termination.c below duet 7 OKAY
1.098 PASS
above 4 OKAY
1.074
McCarthy91_true-unreach-call.c below duet 7 PASS
1.065 FAIL
above 4 FAIL
1.064
MultCommutative_true-unreach-call_true-termination.c below duet 2 FAIL
1.104 FAIL
above 4 FAIL
1.186
Primes_true-unreach-call.c below duet 3 FAIL
2.135 FAIL
above 4 FAIL
2.999
recHanoi01_true-unreach-call_true-termination.c below duet TIMEOUT
300.021 FAIL
above 4 FAIL
2.055
recHanoi02_true-unreach-call_true-termination.c below duet 2 FAIL
0.825 FAIL
above 4 FAIL
0.895
recHanoi03_true-unreach-call_true-termination.c below duet 2 FAIL
0.825 FAIL
above 4 FAIL
0.927
Total Below Time = 328.141 (was 328.207)
Above Time = 32.581 (was 32.298)
/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.78 PASS
FAIL
above 4 OKAY
UNSOUND
0.794
afterrec_2calls_true-unreach-call.c below duet 1 PASS
PASS
0.799 PASS
PASS
above 4 PASS
PASS
0.782
afterrec_false-unreach-call.c below duet 1 OKAY
0.681 PASS
above 4 OKAY
0.667
afterrec_true-unreach-call.c below duet 1 PASS
0.681 PASS
above 4 PASS
0.678
fibo_10_false-unreach-call.c below duet 7 OKAY
1.246 PASS
above 4 OKAY
1.069
fibo_10_true-unreach-call.c below duet 7 FAIL
1.233 FAIL
above 4 FAIL
1.172
fibo_15_false-unreach-call.c below duet 7 OKAY
1.235 PASS
above 4 OKAY
1.111
fibo_15_true-unreach-call.c below duet 7 FAIL
1.235 FAIL
above 4 FAIL
1.116
fibo_20_false-unreach-call.c below duet 7 OKAY
1.2 PASS
above 4 OKAY
1.076
fibo_20_true-unreach-call.c below duet 7 FAIL
1.247 FAIL
above 4 FAIL
1.12
fibo_25_false-unreach-call.c below duet 7 OKAY
1.226 PASS
above 4 OKAY
1.103
fibo_25_true-unreach-call.c below duet 7 FAIL
1.226 FAIL
above 4 FAIL
1.136
fibo_2calls_10_false-unreach-call.c below duet 8 OKAY
15.372 PASS
above 4 OKAY
43.029
fibo_2calls_10_true-unreach-call.c below duet 8 FAIL
15.327 FAIL
above 4 FAIL
44.48
fibo_2calls_15_false-unreach-call.c below duet 8 OKAY
15.157 PASS
above 4 OKAY
43.46
fibo_2calls_15_true-unreach-call.c below duet 8 FAIL
15.191 FAIL
above 4 FAIL
40.369
fibo_2calls_20_false-unreach-call.c below duet 8 OKAY
15.274 PASS
above 4 OKAY
43.265
fibo_2calls_20_true-unreach-call.c below duet 8 FAIL
15.147 FAIL
above 4 FAIL
43.31
fibo_2calls_25_false-unreach-call.c below duet 8 OKAY
15.245 PASS
above 4 OKAY
43.26
fibo_2calls_25_true-unreach-call.c below duet 8 FAIL
15.203 FAIL
above 4 FAIL
42.895
fibo_2calls_2_false-unreach-call.c below duet 8 OKAY
15.301 PASS
above 4 OKAY
41.691
fibo_2calls_2_true-unreach-call.c below duet 8 FAIL
15.275 FAIL
above 4 PASS
42.688
fibo_2calls_4_false-unreach-call.c below duet 8 OKAY
15.199 PASS
above 4 OKAY
40.863
fibo_2calls_4_true-unreach-call.c below duet 8 FAIL
15.303 FAIL
above 4 FAIL
42.036
fibo_2calls_5_false-unreach-call.c below duet 8 OKAY
15.146 PASS
above 4 OKAY
43.761
fibo_2calls_5_true-unreach-call.c below duet 8 FAIL
15.293 FAIL
above 4 FAIL
43.152
fibo_2calls_6_false-unreach-call.c below duet 8 OKAY
15.255 PASS
above 4 OKAY
43.638
fibo_2calls_6_true-unreach-call.c below duet 8 FAIL
15.155 FAIL
above 4 FAIL
40.768
fibo_2calls_8_false-unreach-call.c below duet 8 OKAY
15.246 PASS
above 4 OKAY
40.738
fibo_2calls_8_true-unreach-call.c below duet 8 FAIL
15.134 FAIL
above 4 FAIL
42.108
fibo_5_false-unreach-call.c below duet 7 OKAY
1.198 PASS
above 4 OKAY
1.174
fibo_5_true-unreach-call.c below duet 7 FAIL
1.227 FAIL
above 4 FAIL
1.111
fibo_7_false-unreach-call.c below duet 7 OKAY
1.233 PASS
above 4 OKAY
1.09
fibo_7_true-unreach-call.c below duet 7 FAIL
1.216 FAIL
above 4 FAIL
1.089
id2_b2_o3_true-unreach-call.c below duet 2 PASS
1.008 FAIL
above 4 PASS
1.231
id2_b3_o2_false-unreach-call.c below duet 2 OKAY
1.026 PASS
above 4 OKAY
1.243
id2_b3_o5_true-unreach-call.c below duet 2 PASS
1.006 FAIL
above 4 PASS
1.225
id2_b5_o10_true-unreach-call.c below duet 2 PASS
1.027 FAIL
above 4 PASS
1.248
id2_i5_o5_false-unreach-call.c below duet 2 OKAY
0.899 PASS
above 4 OKAY
0.965
id2_i5_o5_true-unreach-call.c below duet 2 PASS
0.874 PASS
above 4 PASS
0.944
id_b2_o3_true-unreach-call.c below duet 2 PASS
0.923 FAIL
above 4 PASS
1.093
id_b3_o2_false-unreach-call.c below duet 2 OKAY
0.898 PASS
above 4 OKAY
1.078
id_b3_o5_true-unreach-call.c below duet 2 PASS
0.937 FAIL
above 4 PASS
1.082
id_b5_o10_true-unreach-call.c below duet 2 PASS
0.922 FAIL
above 4 PASS
1.078
id_i10_o10_false-unreach-call.c below duet 2 OKAY
0.783 PASS
above 4 OKAY
0.852
id_i10_o10_true-unreach-call.c below duet 2 PASS
0.784 PASS
above 4 PASS
0.868
id_i15_o15_false-unreach-call.c below duet 2 OKAY
0.789 PASS
above 4 OKAY
0.845
id_i15_o15_true-unreach-call.c below duet 2 PASS
0.766 PASS
above 4 PASS
0.866
id_i20_o20_false-unreach-call.c below duet 2 OKAY
0.793 PASS
above 4 OKAY
0.855
id_i20_o20_true-unreach-call.c below duet 2 PASS
0.79 PASS
above 4 PASS
0.84
id_i25_o25_false-unreach-call.c below duet 2 OKAY
0.768 PASS
above 4 OKAY
0.853
id_i25_o25_true-unreach-call.c below duet 2 PASS
0.78 PASS
above 4 PASS
0.85
id_i5_o5_false-unreach-call.c below duet 2 OKAY
0.785 PASS
above 4 OKAY
0.863
id_i5_o5_true-unreach-call.c below duet 2 PASS
0.803 PASS
above 4 PASS
0.861
id_o1000_false-unreach-call.c below duet 2 OKAY
0.797 PASS
above 4 OKAY
0.854
id_o100_false-unreach-call.c below duet 2 OKAY
0.816 PASS
above 4 OKAY
0.846
id_o10_false-unreach-call.c below duet 2 OKAY
0.816 PASS
above 4 OKAY
0.843
id_o200_false-unreach-call.c below duet 2 OKAY
0.802 PASS
above 4 OKAY
0.874
id_o20_false-unreach-call.c below duet 2 OKAY
0.775 PASS
above 4 OKAY
0.85
id_o3_false-unreach-call.c below duet 2 OKAY
0.785 PASS
above 4 OKAY
0.833
sum_10x0_false-unreach-call.c below duet 2 OKAY
0.831 PASS
above 4 OKAY
0.912
sum_10x0_true-unreach-call.c below duet 2 PASS
0.805 PASS
above 4 PASS
0.912
sum_15x0_false-unreach-call.c below duet 2 OKAY
0.795 PASS
above 4 OKAY
0.888
sum_15x0_true-unreach-call.c below duet 2 PASS
0.809 PASS
above 4 PASS
0.878
sum_20x0_false-unreach-call.c below duet 2 OKAY
0.801 PASS
above 4 OKAY
0.887
sum_20x0_true-unreach-call.c below duet 2 PASS
0.814 PASS
above 4 PASS
0.889
sum_25x0_false-unreach-call.c below duet 2 OKAY
0.797 PASS
above 4 OKAY
0.899
sum_25x0_true-unreach-call.c below duet 2 PASS
0.772 PASS
above 4 PASS
0.881
sum_2x3_false-unreach-call.c below duet 2 OKAY
0.823 PASS
above 4 OKAY
0.877
sum_2x3_true-unreach-call.c below duet 2 PASS
0.819 PASS
above 4 PASS
0.874
sum_non_eq_false-unreach-call.c below duet 2 OKAY
0.802 PASS
above 4 OKAY
0.911
sum_non_eq_true-unreach-call.c below duet 2 PASS
0.808 PASS
above 4 PASS
0.875
sum_non_false-unreach-call.c below duet 2 OKAY
0.823 PASS
above 4 OKAY
0.877
sum_non_true-unreach-call.c below duet 2 PASS
0.809 PASS
above 4 PASS
0.875
Total Below Time = 325.346 (was 325.486)
Above Time = 819.074 (was 822.303)
/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.788 FAIL
above 4 PASS
0.863
rec-bhmr2007_true-unreach-call.c below duet 2 PASS
0.778 FAIL
above 4 PASS
0.878
rec-cggmp2005b_true-unreach-call.c below duet 3 PASS
1.233 FAIL
above 4 FAIL
1.78
rec-cggmp2005_true-unreach-call.c below duet 2 PASS
0.749 FAIL
above 4 PASS
0.821
rec-cggmp2005_variant_true-unreach-call.c below duet 2 PASS
0.787 FAIL
above 4 PASS
0.833
rec-css2003_true-unreach-call.c below duet 2 PASS
0.81 PASS
above 4 PASS
0.904
rec-ddlm2013_true-unreach-call.c below duet 2 FAIL
0.894 FAIL
above 4 FAIL
0.945
rec-gcnr2008_false-unreach-call.c below duet 2 OKAY
1.072 PASS
above 4 OKAY
1.184
rec-gj2007b_true-unreach-call.c below duet 2 FAIL
FAIL
0.794 FAIL
FAIL
above 4 FAIL
FAIL
0.89
rec-gj2007_true-unreach-call.c below duet 2 FAIL
0.81 FAIL
above 4 FAIL
0.894
rec-gr2006_true-unreach-call.c below duet 2 FAIL
0.804 FAIL
above 4 FAIL
0.865
rec-gsv2008_true-unreach-call.c below duet 2 PASS
0.772 FAIL
above 4 PASS
0.87
rec-hhk2008_true-unreach-call.c below duet 2 PASS
0.839 FAIL
above 4 PASS
0.92
rec-jm2006_true-unreach-call.c below duet 2 PASS
0.83 PASS
above 4 PASS
0.911
rec-jm2006_variant_true-unreach-call.c below duet 2 PASS
0.847 PASS
above 4 PASS
0.926
rec-mcmillan2006_true-unreach-call.c below duet 2 FAIL
0.975 FAIL
above 4 FAIL
1.035
Total Below Time = 13.782 (was 13.881)
Above Time = 15.519 (was 15.52)
/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.747 FAIL
above 4 PASS
0.811
rec-count_by_1_variant_true-unreach-call.c below duet 2 PASS
0.741 PASS
above 4 PASS
0.81
rec-count_by_2_true-unreach-call.c below duet 2 PASS
0.725 FAIL
above 4 PASS
0.798
rec-count_by_k_true-unreach-call.c below duet 2 FAIL
0.758 FAIL
above 4 FAIL
0.835
rec-count_by_nondet_true-unreach-call.c below duet 2 FAIL
0.77 FAIL
above 4 FAIL
0.832
rec-gauss_sum_true-unreach-call.c below duet 2 PASS
0.783 FAIL
above 4 PASS
0.891
rec-half_true-unreach-call.c below duet 2 FAIL
0.814 FAIL
above 4 FAIL
0.876
rec-nested_true-unreach-call.c below duet 3 PASS
1.034 FAIL
above 4 FAIL
1.186
Total Below Time = 6.372 (was 6.426)
Above Time = 7.039 (was 6.993)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below duet 2 PASS
0.865 FAIL
above 4 PASS
0.961
cubic_polynomial_unsafe.c below duet 2 OKAY
0.845 PASS
above 4 OKAY
1.004
edit_distance_bottom_up.c below duet 3 FAIL
4.53 FAIL
above 4 FAIL
9.733
edit_distance_top_down.c below duet 3 FAIL
3.489 FAIL
above 4 FAIL
42.263
log_log_n_solution.c below duet 3 FAIL
0.868 FAIL
above 4 FAIL
0.949
log_log_n_solution_unsafe.c below duet 3 OKAY
0.872 PASS
above 4 OKAY
0.936
log_n_solution.c below duet 2 FAIL
0.77 FAIL
above 4 FAIL
0.885
log_n_solution_unsafe.c below duet 2 OKAY
0.805 PASS
above 4 OKAY
0.887
multivariate_1.c below duet 4 FAIL
1.294 TIMEOUT
above 4 FAIL
1.73
multivariate_1_unsafe.c below duet 4 OKAY
1.282 TIMEOUT
above 4 OKAY
1.741
multivariate_higher_order.c below duet 7 FAIL
FAIL
FAIL
2.181 FAIL
FAIL
FAIL
above 4 FAIL
FAIL
FAIL
5.848
multivariate_higher_order_unsafe.c below duet 7 OKAY
OKAY
OKAY
2.176 PASS
PASS
PASS
above 4 OKAY
OKAY
OKAY
5.844
n_cubed_solution.c below duet TIMEOUT
300.045 FAIL
above 4 FAIL
1.599
n_cubed_solution_unsafe.c below duet TIMEOUT
300.029 PASS
above 4 OKAY
1.628
n_log_n_solution.c below duet 5 FAIL
1.015 FAIL
above 4 FAIL
1.172
n_log_n_solution_unsafe.c below duet 5 OKAY
1.036 PASS
above 4 OKAY
1.174
n_squared_two_base_case_even.c below duet 2 PASS
0.862 FAIL
above 4 PASS
0.968
n_squared_two_base_case_even_unsafe.c below duet 2 OKAY
0.827 PASS
above 4 OKAY
0.971
n_squared_two_base_case_odd.c below duet 2 PASS
0.832 FAIL
above 4 PASS
0.955
n_squared_two_base_case_odd_unsafe.c below duet 2 OKAY
0.849 PASS
above 4 OKAY
0.954
pascals_dynamic.c below duet 3 FAIL
1.592 FAIL
above 4 FAIL
2.445
pascals_dynamic_unsafe.c below duet 3 OKAY
1.564 PASS
above 4 OKAY
2.521
pascals_iterative.c below duet 1 FAIL
1.976 FAIL
above 4 FAIL
2.209
pascals_iterative_unsafe.c below duet 1 OKAY
1.953 PASS
above 4 OKAY
2.213
pascals_recursive.c below duet 9 FAIL
2.003 FAIL
above 4 FAIL
1.429
pascals_recursive_unsafe.c below duet 9 OKAY
2.03 PASS
above 4 OKAY
1.423
squared_solution.c below duet 4 FAIL
0.913 FAIL
above 4 FAIL
1.163
squared_solution_unsafe.c below duet 4 OKAY
0.961 PASS
above 4 OKAY
1.163
two_n_even.c below duet 2 PASS
0.794 PASS
above 4 PASS
0.885
two_n_even_unsafe.c below duet 2 OKAY
0.8 PASS
above 4 OKAY
0.879
two_n_odd.c below duet 2 PASS
0.805 PASS
above 4 PASS
0.861
two_n_odd_unsafe.c below duet 2 OKAY
0.813 PASS
above 4 OKAY
0.899
two_to_n_over_two_even.c below duet 7 FAIL
1.422 FAIL
above 4 FAIL
1.139
two_to_n_over_two_even_unsafe.c below duet 7 OKAY
1.446 PASS
above 4 OKAY
1.16
two_to_n_over_two_odd.c below duet 7 FAIL
1.432 FAIL
above 4 FAIL
1.11
two_to_n_over_two_odd_unsafe.c below duet 7 OKAY
1.392 PASS
above 4 OKAY
1.127
two_to_n_squared.c below duet 5 FAIL
8.445 FAIL
above 4 FAIL
3.805
two_to_n_squared_unsafe.c below duet 5 OKAY
8.36 PASS
above 4 OKAY
3.867
two_to_two_to_n.c below duet 7 FAIL
1.146 FAIL
above 4 FAIL
1.222
two_to_two_to_n_unsafe.c below duet 7 OKAY
1.169 PASS
above 4 OKAY
1.229
Total Below Time = 666.488 (was 666.364)
Above Time = 114.951 (was 113.869)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below duet 1 PASS
0.515 PASS
above 4 PASS
0.53
adding_and_mult_unsafe.c below duet 1 OKAY
0.475 PASS
above 4 OKAY
0.542
binary_search_array_tree.c below duet 1 FAIL
FAIL
1.233 FAIL
FAIL
above 4 FAIL
FAIL
1.406
exp_add_linear.c below duet 1 PASS
1.079 PASS
above 4 PASS
1.164
exp_add_linear_unsafe.c below duet 1 OKAY
1.128 PASS
above 4 OKAY
1.198
exp_add_loop_rec.c below duet 1 FAIL
0.924 FAIL
above 4 FAIL
1.007
exp_add_loop_rec_unsafe.c below duet 1 OKAY
0.956 PASS
above 4 OKAY
1.074
exp_add_loop_variable.c below duet 1 PASS
1.156 PASS
above 4 PASS
1.184
exp_add_loop_variable_unsafe.c below duet 1 OKAY
1.101 PASS
above 4 OKAY
1.167
exp_with_linear_inner_loop.c below duet 1 FAIL
1.547 FAIL
above 4 FAIL
1.705
exp_with_linear_inner_loop_unsafe.c below duet 1 OKAY
1.523 PASS
above 4 OKAY
1.691
halving_log1.c below duet 1 FAIL
0.968 FAIL
above 4 FAIL
1.084
linear_two_to_n.c below duet 7 FAIL
1.395 FAIL
above 4 FAIL
1.566
linear_two_to_n_unsafe.c below duet 7 OKAY
1.411 PASS
above 4 OKAY
1.628
loop_five_to_n.c below duet 1 PASS
0.993 PASS
above 4 PASS
1.066
loop_five_to_n_unsafe.c below duet 1 OKAY
0.974 PASS
above 4 OKAY
1.05
non_loop_five_to_n.c below duet 7 FAIL
2.138 FAIL
above 4 FAIL
3.044
non_loop_five_to_n_unsafe.c below duet 7 OKAY
2.089 PASS
above 4 OKAY
3.075
power_log_modified.c below duet 1 PASS
1.046 PASS
above 4 PASS
1.241
simple_exponential.c below duet 1 PASS
1.009 PASS
above 4 PASS
1.07
simple_exponential_for.c below duet 1 PASS
1.054 PASS
above 4 PASS
1.133
simple_exponential_for_unsafe.c below duet 1 OKAY
1.074 PASS
above 4 OKAY
1.13
simple_exponential_unsafe.c below duet 1 OKAY
0.988 PASS
above 4 OKAY
1.084
two_to_n_minus_n.c below duet 7 FAIL
1.545 FAIL
above 4 FAIL
1.764
two_to_n_minus_n_loop.c below duet 7 FAIL
1.863 FAIL
above 4 FAIL
1.898
two_to_n_minus_n_loop_unsafe.c below duet 7 OKAY
1.875 PASS
above 4 OKAY
1.89
two_to_n_minus_n_unsafe.c below duet 7 OKAY
1.571 PASS
above 4 OKAY
1.723
Total Below Time = 33.63 (was 33.472)
Above Time = 38.114 (was 38.102)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below duet 3 PASS
0.927 PASS
PASS
PASS
above 4 PASS
1.062
02.c below duet 3 FAIL
1.002 FAIL
PASS
PASS
above 4 FAIL
1.247
03.c below duet 1 PASS
1.316 PASS
PASS
above 4 PASS
1.413
04.c below duet 1 PASS
0.469 PASS
PASS
PASS
above 4 PASS
0.53
05.c below duet 3 PASS
1.166 PASS
PASS
PASS
above 4 PASS
1.479
06.c below duet 3 PASS
1.849 PASS
PASS
PASS
above 4 PASS
2.637
07.c below duet 3 PASS
0.979 PASS
PASS
PASS
above 4 PASS
1.112
08.c below duet 3 PASS
2.018 PASS
PASS
PASS
above 4 PASS
2.825
09.c below duet 3 PASS
1.735 PASS
PASS
PASS
above 4 PASS
2.185
10.c below duet 3 FAIL
1.129 FAIL
PASS
PASS
above 4 FAIL
1.53
11.c below duet 1 PASS
0.561 PASS
PASS
PASS
above 4 PASS
0.588
12.c below duet 3 PASS
1.502 PASS
PASS
PASS
above 4 PASS
1.915
13.c below duet 3 PASS
0.978 PASS
PASS
PASS
above 4 PASS
1.156
14.c below duet 3 PASS
PASS
1.005 PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.127
15.c below duet 1 PASS
0.863 PASS
PASS
PASS
above 4 PASS
0.915
16.c below duet 1 PASS
0.84 PASS
PASS
PASS
above 4 PASS
0.911
17.c below duet 1 PASS
1.335 PASS
PASS
PASS
above 4 PASS
1.478
18.c below duet 1 PASS
0.911 PASS
PASS
PASS
above 4 PASS
0.979
19.c below duet 1 PASS
0.934 PASS
PASS
PASS
above 4 PASS
1.002
20.c below duet 3 PASS
PASS
FAIL
1.185 PASS
PASS
FAIL
PASS
PASS
above 4 PASS
PASS
FAIL
1.374
21.c below duet 3 PASS
0.975 PASS
PASS
PASS
above 4 PASS
1.128
22.c below duet 3 PASS
PASS
1.15 PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.429
23.c below duet 1 PASS
0.833 PASS
PASS
PASS
above 4 PASS
0.9
24.c below duet 1 PASS
1.692 PASS
PASS
PASS
above 4 PASS
1.799
25.c below duet 3 PASS
1.664 PASS
PASS
PASS
above 4 PASS
2.122
26.c below duet 3 PASS
20.091 PASS
PASS
PASS
above 4 PASS
51.118
27.c below duet 1 PASS
1.343 PASS
PASS
PASS
above 4 PASS
1.424
28.c below duet 3 PASS
1.161 PASS
PASS
PASS
above 4 PASS
1.342
29.c below duet 3 PASS
2.253 PASS
PASS
PASS
above 4 PASS
2.787
30.c below duet 1 PASS
0.577 PASS
PASS
PASS
above 4 PASS
0.601
31.c below duet 3 PASS
PASS
3.146 PASS
PASS
PASS
PASS
above 4 PASS
PASS
4.069
32.c below duet 1 FAIL
0.892 FAIL
PASS
PASS
above 4 FAIL
0.962
33.c below duet 3 PASS
1.704 PASS
PASS
PASS
above 4 PASS
2.487
34.c below duet 1 FAIL
0.938 FAIL
PASS
PASS
above 4 FAIL
0.942
35.c below duet 1 PASS
0.838 PASS
PASS
PASS
above 4 PASS
0.864
36.c below duet 3 PASS
2.571 PASS
PASS
PASS
above 4 PASS
3.976
37.c below duet 3 FAIL
1.01 FAIL
PASS
PASS
above 4 FAIL
1.113
38.c below duet 1 FAIL
0.879 FAIL
PASS
PASS
above 4 FAIL
0.935
39.c below duet 3 PASS
PASS
1.068 PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.204
40.c below duet 3 PASS
1.263 PASS
PASS
PASS
above 4 PASS
1.602
41.c below duet 1 PASS
0.921 PASS
PASS
PASS
above 4 PASS
0.956
42.c below duet 3 PASS
1.14 PASS
PASS
PASS
above 4 PASS
1.49
43.c below duet 3 PASS
1.001 PASS
PASS
PASS
above 4 PASS
1.272
44.c below duet 1 PASS
0.868 PASS
PASS
PASS
above 4 PASS
0.926
45.c below duet 3 PASS
1.977 PASS
PASS
PASS
above 4 PASS
2.825
46.c below duet 3 PASS
1.582 PASS
PASS
PASS
above 4 PASS
2.433
Total Below Time = 76.241 (was 75.881)
Above Time = 120.171 (was 119.316)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below duet 1 PASS
0.983 PASS
PASS
PASS
above 4 PASS
1.061
AGHKTW2017_foo.c below duet 1 PASS
1.03 PASS
PASS
PASS
above 4 PASS
1.116
AGHKTW2017_loginSafe.c below duet 1 PASS
1.225 PASS
PASS
PASS
above 4 PASS
1.369
AGHKTW2017_loopAndBranch_safe.c below duet 1 PASS
1.07 PASS
PASS
PASS
above 4 PASS
1.158
AGHKTW2017_loopAndBranch_unsafe.c below duet 1 OKAY
1.038 PASS
FAIL
FAIL
above 4 OKAY
1.132
BCK2011_gauss.c below duet 1 PASS
0.779 PASS
PASS
PASS
above 4 PASS
0.848
BCK2011_strength_reduction.c below duet 1 PASS
1.098 PASS
PASS
PASS
above 4 PASS
1.201
BCK2011_strength_reduction_linear.c below duet 1 PASS
1.089 PASS
PASS
PASS
above 4 PASS
1.15
CFD17-add-const_product.c below duet 1 PASS
0.51 PASS
above 4 PASS
0.573
CFD17-add-const_product-syntax.c below duet 1 PASS
0.77 PASS
above 4 PASS
0.92
CFD17-add-const_self-comp.c below duet 1 FAIL
0.699 FAIL
above 4 FAIL
0.813
collatz_product-syntax.c below duet 1 FAIL
4.03 FAIL
above 4 FAIL
5.146
collatz_self-comp.c below duet 1 FAIL
1.384 FAIL
above 4 FAIL
1.669
fibonacci_information_flow.c below duet 1 PASS
1.097 PASS
PASS
PASS
above 4 PASS
1.227
halving_log1_product.c below duet 1 PASS
0.58 PASS
above 4 PASS
0.645
halving_log1_product-syntax.c below duet 1 FAIL
0.919 FAIL
above 4 FAIL
1.073
halving_log1_self-comp.c below duet 1 FAIL
0.767 FAIL
above 4 FAIL
0.895
loop_splitting_test_safe.c below duet 1 PASS
PASS
0.672 PASS
PASS
above 4 PASS
PASS
0.806
TA2005_fib2.c below duet 1 PASS
0.84 PASS
PASS
PASS
above 4 PASS
0.998
TA2005_fib.c below duet 1 PASS
0.618 PASS
PASS
PASS
above 4 PASS
0.713
top-level-if-add-const_product.c below duet 1 PASS
2.257 PASS
above 4 PASS
2.821
top-level-if-add-const_self-comp.c below duet 1 FAIL
1.144 FAIL
above 4 FAIL
1.268
Total Below Time = 24.599 (was 24.407)
Above Time = 28.602 (was 28.585)
/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.137 PASS
above 4 PASS
1.268
c3_cleanup_better.c below duet 3 PASS
PASS
2.434 PASS
PASS
above 4 PASS
PASS
2.966
c3_cleanup.c below duet 3 PASS
PASS
2.441 PASS
PASS
above 4 PASS
PASS
2.887
c3_intermediate.c below duet 3 PASS
PASS
PASS
2.355 PASS
PASS
PASS
above 4 PASS
PASS
PASS
2.823
c3_noinv.c below duet 3 FAIL
2.192 FAIL
above 4 FAIL
2.548
doublers.c below duet 1 FAIL
1.413 FAIL
above 4 FAIL
1.564
doublers_easier.c below duet 3 FAIL
1.739 FAIL
above 4 FAIL
2.291
doublers_easy.c below duet 1 FAIL
1.968 FAIL
above 4 FAIL
2.216
exp_mult.c below duet 1 FAIL
0.935 FAIL
above 4 FAIL
0.998
fig1_rotation_unsafe.c below duet EXCEPTION
0.312 PASS
above EXCEPTION
0.312
guessing_game.c below duet 3 FAIL
0.852 FAIL
above 4 FAIL
0.983
not_P_solvable.c below duet 1 PASS
0.488 PASS
above 4 PASS
0.519
Total Below Time = 18.266 (was 18.075)
Above Time = 21.375 (was 21.137)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below duet 1 PASS
PASS
PASS
FAIL
0.888 PASS
PASS
PASS
FAIL
above 4 PASS
PASS
PASS
FAIL
0.901
maxequals_linear_1.c below duet 1 PASS
0.881 PASS
above 4 PASS
0.986
maxequals_linear_2.c below duet 1 FAIL
0.92 FAIL
above 4 FAIL
1.058
maxequals_linear_3.c below duet 1 FAIL
0.843 FAIL
above 4 FAIL
0.905
maxequals_linear_4.c below duet 1 PASS
0.846 PASS
above 4 PASS
0.897
maxequals_linear_5.c below duet 1 PASS
0.869 PASS
above 4 PASS
0.891
maxequals_linear_6.c below duet 1 FAIL
0.841 FAIL
above 4 FAIL
0.898
maxequals_matrix1.c below duet 3 FAIL
1.403 FAIL
above 4 FAIL
2.005
maxequals_matrix2.c below duet 3 FAIL
1.589 FAIL
above 4 FAIL
2.002
maxequals_quadratic1.c below duet 1 FAIL
0.861 FAIL
above 4 FAIL
0.909
maxequals_quadratic2.c below duet 1 PASS
0.853 PASS
above 4 PASS
0.904
maxequals_stratified1.c below duet 3 PASS
3.313 PASS
above 4 PASS
4.474
maxequals_stratified2.c below duet 3 PASS
2.67 PASS
above 4 PASS
4.605
maxequals_stratified3.c below duet 3 FAIL
3.336 FAIL
above 4 FAIL
4.732
nine.c below duet 1 PASS
PASS
FAIL
0.838 PASS
PASS
FAIL
above 4 PASS
PASS
FAIL
0.904
nine_nondecreasing.c below duet 1 PASS
PASS
PASS
0.926 PASS
PASS
PASS
above 4 PASS
PASS
PASS
1.058
sum_interval_1.c below duet 1 FAIL
FAIL
0.801 FAIL
FAIL
above 4 FAIL
FAIL
0.887
sum_interval_2.c below duet 1 FAIL
FAIL
0.841 FAIL
FAIL
above 4 FAIL
FAIL
0.919
sum_interval_3.c below duet 1 FAIL
FAIL
0.805 FAIL
FAIL
above 4 FAIL
FAIL
0.888
TrackingObjectFields.c below duet TIMEOUT
300.014
above 4 124.433
TrackingObjectFields_inlined.c below duet 1 5.207
above 4 6.31
Total Below Time = 329.545 (was 329.215)
Above Time = 161.566 (was 160.664)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below duet 1 PASS
0.642 PASS
above 4 PASS
0.71
bobble2_varloop.c below duet 1 PASS
0.568 PASS
above 4 PASS
0.67
bobble3.c below duet 1 FAIL
0.545 FAIL
above 4 FAIL
0.602
bobble4.c below duet 1 PASS
0.641 PASS
above 4 PASS
0.714
bobble5.c below duet 1 PASS
0.645 PASS
above 4 PASS
0.721
bobble.c below duet 1 PASS
0.65 PASS
above 4 PASS
0.719
inchworm2.c below duet 1 FAIL
116.793 PASS
above 4 FAIL
120.118
inchworm3.c below duet 1 PASS
129.147 (90.349) PASS
above 4 PASS
96.818
inchworm4.c below duet 1 PASS
81.986 (119.766) PASS
above 4 PASS
114.018
inchworm5.c below duet 1 PASS
0.668 PASS
above 4 PASS
0.557
inchworm6_unsafe.c below duet 1 OKAY
0.565 PASS
above 4 OKAY
0.61
inchworm.c below duet 1 FAIL
118.05 FAIL
above 4 FAIL
119.649
leapdiff2.c below duet 1 PASS
0.79 PASS
above 4 PASS
0.665
leapfrog_annotated.c below duet 1 FAIL
0.605 FAIL
above 4 FAIL
0.653
leapfrog_annotated_disjunction.c below duet 1 PASS
0.647 PASS
above 4 PASS
0.699
leapfrog_asymmetric2.c below duet 1 FAIL
0.666 FAIL
above 4 FAIL
0.72
leapfrog_asymmetric3.c below duet 1 FAIL
0.613 FAIL
above 4 FAIL
0.668
leapfrog_asymmetric.c below duet 1 FAIL
0.55 FAIL
above 4 FAIL
0.602
leapfrog.c below duet 1 FAIL
0.537 FAIL
above 4 FAIL
0.59
leapfrog_materialized.c below duet 1 FAIL
0.625 FAIL
above 4 FAIL
0.683
leapfrog_verbose.c below duet 1 FAIL
0.674 FAIL
above 4 FAIL
0.764
leapspin.c below duet 1 PASS
0.492 PASS
above 4 PASS
0.544
leapsum2.c below duet 1 FAIL
0.529 FAIL
above 4 FAIL
0.586
leapthree.c below duet 1 FAIL
0.566 FAIL
above 4 FAIL
0.639
microbobble2.c below duet 1 PASS
0.517 PASS
above 4 PASS
0.581
microbobble3.c below duet 1 PASS
0.55 PASS
above 4 PASS
0.583
microbobble_asymmetric.c below duet 1 PASS
0.51 PASS
above 4 PASS
0.539
microbobble.c below duet 1 PASS
0.512 PASS
above 4 PASS
0.577
simple_bl2.c below duet 1 PASS
0.582 PASS
above 4 PASS
0.626
simple_bl3.c below duet 1 FAIL
0.561 FAIL
above 4 FAIL
0.63
simple_bl.c below duet 1 FAIL
0.557 FAIL
above 4 FAIL
0.588
Total Below Time = 461.983 (was 466.544)
Above Time = 467.843 (was 477.911)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below duet 1 PASS
PASS
0.794 PASS
PASS
above 4 PASS
PASS
0.807
binval_example_2_unsafe.c below duet 1 OKAY
0.745 PASS
above 4 OKAY
0.779
binval_example_3_unsafe.c below duet 1 OKAY
0.764 PASS
above 4 OKAY
0.756
binval_example_4.c below duet 1 PASS
PASS
PASS
0.78 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.796
binval_example_4_unsafe.c below duet 1 OKAY
0.708 PASS
above 4 OKAY
0.749
binval_example_5.c below duet 1 FAIL
FAIL
PASS
1.02 FAIL
FAIL
PASS
above 4 FAIL
FAIL
PASS
1.101
binval_example_5_unsafe.c below duet 1 OKAY
0.905 PASS
above 4 OKAY
1.056
Total Below Time = 5.716 (was 5.713)
Above Time = 6.044 (was 5.952)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/ethereum
array2_memory_contract.c below duet 1 1.631
above 4 1.73
array3_memory_contract.c below duet 1 1.628
above 4 2.072
array4_memory_contract.c below duet 1 1.94
above 4 2.188
arraylength_memory_contract.c below duet 1 0.774
above 4 0.805
array_memory_contract.c below duet 1 1.048
above 4 1.144
GovernMental.c below duet 1 28.326 (36.638)
above 4 38.919 (47.085)
HelloWorld.c below duet 1 0.627
above 4 0.625
linear2_memory_contract.c below duet 1 1.3
above 4 1.432
linear2_no_memory_contract.c below duet 1 1.213
above 4 1.394
linear3_no_memory_contract.c below duet 1 1.344
above 4 1.489
Linear.c below duet 1 1.002
above 4 1.08
linear_memory_contract.c below duet 1 0.998
above 4 1.099
linear_no_memory_contract.c below duet 1 0.978
above 4 1.089
nested2_memory_contract.c below duet 1 1.545
above 4 1.741
nested2_no_memory_contract.c below duet 1 1.583
above 4 1.817
nested_memory_contract.c below duet 1 1.471
above 4 1.629
nested_no_memory_contract.c below duet 1 1.38
above 4 1.561
Total Below Time = 48.788 (was 57.253)
Above Time = 61.814 (was 70.076)

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