[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.813 PASS
above 4 PASS
0.882
kmp.c below duet EXCEPTION
0.625
above EXCEPTION
0.643
qsort.c below duet 7 PASS
1.558 FAIL
above 4 FAIL
2.165
speed_pldi09_fig1.c below duet 1 PASS
0.941 PASS
above 4 PASS
1.075
speed_pldi09_fig4_2.c below duet 1 PASS
0.897 PASS
above 4 PASS
0.946
speed_pldi09_fig4_4.c below duet 1 PASS
0.869 PASS
above 4 PASS
0.989
speed_pldi09_fig4_5.c below duet 1 PASS
0.801 PASS
above 4 PASS
0.876
speed_pldi10_ex1.c below duet 1 PASS
1.866 PASS
above 4 PASS
2.688
speed_pldi10_ex3.c below duet 1 PASS
0.891 PASS
above 4 PASS
1.005
speed_pldi10_ex4.c below duet 1 PASS
0.929 PASS
above 4 PASS
1.055
speed_popl10_fig2_1.c below duet 1 PASS
0.797 PASS
above 4 PASS
0.909
speed_popl10_fig2_2.c below duet 1 FAIL
0.752 FAIL
above 4 FAIL
0.773
speed_popl10_nested_multiple.c below duet 1 PASS
0.863 PASS
above 4 PASS
1.036
speed_popl10_nested_single.c below duet 1 FAIL
1.053 FAIL
above 4 FAIL
1.176
speed_popl10_sequential_single.c below duet 1 PASS
0.891 PASS
above 4 PASS
0.955
speed_popl10_simple_multiple.c below duet 1 PASS
0.868 PASS
above 4 PASS
0.963
speed_popl10_simple_single_2.c below duet 1 PASS
1.009 PASS
above 4 PASS
1.19
speed_popl10_simple_single.c below duet 1 PASS
0.775 PASS
above 4 PASS
0.799
t07.c below duet 1 PASS
0.822 PASS
above 4 PASS
0.938
t08.c below duet 1 PASS
0.803 PASS
above 4 PASS
0.879
t09.c below duet 1 PASS
0.837 PASS
above 4 PASS
0.902
t10.c below duet 1 PASS
0.738 PASS
above 4 PASS
0.763
t11.c below duet 1 PASS
0.81 PASS
above 4 PASS
0.911
t13.c below duet 1 FAIL
0.851 FAIL
above 4 FAIL
0.898
t15.c below duet 1 PASS
0.787 PASS
above 4 PASS
0.902
t16.c below duet 1 PASS
0.895 PASS
above 4 PASS
0.971
t19.c below duet 1 PASS
0.768 PASS
above 4 PASS
0.83
t20.c below duet 1 PASS
0.788 PASS
above 4 PASS
0.84
t27.c below duet 1 PASS
0.831 PASS
above 4 PASS
0.985
t28.c below duet 1 PASS
0.889 PASS
above 4 PASS
0.983
t30.c below duet 1 FAIL
0.734 FAIL
above 4 FAIL
0.77
t37.c below duet 2 PASS
1.047 FAIL
above 4 PASS
1.137
t39.c below duet 2 PASS
0.941 FAIL
above 4 PASS
1.073
t46.c below duet 1 PASS
0.784 PASS
above 4 PASS
0.966
t47.c below duet 1 FAIL
0.787 FAIL
above 4 FAIL
0.858
Total Below Time = 31.31 (was 31.322)
Above Time = 35.731 (was 36.012)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below duet 2 PASS
PASS
0.814 PASS
PASS
above 4 PASS
PASS
0.881
qsort_full.c below duet 4 PASS
PASS
PASS
PASS
PASS
PASS
2.939 PASS
PASS
PASS
PASS
PASS
PASS
above 4 FAIL
PASS
PASS
PASS
PASS
PASS
4.551
rec1-param_safe.c below duet 2 PASS
PASS
PASS
0.8 PASS
FAIL
PASS
above 4 PASS
PASS
PASS
0.86
rec1-param_unsafe.c below duet 2 OKAY
0.77 PASS
above 4 OKAY
0.806
rec1_safe.c below duet 2 PASS
PASS
PASS
0.782 PASS
FAIL
PASS
above 4 PASS
PASS
PASS
0.833
rec1_unsafe.c below duet 2 OKAY
0.753 PASS
above 4 OKAY
0.8
rec2-param_safe.c below duet 2 PASS
PASS
PASS
0.8 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.873
rec2-param_unsafe.c below duet 2 OKAY
0.764 PASS
above 4 OKAY
0.806
rec2_safe.c below duet 2 PASS
PASS
PASS
0.778 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.852
rec2_unsafe.c below duet 2 OKAY
0.719 PASS
above 4 OKAY
0.768
rec-test.c below duet 2 PASS
0.723 FAIL
above 4 PASS
0.83
sas03_bothbranches.c below duet 7 PASS
1.059 PASS
above 4 FAIL
1.175
sas03.c below duet 2 PASS
1.115 PASS
above 4 PASS
1.25
simulated_lese_recursive.c below duet 2 PASS
0.78 PASS
above 4 PASS
0.833
Total Below Time = 13.596 (was 13.695)
Above Time = 16.118 (was 16.131)
/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.509
count_up_down_unsafe.c below duet 1 OKAY
0.474 PASS
above 4 OKAY
0.514
divide.c below duet 1 PASS
0.505 PASS
above 4 PASS
0.577
factor_unsafe.c below duet 1 OKAY
0.489 PASS
above 4 OKAY
0.532
for_infinite_loop_1_safe.c below duet 1 PASS
0.434 PASS
above 0 PASS
0.461
for_infinite_loop_2_safe.c below duet 1 PASS
0.436 PASS
above 0 PASS
0.46
interproc.c below duet 1 PASS
0.632 PASS
above 4 PASS
0.613
mult.c below duet 1 PASS
PASS
0.511 PASS
PASS
above 4 PASS
PASS
0.582
pointer_arith.c below duet 1 PASS
PASS
PASS
PASS
0.388 PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
0.393
quotient.c below duet 3 PASS
0.883 PASS
above 4 PASS
1.043
subtract.c below duet 1 PASS
0.402 PASS
above 4 PASS
0.449
sum01_bug02_sum01_bug02_base.case_unsafe.c below duet 1 OKAY
0.542 PASS
above 4 OKAY
0.574
sum01_bug02_unsafe.c below duet 1 OKAY
0.624 PASS
above 4 OKAY
0.746
sum01_real_safe.c below duet 1 PASS
0.511 PASS
above 4 PASS
0.54
sum01_safe.c below duet 1 PASS
0.507 PASS
above 4 PASS
0.541
sum01_unsafe.c below duet 1 OKAY
0.616 PASS
above 4 OKAY
0.709
sum02_safe.c below duet 1 PASS
0.51 PASS
above 4 PASS
0.537
sum03_safe.c below duet 1 PASS
0.473 PASS
above 0 PASS
0.519
sum03_unsafe.c below duet 1 OKAY
0.614 PASS
above 0 OKAY
0.718
sum04_safe.c below duet 1 PASS
0.507 PASS
above 4 PASS
0.556
sum04_unsafe.c below duet 1 OKAY
0.612 PASS
above 4 OKAY
0.689
terminator_02_safe.c below duet 1 PASS
0.425 PASS
above 4 PASS
0.428
terminator_02_unsafe.c below duet 1 OKAY
0.45 PASS
above 4 OKAY
0.469
terminator_03_safe.c below duet 1 PASS
0.428 PASS
above 4 PASS
0.462
terminator_03_unsafe.c below duet 1 OKAY
0.416 PASS
above 4 OKAY
0.467
token_ring01_safe.c below duet 4 FAIL
36.472 FAIL
above 4 FAIL
92.988
token_ring01_unsafe.c below duet 4 OKAY
52.101 PASS
above 4 OKAY
207.788
toy_safe.c below duet TIMEOUT
300.04 FAIL
above TIMEOUT
300.036
trex01_safe.c below duet 1 PASS
1.076 PASS
above 4 PASS
1.118
trex01_unsafe.c below duet 1 OKAY
1.031 PASS
above 4 OKAY
1.146
trex02_safe2.c below duet 3 PASS
0.853 PASS
above 4 PASS
0.965
trex02_safe.c below duet 3 PASS
0.771 PASS
above 4 PASS
0.879
trex02_unsafe.c below duet 3 OKAY
0.771 PASS
above 4 OKAY
0.877
trex03_safe.c below duet 1 PASS
0.527 PASS
above 4 PASS
0.626
trex03_unsafe.c below duet 1 OKAY
0.54 PASS
above 4 OKAY
0.585
trex04_safe.c below duet 1 PASS
0.765 PASS
above 4 PASS
0.819
while_infinite_loop_1_safe.c below duet 1 PASS
0.376 PASS
above 0 PASS
0.388
while_infinite_loop_2_safe.c below duet 1 PASS
0.387 PASS
above 0 PASS
0.395
while_infinite_loop_3_safe.c below duet 1 PASS
0.659 PASS
above 4 PASS
0.678
Total Below Time = 409.242 (was 411.406)
Above Time = 623.376 (was 625.624)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below duet 3 PASS
0.794 PASS
above 4 FAIL
0.916
blogger_simplified1.c below duet 3 PASS
1.712 PASS
above 4 PASS
2.362
divided_difference2.c below duet 3 PASS
PASS
PASS
3.785 PASS
PASS
PASS
above 4 PASS
PASS
PASS
4.28
mult-proc.c below duet 3 PASS
PASS
0.818 PASS
PASS
above 4 PASS
PASS
0.92
mult-proc-params.c below duet 3 PASS
PASS
0.856 PASS
PASS
above 4 PASS
PASS
0.995
popall.c below duet 1 PASS
PASS
PASS
PASS
PASS
0.911 PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
1.042
simulated_scc.c below duet 1 PASS
PASS
1.137 PASS
PASS
above 4 PASS
PASS
1.294
Total Below Time = 10.013 (was 10.02)
Above Time = 11.809 (was 11.858)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below duet 1 PASS
0.773 PASS
above 4 PASS
0.826
degree2_binomial.c below duet 1 PASS
1.225 PASS
above 4 PASS
1.505
degree2_monomial.c below duet 1 PASS
1.135 PASS
above 4 PASS
1.22
degree3_binomial.c below duet 1 PASS
2.318 PASS
above 4 PASS
2.958
degree3_monomial.c below duet 1 PASS
1.608 PASS
above 4 PASS
1.757
degree4_binomial.c below duet 1 PASS
4.326 PASS
above 4 PASS
5.91
degree4_monomial.c below duet 1 PASS
2.411 PASS
above 4 PASS
2.647
degree5_binomial.c below duet 1 PASS
11.912 PASS
above 4 PASS
19.173
degree5_monomial.c below duet 1 PASS
3.549 PASS
above 4 PASS
3.971
Total Below Time = 29.257 (was 29.505)
Above Time = 39.967 (was 39.955)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below duet 1 PASS
0.55 PASS
above 4 PASS
0.595
cubic_with_square_interproc.c below duet 2 PASS
0.82 FAIL
above 4 PASS
0.89
cubic_with_square_nonlinear.c below duet 1 PASS
0.522 PASS
above 4 PASS
0.565
cubic_with_square_nonlinear_interproc.c below duet 2 PASS
0.778 FAIL
above 4 PASS
0.879
cubic_with_square_nonlinear_unsafe.c below duet 1 OKAY
0.534 PASS
above 4 OKAY
0.589
cubic_with_square_unsafe.c below duet 1 OKAY
0.576 PASS
above 4 OKAY
0.608
multi-input.c below duet 1 PASS
0.725 PASS
above 4 PASS
0.887
multi-input_unsafe.c below duet 1 OKAY
0.748 PASS
above 4 OKAY
0.903
nondet_loop_bound.c below duet 1 PASS
0.513 PASS
above 4 PASS
0.556
nondet_loop_bound_quartic.c below duet 1 PASS
0.54 PASS
above 4 PASS
0.588
nondet_loop_bound_quartic_unsafe.c below duet 1 OKAY
0.535 PASS
above 4 OKAY
0.594
nondet_loop_bound_unsafe.c below duet 1 OKAY
0.539 PASS
above 4 OKAY
0.544
nonlinear_stratified.c below duet 1 PASS
189.724 PASS
above 4 PASS
189.938
nonlinear_stratified_unsafe.c below duet 1 TIMEOUT
300.005 TIMEOUT
above 4 TIMEOUT
300.007
quartic_with_cube.c below duet 1 PASS
0.566 PASS
above 4 PASS
0.66
quartic_with_cube_nonlinear.c below duet 1 PASS
0.571 PASS
above 4 PASS
0.638
quartic_with_cube_nonlinear_unsafe.c below duet 1 OKAY
0.587 PASS
above 4 OKAY
0.645
quartic_with_cube_unsafe.c below duet 1 OKAY
0.515 PASS
above 4 OKAY
0.534
quintic_with_quartic.c below duet 1 PASS
0.671 PASS
above 4 PASS
0.826
quintic_with_quartic_nonlinear.c below duet 1 PASS
0.756 PASS
above 4 PASS
0.844
quintic_with_quartic_nonlinear_unsafe.c below duet 1 OKAY
0.733 PASS
above 4 OKAY
0.915
quintic_with_quartic_unsafe.c below duet 1 OKAY
0.682 PASS
above 4 OKAY
0.838
Total Below Time = 502.19 (was 503.418)
Above Time = 504.043 (was 504.03)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below duet 1 PASS
1.374 PASS
above 4 PASS
2.013
degree2_FD_AllAux_AllAssm.c below duet 1 PASS
5.125 PASS
above 4 PASS
9.113
degree2_FD_AllAux_FewAssm.c below duet 1 PASS
4.997 PASS
above 4 PASS
8.695
degree2_FD_FewAux_FewAssm.c below duet 1 PASS
1.899 PASS
above 4 PASS
3.092
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below duet 1 PASS
1.841 PASS
above 4 PASS
2.99
degree3.c below duet 1 PASS
1.614 PASS
above 4 PASS
2.515
degree3_FD.c below duet 1 PASS
1.905 PASS
above 4 PASS
3.003
degree4.c below duet 1 PASS
1.365 PASS
above 4 PASS
1.527
Total Below Time = 20.12 (was 20.29)
Above Time = 32.948 (was 33.075)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below duet EXCEPTION
0.316
above EXCEPTION
0.324
loop_unsafe.c below duet EXCEPTION
0.336
above EXCEPTION
0.321
simulated_lese_parser.c below duet 1 PASS
0.777 PASS
above 4 PASS
0.862
simulated_lese_sentinel.c below duet 1 PASS
0.781 PASS
above 4 PASS
0.797
Total Below Time = 2.21 (was 2.227)
Above Time = 2.304 (was 2.34)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below duet 1 PASS
PASS
PASS
0.614 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.651
Total Below Time = 0.614 (was 0.616)
Above Time = 0.651 (was 0.632)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below duet TIMEOUT
300.021 TIMEOUT
above TIMEOUT
300.015
Total Below Time = 300.021 (was 300.019)
Above Time = 300.015 (was 300.014)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below duet 1 OKAY
0.516 PASS
above 4 OKAY
0.555
array_false-unreach-call2.c below duet 1 OKAY
0.521 PASS
above 4 OKAY
0.55
array_false-unreach-call3.c below duet 1 OKAY
0.609 PASS
above 4 OKAY
0.659
array_true-unreach-call1.c below duet 1 FAIL
0.521 FAIL
above 4 FAIL
0.553
array_true-unreach-call2.c below duet 1 FAIL
0.508 FAIL
above 4 FAIL
0.59
array_true-unreach-call3.c below duet 1 PASS
0.545 PASS
above 4 PASS
0.576
array_true-unreach-call4.c below duet 1 FAIL
0.542 FAIL
above 4 FAIL
0.54
const_false-unreach-call1.c below duet 1 OKAY
0.501 PASS
above 4 OKAY
0.528
const_true-unreach-call1.c below duet 1 PASS
0.498 PASS
above 4 PASS
0.566
diamond_false-unreach-call1.c below duet 1 OKAY
0.526 PASS
above 4 OKAY
0.545
diamond_true-unreach-call1.c below duet 1 PASS
0.541 PASS
above 4 PASS
0.576
diamond_true-unreach-call2.c below duet 1 PASS
0.551 PASS
above 4 PASS
0.628
functions_false-unreach-call1.c below duet 3 OKAY
0.776 PASS
above 4 OKAY
0.916
functions_true-unreach-call1.c below duet 3 PASS
0.79 PASS
above 4 PASS
0.921
multivar_false-unreach-call1.c below duet 1 OKAY
0.395 PASS
above 4 OKAY
0.443
multivar_true-unreach-call1.c below duet 1 PASS
0.409 PASS
above 4 PASS
0.429
nested_false-unreach-call1.c below duet 1 OKAY
0.825 PASS
above 4 OKAY
0.905
nested_true-unreach-call1.c below duet 1 PASS
0.839 PASS
above 4 PASS
0.874
overflow_true-unreach-call1.c below duet 1 PASS
0.451 PASS
above 4 PASS
0.513
phases_false-unreach-call1.c below duet 1 OKAY
0.591 PASS
above 4 OKAY
0.669
phases_false-unreach-call2.c below duet 1 OKAY
0.589 PASS
above 4 OKAY
0.662
phases_true-unreach-call1.c below duet 1 PASS
0.598 PASS
above 4 PASS
0.659
phases_true-unreach-call2.c below duet 1 FAIL
0.598 FAIL
above 4 FAIL
0.661
simple_false-unreach-call1.c below duet 1 OKAY
0.484 PASS
above 4 OKAY
0.511
simple_false-unreach-call2.c below duet 1 OKAY
0.403 PASS
above 4 OKAY
0.433
simple_false-unreach-call3.c below duet 1 OKAY
0.472 PASS
above 4 OKAY
0.506
simple_false-unreach-call4.c below duet 1 OKAY
0.5 PASS
above 4 OKAY
0.525
simple_true-unreach-call1.c below duet 1 PASS
0.495 PASS
above 4 PASS
0.515
simple_true-unreach-call2.c below duet 1 PASS
0.382 PASS
above 4 PASS
0.423
simple_true-unreach-call3.c below duet 1 PASS
0.48 PASS
above 4 PASS
0.5
simple_true-unreach-call4.c below duet 1 PASS
0.492 PASS
above 4 PASS
0.527
underapprox_false-unreach-call1.c below duet 1 OKAY
0.506 PASS
above 4 OKAY
0.542
underapprox_false-unreach-call2.c below duet 1 OKAY
0.497 PASS
above 4 OKAY
0.533
underapprox_true-unreach-call1.c below duet 1 PASS
0.518 PASS
above 4 PASS
0.557
underapprox_true-unreach-call2.c below duet 1 PASS
0.51 PASS
above 4 PASS
0.545
Total Below Time = 18.979 (was 19.046)
Above Time = 20.635 (was 20.449)
/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.682 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.871
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.17 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.297
down_true-unreach-call.c below duet 1 PASS
0.539 PASS
above 4 PASS
0.608
fragtest_simple_true-unreach-call.c below duet 1 PASS
0.996 PASS
above 4 PASS
1.101
half_2_true-unreach-call.c below duet 1 PASS
0.713 PASS
above 4 PASS
0.773
heapsort_true-unreach-call.c below duet 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
5.91 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.155
id_build_true-unreach-call.c below duet 1 PASS
PASS
0.981 PASS
PASS
above 4 PASS
PASS
1.04
id_trans_false-unreach-call.c below duet 1 OKAY
0.64 PASS
above 4 OKAY
0.698
id_trans_true-unreach-call.c below duet 1 PASS
PASS
PASS
0.693 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.774
large_const_true-unreach-call.c below duet 1 PASS
0.662 PASS
above 4 PASS
0.766
MADWiFi-encode_ie_ok_true-unreach-call.c below duet 1 PASS
PASS
0.826 PASS
PASS
above 4 PASS
PASS
0.875
nested6_true-unreach-call.c below duet 1 PASS
PASS
PASS
2.038 PASS
PASS
PASS
above 4 PASS
PASS
PASS
2.168
nested9_true-unreach-call.c below duet 1 PASS
3.209 PASS
above 4 PASS
3.455
nest-if3_true-unreach-call.c below duet 1 PASS
0.84 PASS
above 4 PASS
0.968
NetBSD_loop_true-unreach-call.c below duet 1 PASS
PASS
0.624 PASS
PASS
above 4 PASS
PASS
0.673
sendmail-close-angle_true-unreach-call.c below duet 1 PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
1.006 PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
above 4 PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
1.069
seq_true-unreach-call.c below duet 1 PASS
0.988 PASS
above 4 PASS
1.108
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.951 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.909
string_concat-noarr_true-unreach-call.c below duet 1 PASS
1.082 PASS
above 4 PASS
1.165
up_true-unreach-call.c below duet 1 PASS
0.653 PASS
above 4 PASS
0.741
Total Below Time = 32.203 (was 32.075)
Above Time = 41.214 (was 41.499)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below duet 1 PASS
0.593 PASS
above 4 PASS
0.638
bhmr2007_true-unreach-call.c below duet 1 PASS
0.54 PASS
above 4 PASS
0.572
cggmp2005b_true-unreach-call.c below duet 1 PASS
1.108 PASS
above 4 PASS
1.233
cggmp2005_true-unreach-call.c below duet 1 PASS
0.483 PASS
above 4 PASS
0.521
cggmp2005_variant_true-unreach-call.c below duet 1 PASS
0.514 PASS
above 4 PASS
0.553
css2003_true-unreach-call.c below duet 1 PASS
0.641 PASS
above 4 PASS
0.707
ddlm2013_true-unreach-call.c below duet 1 PASS
0.637 PASS
above 4 PASS
0.741
gcnr2008_false-unreach-call.c below duet 1 OKAY
1.095 PASS
above 4 OKAY
1.297
gj2007b_true-unreach-call.c below duet 1 PASS
FAIL
0.533 PASS
FAIL
above 4 PASS
FAIL
0.57
gj2007_true-unreach-call.c below duet 1 PASS
0.598 PASS
above 4 PASS
0.68
gr2006_true-unreach-call.c below duet 1 PASS
0.588 PASS
above 4 PASS
0.689
gsv2008_true-unreach-call.c below duet 1 PASS
0.514 PASS
above 4 PASS
0.529
hhk2008_true-unreach-call.c below duet 1 PASS
0.553 PASS
above 4 PASS
0.545
jm2006_true-unreach-call.c below duet 1 PASS
0.546 PASS
above 4 PASS
0.546
jm2006_variant_true-unreach-call.c below duet 1 PASS
0.555 PASS
above 4 PASS
0.601
mcmillan2006_true-unreach-call.c below duet 1 FAIL
0.721 FAIL
above 4 FAIL
0.795
Total Below Time = 10.219 (was 10.068)
Above Time = 11.217 (was 11.183)
/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.484 PASS
above 4 PASS
0.519
count_by_1_variant_true-unreach-call.c below duet 1 PASS
0.512 PASS
above 4 PASS
0.533
count_by_2_true-unreach-call.c below duet 1 PASS
0.501 PASS
above 4 PASS
0.534
count_by_k_true-unreach-call.c below duet 1 PASS
0.501 PASS
above 4 PASS
0.543
count_by_nondet_true-unreach-call.c below duet 1 FAIL
0.535 FAIL
above 4 FAIL
0.588
gauss_sum_true-unreach-call.c below duet 1 PASS
0.516 PASS
above 4 PASS
0.531
half_true-unreach-call.c below duet 1 FAIL
0.54 FAIL
above 4 FAIL
0.592
nested_true-unreach-call.c below duet 1 PASS
0.976 PASS
above 4 PASS
1.111
Total Below Time = 4.565 (was 4.576)
Above Time = 4.951 (was 4.951)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below duet 1 OKAY
0.479 PASS
above 4 OKAY
0.509
array_true-unreach-call.c below duet 1 FAIL
0.473 FAIL
above 4 FAIL
0.509
bubble_sort_false-unreach-call.c below duet 4 OKAY
UNSOUND
3.66 PASS
FAIL
above 4 OKAY
UNSOUND
16.126
bubble_sort_true-unreach-call.c below duet 1 2.17
above 4 2.362
compact_false-unreach-call.c below duet EXCEPTION
0.322
above EXCEPTION
0.311
count_up_down_false-unreach-call_true-termination.c below duet 1 OKAY
0.487 PASS
above 4 OKAY
0.518
count_up_down_true-unreach-call_true-termination.c below duet 1 PASS
0.49 PASS
above 4 PASS
0.494 (0.551)
eureka_01_false-unreach-call.c below duet EXCEPTION
0.341
above EXCEPTION
0.341
eureka_01_true-unreach-call.c below duet EXCEPTION
0.332
above EXCEPTION
0.334
eureka_05_true-unreach-call.c below duet EXCEPTION
0.624
above EXCEPTION
0.621
for_bounded_loop1_false-unreach-call_true-termination.c below duet 1 OKAY
0.532 (0.47) PASS
above 4 OKAY
0.519
for_bounded_loop1_true-unreach-call_true-termination.c below duet 1 PASS
PASS
0.579 PASS
PASS
above 4 PASS
PASS
0.614
for_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.434 PASS
above 0 PASS
0.462
for_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.443 PASS
above 0 PASS
0.472
heavy_false-unreach-call.c below duet 1 OKAY
1.531 PASS
above 4 OKAY
1.673
heavy_true-unreach-call.c below duet 1 PASS
1.505 PASS
above 4 PASS
1.655
insertion_sort_false-unreach-call.c below duet 1 OKAY
1.294 PASS
above 4 OKAY
1.502
insertion_sort_true-unreach-call.c below duet 1 FAIL
1.063 FAIL
above 4 FAIL
1.145
invert_string_false-unreach-call.c below duet 1 OKAY
0.85 PASS
above 4 OKAY
0.971
invert_string_true-unreach-call.c below duet 1 FAIL
1.001 FAIL
above 4 FAIL
1.099
linear_sea.ch_true-unreach-call.c below duet 1 FAIL
0.892 FAIL
above 4 FAIL
0.944
linear_search_false-unreach-call.c below duet 1 OKAY
0.907 PASS
above 4 OKAY
0.953
lu.cmp_true-unreach-call.c below duet 3 PASS
8.017 PASS
above 4 PASS
10.752
ludcmp_false-unreach-call.c below duet 3 OKAY
7.376 PASS
above 4 OKAY
10.196
matrix_false-unreach-call_true-termination.c below duet 1 OKAY
1.395 PASS
above 4 OKAY
1.508
matrix_true-unreach-call_true-termination.c below duet 1 FAIL
0.592 FAIL
above 4 FAIL
0.683
n.c11_true-unreach-call.c below duet EXCEPTION
0.603
above EXCEPTION
0.603
n.c24_false-unreach-call.c below duet EXCEPTION
0.633
above EXCEPTION
0.64
n.c40_true-unreach-call.c below duet EXCEPTION
0.318
above EXCEPTION
0.304
nec11_false-unreach-call.c below duet EXCEPTION
0.589
above EXCEPTION
0.607
nec20_false-unreach-call.c below duet EXCEPTION
0.617
above EXCEPTION
0.615
nec40_true-unreach-call.c below duet EXCEPTION
0.321
above EXCEPTION
0.322
string_false-unreach-call.c below duet 1 OKAY
1.518 PASS
above 4 OKAY
1.682
string_true-unreach-call.c below duet 1 FAIL
1.475 FAIL
above 4 FAIL
1.658
sum01_bug02_false-unreach-call_true-termination.c below duet 1 OKAY
0.661 PASS
above 4 OKAY
0.805
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below duet 1 OKAY
0.538 PASS
above 4 OKAY
0.56
sum01_false-unreach-call_true-termination.c below duet 1 OKAY
0.599 PASS
above 4 OKAY
0.685
sum01_true-unreach-call_true-termination.c below duet 1 PASS
0.529 PASS
above 4 PASS
0.573
sum03_false-unreach-call_true-termination.c below duet 1 OKAY
0.602 PASS
above 0 OKAY
0.707
sum03_true-unreach-call_false-termination.c below duet 1 PASS
0.54 PASS
above 4 PASS
0.61
sum04_false-unreach-call_true-termination.c below duet 1 OKAY
0.591 PASS
above 4 OKAY
0.685
sum04_true-unreach-call_true-termination.c below duet 1 PASS
0.529 PASS
above 4 PASS
0.541
sum_array_false-unreach-call.c below duet 1 OKAY
0.962 PASS
above 4 OKAY
1.073
sum_array_true-unreach-call.c below duet 1 FAIL
0.966 FAIL
above 4 FAIL
1.073
terminator_01_false-unreach-call_false-termination.c below duet 1 OKAY
0.383 PASS
above 4 OKAY
0.42
terminator_02_false-unreach-call_true-termination.c below duet 1 OKAY
0.719 PASS
above 4 OKAY
0.712
terminator_02_true-unreach-call_true-termination.c below duet 2 PASS
0.742 PASS
above 4 PASS
0.844
terminator_03_false-unreach-call_true-termination.c below duet 1 OKAY
0.428 PASS
above 4 OKAY
0.458
terminator_03_true-unreach-call_true-termination.c below duet 1 PASS
0.432 PASS
above 4 PASS
0.472
trex01_false-unreach-call_true-termination.c below duet 3 OKAY
1.284 PASS
above 4 OKAY
1.465
trex01_true-unreach-call.c below duet 3 PASS
1.443 PASS
above 4 PASS
1.723
trex02_false-unreach-call_true-termination.c below duet 3 OKAY
0.782 PASS
above 4 OKAY
0.917
trex02_true-unreach-call_true-termination.c below duet 3 PASS
0.767 PASS
above 4 PASS
0.897
trex03_false-unreach-call_true-termination.c below duet 3 OKAY
0.917 PASS
above 4 OKAY
1.139
trex03_true-unreach-call.c below duet 3 PASS
0.92 PASS
above 4 PASS
1.144
trex04_true-unreach-call_false-termination.c below duet 1 PASS
0.907 PASS
above 4 PASS
1.024
veris.c_NetBSD-libc__loop_true-unreach-call.c below duet 1 PASS
0.718 PASS
above 4 PASS
0.743
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below duet EXCEPTION
0.641
above EXCEPTION
0.628
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below duet 1 PASS
0.539 PASS
above 4 PASS
0.579
verisec_NetBSD-libc__loop_false-unreach-call.c below duet 1 OKAY
0.74 PASS
above 4 OKAY
0.763
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below duet EXCEPTION
0.65
above EXCEPTION
0.636
vogal_false-unreach-call.c below duet 1 OKAY
2.136 PASS
above 4 OKAY
2.303
vogal_true-unreach-call.c below duet 1 FAIL
1.927 FAIL
above 4 FAIL
2.091
while_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.372 PASS
above 0 PASS
0.394
while_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.368 PASS
above 0 PASS
0.384
while_infinite_loop_3_true-unreach-call_false-termination.c below duet 1 PASS
0.657 PASS
above 4 PASS
0.666
while_infinite_loop_4_false-unreach-call_true-termination.c below duet 1 OKAY
0.65 PASS
above 4 OKAY
0.669
Total Below Time = 69.502 (was 69.656)
Above Time = 92.087 (was 92.775)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below duet 7 PASS
1.419 FAIL
above 4 FAIL
1.528
Ackermann02_false-unreach-call_false-termination.c below duet 7 OKAY
1.342 PASS
above 4 OKAY
1.526
Ackermann03_true-unreach-call.c below duet 7 FAIL
1.413 FAIL
above 4 FAIL
1.542
Ackermann04_true-unreach-call.c below duet 7 FAIL
1.405 FAIL
above 4 FAIL
1.541
Addition01_true-unreach-call_true-termination.c below duet 2 PASS
1.113 PASS
above 4 PASS
1.238
Addition02_false-unreach-call_false-termination.c below duet 2 OKAY
1.019 PASS
above 4 OKAY
1.124
Addition03_false-no-overflow.c below duet 2 PASS
1.06 PASS
above 4 PASS
1.184
Addition03_true-unreach-call.c below duet 2 PASS
1.074 PASS
above 4 PASS
1.134
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below duet 2 OKAY
0.828 PASS
above 4 OKAY
0.941
EvenOdd01_true-unreach-call_true-termination.c below duet 2 PASS
0.97 FAIL
above 4 PASS
1.005
EvenOdd03_false-unreach-call_false-termination.c below duet 2 OKAY
0.933 PASS
above 4 OKAY
1.033
Fibonacci01_true-unreach-call.c below duet 7 FAIL
1.3 FAIL
above 4 FAIL
1.194
Fibonacci02_true-unreach-call_true-termination.c below duet 7 FAIL
1.253 FAIL
above 4 FAIL
1.111
Fibonacci03_true-unreach-call_true-termination.c below duet 7 FAIL
1.273 FAIL
above 4 FAIL
1.209
Fibonacci04_false-unreach-call_true-termination.c below duet 7 OKAY
1.252 PASS
above 4 OKAY
1.333
Fibonacci05_false-unreach-call_true-termination.c below duet 7 OKAY
1.234 PASS
above 4 OKAY
1.162
gcd01_true-unreach-call_true-termination.c below duet 2 PASS
1.007 FAIL
above 4 PASS
1.166
gcd02_true-unreach-call.c below duet 2 FAIL
PASS
1.24 FAIL
PASS
above 4 FAIL
PASS
1.403
McCarthy91_false-unreach-call_false-termination.c below duet 7 OKAY
1.107 PASS
above 4 OKAY
1.091
McCarthy91_true-unreach-call.c below duet 7 PASS
1.088 FAIL
above 4 FAIL
1.054
MultCommutative_true-unreach-call_true-termination.c below duet 2 FAIL
1.067 FAIL
above 4 FAIL
1.217
Primes_true-unreach-call.c below duet 3 FAIL
2.136 FAIL
above 4 FAIL
2.872
recHanoi01_true-unreach-call_true-termination.c below duet TIMEOUT
300.026 FAIL
above 4 FAIL
1.984
recHanoi02_true-unreach-call_true-termination.c below duet 2 FAIL
0.799 FAIL
above 4 FAIL
0.888
recHanoi03_true-unreach-call_true-termination.c below duet 2 FAIL
0.805 FAIL
above 4 FAIL
0.891
Total Below Time = 328.163 (was 328.087)
Above Time = 32.371 (was 32.217)
/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.795 PASS
FAIL
above 4 OKAY
UNSOUND
0.809
afterrec_2calls_true-unreach-call.c below duet 1 PASS
PASS
0.781 PASS
PASS
above 4 PASS
PASS
0.803
afterrec_false-unreach-call.c below duet 1 OKAY
0.726 PASS
above 4 OKAY
0.704
afterrec_true-unreach-call.c below duet 1 PASS
0.692 PASS
above 4 PASS
0.676
fibo_10_false-unreach-call.c below duet 7 OKAY
1.247 PASS
above 4 OKAY
1.12
fibo_10_true-unreach-call.c below duet 7 FAIL
1.237 FAIL
above 4 FAIL
1.208
fibo_15_false-unreach-call.c below duet 7 OKAY
1.267 PASS
above 4 OKAY
1.112
fibo_15_true-unreach-call.c below duet 7 FAIL
1.228 FAIL
above 4 FAIL
1.124
fibo_20_false-unreach-call.c below duet 7 OKAY
1.236 PASS
above 4 OKAY
1.108
fibo_20_true-unreach-call.c below duet 7 FAIL
1.195 FAIL
above 4 FAIL
1.105
fibo_25_false-unreach-call.c below duet 7 OKAY
1.211 PASS
above 4 OKAY
1.112
fibo_25_true-unreach-call.c below duet 7 FAIL
1.204 FAIL
above 4 FAIL
1.093
fibo_2calls_10_false-unreach-call.c below duet 8 OKAY
15.248 PASS
above 4 OKAY
43.69
fibo_2calls_10_true-unreach-call.c below duet 8 FAIL
15.223 FAIL
above 4 FAIL
43.336
fibo_2calls_15_false-unreach-call.c below duet 8 OKAY
15.204 PASS
above 4 OKAY
43.104
fibo_2calls_15_true-unreach-call.c below duet 8 FAIL
15.211 FAIL
above 4 FAIL
40.206
fibo_2calls_20_false-unreach-call.c below duet 8 OKAY
15.29 PASS
above 4 OKAY
43.161
fibo_2calls_20_true-unreach-call.c below duet 8 FAIL
15.255 FAIL
above 4 FAIL
43.741
fibo_2calls_25_false-unreach-call.c below duet 8 OKAY
15.13 PASS
above 4 OKAY
43.743
fibo_2calls_25_true-unreach-call.c below duet 8 FAIL
15.257 FAIL
above 4 FAIL
42.38
fibo_2calls_2_false-unreach-call.c below duet 8 OKAY
15.148 PASS
above 4 OKAY
41.314
fibo_2calls_2_true-unreach-call.c below duet 8 FAIL
15.212 FAIL
above 4 PASS
42.53
fibo_2calls_4_false-unreach-call.c below duet 8 OKAY
15.101 PASS
above 4 OKAY
40.973
fibo_2calls_4_true-unreach-call.c below duet 8 FAIL
15.312 FAIL
above 4 FAIL
43.313
fibo_2calls_5_false-unreach-call.c below duet 8 OKAY
15.166 PASS
above 4 OKAY
42.844
fibo_2calls_5_true-unreach-call.c below duet 8 FAIL
15.276 FAIL
above 4 FAIL
41.761
fibo_2calls_6_false-unreach-call.c below duet 8 OKAY
15.185 PASS
above 4 OKAY
43.091
fibo_2calls_6_true-unreach-call.c below duet 8 FAIL
15.185 FAIL
above 4 FAIL
40.807
fibo_2calls_8_false-unreach-call.c below duet 8 OKAY
15.264 PASS
above 4 OKAY
42.828
fibo_2calls_8_true-unreach-call.c below duet 8 FAIL
15.352 FAIL
above 4 FAIL
41.886
fibo_5_false-unreach-call.c below duet 7 OKAY
1.212 PASS
above 4 OKAY
1.127
fibo_5_true-unreach-call.c below duet 7 FAIL
1.258 FAIL
above 4 FAIL
1.133
fibo_7_false-unreach-call.c below duet 7 OKAY
1.21 PASS
above 4 OKAY
1.098
fibo_7_true-unreach-call.c below duet 7 FAIL
1.231 FAIL
above 4 FAIL
1.104
id2_b2_o3_true-unreach-call.c below duet 2 PASS
0.983 FAIL
above 4 PASS
1.198
id2_b3_o2_false-unreach-call.c below duet 2 OKAY
0.994 PASS
above 4 OKAY
1.246
id2_b3_o5_true-unreach-call.c below duet 2 PASS
1.016 FAIL
above 4 PASS
1.216
id2_b5_o10_true-unreach-call.c below duet 2 PASS
1.025 FAIL
above 4 PASS
1.256
id2_i5_o5_false-unreach-call.c below duet 2 OKAY
0.904 PASS
above 4 OKAY
0.955
id2_i5_o5_true-unreach-call.c below duet 2 PASS
0.894 PASS
above 4 PASS
0.965
id_b2_o3_true-unreach-call.c below duet 2 PASS
0.895 FAIL
above 4 PASS
1.048
id_b3_o2_false-unreach-call.c below duet 2 OKAY
0.901 PASS
above 4 OKAY
1.11
id_b3_o5_true-unreach-call.c below duet 2 PASS
0.893 FAIL
above 4 PASS
1.068
id_b5_o10_true-unreach-call.c below duet 2 PASS
0.923 FAIL
above 4 PASS
1.08
id_i10_o10_false-unreach-call.c below duet 2 OKAY
0.785 PASS
above 4 OKAY
0.862
id_i10_o10_true-unreach-call.c below duet 2 PASS
0.79 PASS
above 4 PASS
0.86
id_i15_o15_false-unreach-call.c below duet 2 OKAY
0.78 PASS
above 4 OKAY
0.846
id_i15_o15_true-unreach-call.c below duet 2 PASS
0.79 PASS
above 4 PASS
0.838
id_i20_o20_false-unreach-call.c below duet 2 OKAY
0.776 PASS
above 4 OKAY
0.864
id_i20_o20_true-unreach-call.c below duet 2 PASS
0.792 PASS
above 4 PASS
0.828
id_i25_o25_false-unreach-call.c below duet 2 OKAY
0.771 PASS
above 4 OKAY
0.852
id_i25_o25_true-unreach-call.c below duet 2 PASS
0.794 PASS
above 4 PASS
0.872
id_i5_o5_false-unreach-call.c below duet 2 OKAY
0.818 PASS
above 4 OKAY
0.859
id_i5_o5_true-unreach-call.c below duet 2 PASS
0.81 PASS
above 4 PASS
0.864
id_o1000_false-unreach-call.c below duet 2 OKAY
0.776 PASS
above 4 OKAY
0.839
id_o100_false-unreach-call.c below duet 2 OKAY
0.781 PASS
above 4 OKAY
0.837
id_o10_false-unreach-call.c below duet 2 OKAY
0.792 PASS
above 4 OKAY
0.852
id_o200_false-unreach-call.c below duet 2 OKAY
0.765 PASS
above 4 OKAY
0.848
id_o20_false-unreach-call.c below duet 2 OKAY
0.784 PASS
above 4 OKAY
0.835
id_o3_false-unreach-call.c below duet 2 OKAY
0.787 PASS
above 4 OKAY
0.841
sum_10x0_false-unreach-call.c below duet 2 OKAY
0.815 PASS
above 4 OKAY
0.893
sum_10x0_true-unreach-call.c below duet 2 PASS
0.87 PASS
above 4 PASS
0.883
sum_15x0_false-unreach-call.c below duet 2 OKAY
0.817 PASS
above 4 OKAY
0.9
sum_15x0_true-unreach-call.c below duet 2 PASS
0.822 PASS
above 4 PASS
0.885
sum_20x0_false-unreach-call.c below duet 2 OKAY
0.796 PASS
above 4 OKAY
0.86
sum_20x0_true-unreach-call.c below duet 2 PASS
0.856 PASS
above 4 PASS
0.877
sum_25x0_false-unreach-call.c below duet 2 OKAY
0.805 PASS
above 4 OKAY
0.904
sum_25x0_true-unreach-call.c below duet 2 PASS
0.81 PASS
above 4 PASS
0.865
sum_2x3_false-unreach-call.c below duet 2 OKAY
0.83 PASS
above 4 OKAY
0.867
sum_2x3_true-unreach-call.c below duet 2 PASS
0.803 PASS
above 4 PASS
0.878
sum_non_eq_false-unreach-call.c below duet 2 OKAY
0.794 PASS
above 4 OKAY
0.883
sum_non_eq_true-unreach-call.c below duet 2 PASS
0.842 PASS
above 4 PASS
0.891
sum_non_false-unreach-call.c below duet 2 OKAY
0.799 PASS
above 4 OKAY
0.893
sum_non_true-unreach-call.c below duet 2 PASS
0.825 PASS
above 4 PASS
0.865
Total Below Time = 325.252 (was 326.066)
Above Time = 818.227 (was 818.305)
/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.801 FAIL
above 4 PASS
0.889
rec-bhmr2007_true-unreach-call.c below duet 2 PASS
0.785 FAIL
above 4 PASS
0.845
rec-cggmp2005b_true-unreach-call.c below duet 3 PASS
1.208 FAIL
above 4 FAIL
1.785
rec-cggmp2005_true-unreach-call.c below duet 2 PASS
0.745 FAIL
above 4 PASS
0.835
rec-cggmp2005_variant_true-unreach-call.c below duet 2 PASS
0.779 FAIL
above 4 PASS
0.849
rec-css2003_true-unreach-call.c below duet 2 PASS
0.83 PASS
above 4 PASS
0.919
rec-ddlm2013_true-unreach-call.c below duet 2 FAIL
0.865 FAIL
above 4 FAIL
0.985
rec-gcnr2008_false-unreach-call.c below duet 2 OKAY
1.052 PASS
above 4 OKAY
1.188
rec-gj2007b_true-unreach-call.c below duet 2 FAIL
FAIL
0.812 FAIL
FAIL
above 4 FAIL
FAIL
0.929
rec-gj2007_true-unreach-call.c below duet 2 FAIL
0.855 FAIL
above 4 FAIL
0.906
rec-gr2006_true-unreach-call.c below duet 2 FAIL
0.818 FAIL
above 4 FAIL
0.889
rec-gsv2008_true-unreach-call.c below duet 2 PASS
0.79 FAIL
above 4 PASS
0.854
rec-hhk2008_true-unreach-call.c below duet 2 PASS
0.842 FAIL
above 4 PASS
0.935
rec-jm2006_true-unreach-call.c below duet 2 PASS
0.844 PASS
above 4 PASS
0.869
rec-jm2006_variant_true-unreach-call.c below duet 2 PASS
0.86 PASS
above 4 PASS
0.952
rec-mcmillan2006_true-unreach-call.c below duet 2 FAIL
0.964 FAIL
above 4 FAIL
1.035
Total Below Time = 13.85 (was 13.906)
Above Time = 15.664 (was 15.59)
/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.808 FAIL
above 4 PASS
0.8
rec-count_by_1_variant_true-unreach-call.c below duet 2 PASS
0.754 PASS
above 4 PASS
0.813
rec-count_by_2_true-unreach-call.c below duet 2 PASS
0.742 FAIL
above 4 PASS
0.797
rec-count_by_k_true-unreach-call.c below duet 2 FAIL
0.756 FAIL
above 4 FAIL
0.858
rec-count_by_nondet_true-unreach-call.c below duet 2 FAIL
0.784 FAIL
above 4 FAIL
0.83
rec-gauss_sum_true-unreach-call.c below duet 2 PASS
0.784 FAIL
above 4 PASS
0.88
rec-half_true-unreach-call.c below duet 2 FAIL
0.798 FAIL
above 4 FAIL
0.902
rec-nested_true-unreach-call.c below duet 3 PASS
1.046 FAIL
above 4 FAIL
1.184
Total Below Time = 6.472 (was 6.393)
Above Time = 7.064 (was 6.981)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below duet 2 PASS
0.871 FAIL
above 4 PASS
0.995
cubic_polynomial_unsafe.c below duet 2 OKAY
0.852 PASS
above 4 OKAY
0.963
edit_distance_bottom_up.c below duet 3 FAIL
4.304 FAIL
above 4 FAIL
9.488
edit_distance_top_down.c below duet 3 FAIL
3.513 FAIL
above 4 FAIL
40.902
log_log_n_solution.c below duet 3 FAIL
0.856 FAIL
above 4 FAIL
0.969
log_log_n_solution_unsafe.c below duet 3 OKAY
0.849 PASS
above 4 OKAY
0.945
log_n_solution.c below duet 2 FAIL
0.795 FAIL
above 4 FAIL
0.863
log_n_solution_unsafe.c below duet 2 OKAY
0.789 PASS
above 4 OKAY
0.857
multivariate_1.c below duet 4 FAIL
1.31 TIMEOUT
above 4 FAIL
1.743
multivariate_1_unsafe.c below duet 4 OKAY
1.337 TIMEOUT
above 4 OKAY
1.715
multivariate_higher_order.c below duet 7 FAIL
FAIL
FAIL
2.131 FAIL
FAIL
FAIL
above 4 FAIL
FAIL
FAIL
5.967
multivariate_higher_order_unsafe.c below duet 7 OKAY
OKAY
OKAY
2.221 PASS
PASS
PASS
above 4 OKAY
OKAY
OKAY
5.853
n_cubed_solution.c below duet TIMEOUT
300.044 FAIL
above 4 FAIL
1.613
n_cubed_solution_unsafe.c below duet TIMEOUT
300.027 PASS
above 4 OKAY
1.599
n_log_n_solution.c below duet 5 FAIL
1.001 FAIL
above 4 FAIL
1.179
n_log_n_solution_unsafe.c below duet 5 OKAY
1.016 PASS
above 4 OKAY
1.157
n_squared_two_base_case_even.c below duet 2 PASS
0.83 FAIL
above 4 PASS
0.97
n_squared_two_base_case_even_unsafe.c below duet 2 OKAY
0.856 PASS
above 4 OKAY
0.968
n_squared_two_base_case_odd.c below duet 2 PASS
0.85 FAIL
above 4 PASS
0.948
n_squared_two_base_case_odd_unsafe.c below duet 2 OKAY
0.838 PASS
above 4 OKAY
0.946
pascals_dynamic.c below duet 3 FAIL
1.585 FAIL
above 4 FAIL
2.442
pascals_dynamic_unsafe.c below duet 3 OKAY
1.562 PASS
above 4 OKAY
2.428
pascals_iterative.c below duet 1 FAIL
1.911 FAIL
above 4 FAIL
2.243
pascals_iterative_unsafe.c below duet 1 OKAY
1.909 PASS
above 4 OKAY
2.205
pascals_recursive.c below duet 9 FAIL
2.087 FAIL
above 4 FAIL
1.385
pascals_recursive_unsafe.c below duet 9 OKAY
2.042 PASS
above 4 OKAY
1.404
squared_solution.c below duet 4 FAIL
0.924 FAIL
above 4 FAIL
1.151
squared_solution_unsafe.c below duet 4 OKAY
0.951 PASS
above 4 OKAY
1.128
two_n_even.c below duet 2 PASS
0.808 PASS
above 4 PASS
0.869
two_n_even_unsafe.c below duet 2 OKAY
0.782 PASS
above 4 OKAY
0.873
two_n_odd.c below duet 2 PASS
0.802 PASS
above 4 PASS
0.897
two_n_odd_unsafe.c below duet 2 OKAY
0.802 PASS
above 4 OKAY
0.891
two_to_n_over_two_even.c below duet 7 FAIL
1.461 FAIL
above 4 FAIL
1.11
two_to_n_over_two_even_unsafe.c below duet 7 OKAY
1.401 PASS
above 4 OKAY
1.123
two_to_n_over_two_odd.c below duet 7 FAIL
1.429 FAIL
above 4 FAIL
1.145
two_to_n_over_two_odd_unsafe.c below duet 7 OKAY
1.484 PASS
above 4 OKAY
1.107
two_to_n_squared.c below duet 5 FAIL
8.368 FAIL
above 4 FAIL
3.879
two_to_n_squared_unsafe.c below duet 5 OKAY
8.457 PASS
above 4 OKAY
3.807
two_to_two_to_n.c below duet 7 FAIL
1.163 FAIL
above 4 FAIL
1.213
two_to_two_to_n_unsafe.c below duet 7 OKAY
1.178 PASS
above 4 OKAY
1.241
Total Below Time = 666.396 (was 665.954)
Above Time = 113.181 (was 115.008)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below duet 1 PASS
0.491 PASS
above 4 PASS
0.525
adding_and_mult_unsafe.c below duet 1 OKAY
0.501 PASS
above 4 OKAY
0.526
binary_search_array_tree.c below duet 1 FAIL
FAIL
1.235 FAIL
FAIL
above 4 FAIL
FAIL
1.393
exp_add_linear.c below duet 1 PASS
1.085 PASS
above 4 PASS
1.188
exp_add_linear_unsafe.c below duet 1 OKAY
1.1 PASS
above 4 OKAY
1.181
exp_add_loop_rec.c below duet 1 FAIL
0.965 FAIL
above 4 FAIL
0.979
exp_add_loop_rec_unsafe.c below duet 1 OKAY
0.945 PASS
above 4 OKAY
1.004
exp_add_loop_variable.c below duet 1 PASS
1.088 PASS
above 4 PASS
1.258
exp_add_loop_variable_unsafe.c below duet 1 OKAY
1.183 (1.041) PASS
above 4 OKAY
1.187
exp_with_linear_inner_loop.c below duet 1 FAIL
1.514 FAIL
above 4 FAIL
1.66
exp_with_linear_inner_loop_unsafe.c below duet 1 OKAY
1.529 PASS
above 4 OKAY
1.65
halving_log1.c below duet 1 FAIL
0.988 FAIL
above 4 FAIL
1.128
linear_two_to_n.c below duet 7 FAIL
1.36 FAIL
above 4 FAIL
1.558
linear_two_to_n_unsafe.c below duet 7 OKAY
1.365 PASS
above 4 OKAY
1.599
loop_five_to_n.c below duet 1 PASS
0.982 PASS
above 4 PASS
1.039
loop_five_to_n_unsafe.c below duet 1 OKAY
0.967 PASS
above 4 OKAY
1.069
non_loop_five_to_n.c below duet 7 FAIL
2.106 FAIL
above 4 FAIL
3.035
non_loop_five_to_n_unsafe.c below duet 7 OKAY
2.088 PASS
above 4 OKAY
3.026
power_log_modified.c below duet 1 PASS
1.079 PASS
above 4 PASS
1.212
simple_exponential.c below duet 1 PASS
0.961 PASS
above 4 PASS
1.063
simple_exponential_for.c below duet 1 PASS
1.028 PASS
above 4 PASS
1.125
simple_exponential_for_unsafe.c below duet 1 OKAY
1.043 PASS
above 4 OKAY
1.145
simple_exponential_unsafe.c below duet 1 OKAY
0.994 PASS
above 4 OKAY
1.044
two_to_n_minus_n.c below duet 7 FAIL
1.58 FAIL
above 4 FAIL
1.758
two_to_n_minus_n_loop.c below duet 7 FAIL
1.85 FAIL
above 4 FAIL
1.891
two_to_n_minus_n_loop_unsafe.c below duet 7 OKAY
1.85 PASS
above 4 OKAY
1.915
two_to_n_minus_n_unsafe.c below duet 7 OKAY
1.569 PASS
above 4 OKAY
1.725
Total Below Time = 33.446 (was 33.372)
Above Time = 37.883 (was 37.946)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below duet 3 PASS
0.935 PASS
PASS
PASS
above 4 PASS
1.063
02.c below duet 3 FAIL
1.025 FAIL
PASS
PASS
above 4 FAIL
1.209
03.c below duet 1 PASS
1.295 PASS
PASS
above 4 PASS
1.415
04.c below duet 1 PASS
0.476 PASS
PASS
PASS
above 4 PASS
0.505
05.c below duet 3 PASS
1.158 PASS
PASS
PASS
above 4 PASS
1.445
06.c below duet 3 PASS
1.82 PASS
PASS
PASS
above 4 PASS
2.717
07.c below duet 3 PASS
0.996 PASS
PASS
PASS
above 4 PASS
1.108
08.c below duet 3 PASS
2.002 PASS
PASS
PASS
above 4 PASS
2.769
09.c below duet 3 PASS
1.749 PASS
PASS
PASS
above 4 PASS
2.156
10.c below duet 3 FAIL
1.124 FAIL
PASS
PASS
above 4 FAIL
1.505
11.c below duet 1 PASS
0.558 PASS
PASS
PASS
above 4 PASS
0.611
12.c below duet 3 PASS
1.543 PASS
PASS
PASS
above 4 PASS
1.932
13.c below duet 3 PASS
0.998 PASS
PASS
PASS
above 4 PASS
1.127
14.c below duet 3 PASS
PASS
0.996 PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.11
15.c below duet 1 PASS
0.876 PASS
PASS
PASS
above 4 PASS
0.898
16.c below duet 1 PASS
0.811 PASS
PASS
PASS
above 4 PASS
0.91
17.c below duet 1 PASS
1.333 PASS
PASS
PASS
above 4 PASS
1.459
18.c below duet 1 PASS
0.915 PASS
PASS
PASS
above 4 PASS
0.949
19.c below duet 1 PASS
0.912 PASS
PASS
PASS
above 4 PASS
1.029
20.c below duet 3 PASS
PASS
FAIL
1.209 PASS
PASS
FAIL
PASS
PASS
above 4 PASS
PASS
FAIL
1.386
21.c below duet 3 PASS
0.989 PASS
PASS
PASS
above 4 PASS
1.123
22.c below duet 3 PASS
PASS
1.156 PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.379
23.c below duet 1 PASS
0.847 PASS
PASS
PASS
above 4 PASS
0.876
24.c below duet 1 PASS
1.65 PASS
PASS
PASS
above 4 PASS
1.769
25.c below duet 3 PASS
1.702 PASS
PASS
PASS
above 4 PASS
2.073
26.c below duet 3 PASS
20.148 PASS
PASS
PASS
above 4 PASS
51.524
27.c below duet 1 PASS
1.306 PASS
PASS
PASS
above 4 PASS
1.465
28.c below duet 3 PASS
1.147 PASS
PASS
PASS
above 4 PASS
1.289
29.c below duet 3 PASS
2.33 PASS
PASS
PASS
above 4 PASS
2.795
30.c below duet 1 PASS
0.555 (0.625) PASS
PASS
PASS
above 4 PASS
0.596 (0.675)
31.c below duet 3 PASS
PASS
3.204 PASS
PASS
PASS
PASS
above 4 PASS
PASS
3.92
32.c below duet 1 FAIL
0.909 FAIL
PASS
PASS
above 4 FAIL
0.918
33.c below duet 3 PASS
1.715 PASS
PASS
PASS
above 4 PASS
2.529
34.c below duet 1 FAIL
0.889 FAIL
PASS
PASS
above 4 FAIL
0.981
35.c below duet 1 PASS
0.825 PASS
PASS
PASS
above 4 PASS
0.892
36.c below duet 3 PASS
2.532 PASS
PASS
PASS
above 4 PASS
3.999
37.c below duet 3 FAIL
0.994 FAIL
PASS
PASS
above 4 FAIL
1.132
38.c below duet 1 FAIL
0.87 FAIL
PASS
PASS
above 4 FAIL
0.92
39.c below duet 3 PASS
PASS
1.095 PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.205
40.c below duet 3 PASS
1.235 PASS
PASS
PASS
above 4 PASS
1.577
41.c below duet 1 PASS
0.914 PASS
PASS
PASS
above 4 PASS
0.968
42.c below duet 3 PASS
1.113 PASS
PASS
PASS
above 4 PASS
1.438
43.c below duet 3 PASS
0.974 PASS
PASS
PASS
above 4 PASS
1.271
44.c below duet 1 PASS
0.85 PASS
PASS
PASS
above 4 PASS
0.919
45.c below duet 3 PASS
1.928 PASS
PASS
PASS
above 4 PASS
2.718
46.c below duet 3 PASS
1.569 PASS
PASS
PASS
above 4 PASS
2.289
Total Below Time = 76.177 (was 76.145)
Above Time = 119.868 (was 119.994)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below duet 1 PASS
0.981 PASS
PASS
PASS
above 4 PASS
1.068
AGHKTW2017_foo.c below duet 1 PASS
1.079 PASS
PASS
PASS
above 4 PASS
1.089
AGHKTW2017_loginSafe.c below duet 1 PASS
1.186 PASS
PASS
PASS
above 4 PASS
1.314
AGHKTW2017_loopAndBranch_safe.c below duet 1 PASS
1.014 PASS
PASS
PASS
above 4 PASS
1.133
AGHKTW2017_loopAndBranch_unsafe.c below duet 1 OKAY
1.064 PASS
FAIL
FAIL
above 4 OKAY
1.123
BCK2011_gauss.c below duet 1 PASS
0.765 PASS
PASS
PASS
above 4 PASS
0.847
BCK2011_strength_reduction.c below duet 1 PASS
1.089 PASS
PASS
PASS
above 4 PASS
1.191
BCK2011_strength_reduction_linear.c below duet 1 PASS
1.065 PASS
PASS
PASS
above 4 PASS
1.158
CFD17-add-const_product.c below duet 1 PASS
0.505 PASS
above 4 PASS
0.548
CFD17-add-const_product-syntax.c below duet 1 PASS
0.779 PASS
above 4 PASS
0.913
CFD17-add-const_self-comp.c below duet 1 FAIL
0.743 FAIL
above 4 FAIL
0.796
collatz_product-syntax.c below duet 1 FAIL
3.933 FAIL
above 4 FAIL
5.238
collatz_self-comp.c below duet 1 FAIL
1.391 FAIL
above 4 FAIL
1.686
fibonacci_information_flow.c below duet 1 PASS
1.074 PASS
PASS
PASS
above 4 PASS
1.191
halving_log1_product.c below duet 1 PASS
0.588 PASS
above 4 PASS
0.631
halving_log1_product-syntax.c below duet 1 FAIL
0.897 FAIL
above 4 FAIL
1.063
halving_log1_self-comp.c below duet 1 FAIL
0.756 FAIL
above 4 FAIL
0.839
loop_splitting_test_safe.c below duet 1 PASS
PASS
0.676 PASS
PASS
above 4 PASS
PASS
0.83
TA2005_fib2.c below duet 1 PASS
0.837 PASS
PASS
PASS
above 4 PASS
1.001
TA2005_fib.c below duet 1 PASS
0.618 PASS
PASS
PASS
above 4 PASS
0.696
top-level-if-add-const_product.c below duet 1 PASS
2.281 PASS
above 4 PASS
2.873
top-level-if-add-const_self-comp.c below duet 1 FAIL
1.112 FAIL
above 4 FAIL
1.314
Total Below Time = 24.433 (was 24.46)
Above Time = 28.542 (was 28.577)
/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.125 PASS
above 4 PASS
1.284
c3_cleanup_better.c below duet 3 PASS
PASS
2.467 PASS
PASS
above 4 PASS
PASS
2.925
c3_cleanup.c below duet 3 PASS
PASS
2.428 PASS
PASS
above 4 PASS
PASS
2.917
c3_intermediate.c below duet 3 PASS
PASS
PASS
2.291 PASS
PASS
PASS
above 4 PASS
PASS
PASS
2.748
c3_noinv.c below duet 3 FAIL
2.125 FAIL
above 4 FAIL
2.585
doublers.c below duet 1 FAIL
1.443 FAIL
above 4 FAIL
1.514
doublers_easier.c below duet 3 FAIL
1.768 FAIL
above 4 FAIL
2.235
doublers_easy.c below duet 1 FAIL
2.036 FAIL
above 4 FAIL
2.182
exp_mult.c below duet 1 FAIL
0.94 FAIL
above 4 FAIL
1.002
fig1_rotation_unsafe.c below duet EXCEPTION
0.307 PASS
above EXCEPTION
0.313 (0.596)
guessing_game.c below duet 3 FAIL
0.835 FAIL
above 4 FAIL
0.986
not_P_solvable.c below duet 1 PASS
0.491 PASS
above 4 PASS
0.532
Total Below Time = 18.256 (was 18.087)
Above Time = 21.223 (was 21.488)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below duet 1 PASS
PASS
PASS
FAIL
0.845 PASS
PASS
PASS
FAIL
above 4 PASS
PASS
PASS
FAIL
0.877
maxequals_linear_1.c below duet 1 PASS
0.85 PASS
above 4 PASS
0.977
maxequals_linear_2.c below duet 1 FAIL
0.881 FAIL
above 4 FAIL
1.016
maxequals_linear_3.c below duet 1 FAIL
0.877 FAIL
above 4 FAIL
0.886
maxequals_linear_4.c below duet 1 PASS
0.852 PASS
above 4 PASS
0.899
maxequals_linear_5.c below duet 1 PASS
0.846 PASS
above 4 PASS
0.887
maxequals_linear_6.c below duet 1 FAIL
0.884 FAIL
above 4 FAIL
0.916
maxequals_matrix1.c below duet 3 FAIL
1.424 FAIL
above 4 FAIL
1.986
maxequals_matrix2.c below duet 3 FAIL
1.594 FAIL
above 4 FAIL
1.998
maxequals_quadratic1.c below duet 1 FAIL
0.87 FAIL
above 4 FAIL
0.905
maxequals_quadratic2.c below duet 1 PASS
0.859 PASS
above 4 PASS
0.907
maxequals_stratified1.c below duet 3 PASS
3.2 PASS
above 4 PASS
4.505
maxequals_stratified2.c below duet 3 PASS
2.659 PASS
above 4 PASS
4.689
maxequals_stratified3.c below duet 3 FAIL
3.316 FAIL
above 4 FAIL
4.645
nine.c below duet 1 PASS
PASS
FAIL
0.828 PASS
PASS
FAIL
above 4 PASS
PASS
FAIL
0.889
nine_nondecreasing.c below duet 1 PASS
PASS
PASS
0.932 PASS
PASS
PASS
above 4 PASS
PASS
PASS
1.053
sum_interval_1.c below duet 1 FAIL
FAIL
0.795 FAIL
FAIL
above 4 FAIL
FAIL
0.887
sum_interval_2.c below duet 1 FAIL
FAIL
0.835 FAIL
FAIL
above 4 FAIL
FAIL
0.933
sum_interval_3.c below duet 1 FAIL
FAIL
0.792 FAIL
FAIL
above 4 FAIL
FAIL
0.883
TrackingObjectFields.c below duet TIMEOUT
300.017
above 4 126.234
TrackingObjectFields_inlined.c below duet 1 5.14
above 4 6.354
Total Below Time = 329.296 (was 329.259)
Above Time = 163.326 (was 161.389)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below duet 1 PASS
0.65 PASS
above 4 PASS
0.727
bobble2_varloop.c below duet 1 PASS
0.576 PASS
above 4 PASS
0.654
bobble3.c below duet 1 FAIL
0.556 FAIL
above 4 FAIL
0.618
bobble4.c below duet 1 PASS
0.646 PASS
above 4 PASS
0.723
bobble5.c below duet 1 PASS
0.652 PASS
above 4 PASS
0.732
bobble.c below duet 1 PASS
0.641 PASS
above 4 PASS
0.74
inchworm2.c below duet 1 FAIL
122.637 (110.913) FAIL
above EXCEPTION
119.577 (71.084)
inchworm3.c below duet 1 PASS
113.938
above 4 PASS
86.833 (77.724)
inchworm4.c below duet 1 PASS
111.415 (137.928) PASS
above 4 PASS
120.88 (135.575)
inchworm5.c below duet 1 PASS
0.697 PASS
above 4 PASS
0.539
inchworm6_unsafe.c below duet 1 OKAY
0.545 PASS
above 4 OKAY
0.615
inchworm.c below duet 1 FAIL
133.01 FAIL
above 4 FAIL
119.784
leapdiff2.c below duet 1 PASS
0.878 PASS
above 4 PASS
0.657
leapfrog_annotated.c below duet 1 FAIL
0.614 FAIL
above 4 FAIL
0.674
leapfrog_annotated_disjunction.c below duet 1 PASS
0.64 PASS
above 4 PASS
0.703
leapfrog_asymmetric2.c below duet 1 FAIL
0.669 FAIL
above 4 FAIL
0.732
leapfrog_asymmetric3.c below duet 1 FAIL
0.633 FAIL
above 4 FAIL
0.693
leapfrog_asymmetric.c below duet 1 FAIL
0.547 FAIL
above 4 FAIL
0.626
leapfrog.c below duet 1 FAIL
0.547 FAIL
above 4 FAIL
0.588
leapfrog_materialized.c below duet 1 FAIL
0.641 FAIL
above 4 FAIL
0.711
leapfrog_verbose.c below duet 1 FAIL
0.664 FAIL
above 4 FAIL
0.776
leapspin.c below duet 1 PASS
0.506 PASS
above 4 PASS
0.56
leapsum2.c below duet 1 FAIL
0.526 FAIL
above 4 FAIL
0.586
leapthree.c below duet 1 FAIL
0.562 FAIL
above 4 FAIL
0.622
microbobble2.c below duet 1 PASS
0.561 PASS
above 4 PASS
0.594
microbobble3.c below duet 1 PASS
0.531 PASS
above 4 PASS
0.582
microbobble_asymmetric.c below duet 1 PASS
0.527 PASS
above 4 PASS
0.541
microbobble.c below duet 1 PASS
0.522 PASS
above 4 PASS
0.601
simple_bl2.c below duet 1 PASS
0.598 PASS
above 4 PASS
0.641
simple_bl3.c below duet 1 FAIL
0.584 FAIL
above 4 FAIL
0.646
simple_bl.c below duet 1 FAIL
0.538 FAIL
above 4 FAIL
0.615
Total Below Time = 497.251 (was 505.161)
Above Time = 464.57 (was 419.523)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below duet 1 PASS
PASS
0.819 PASS
PASS
above 4 PASS
PASS
0.803
binval_example_2_unsafe.c below duet 1 OKAY
0.754 PASS
above 4 OKAY
0.771
binval_example_3_unsafe.c below duet 1 OKAY
0.759 PASS
above 4 OKAY
0.747
binval_example_4.c below duet 1 PASS
PASS
PASS
0.785 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.756
binval_example_4_unsafe.c below duet 1 OKAY
0.725 PASS
above 4 OKAY
0.747
binval_example_5.c below duet 1 FAIL
FAIL
PASS
0.997 FAIL
FAIL
PASS
above 4 FAIL
FAIL
PASS
1.112
binval_example_5_unsafe.c below duet 1 OKAY
0.931 PASS
above 4 OKAY
1.023
Total Below Time = 5.77 (was 5.705)
Above Time = 5.959 (was 6.028)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/ethereum
array2_memory_contract.c below duet 1 1.621
above 4 1.782
array3_memory_contract.c below duet 1 1.637
above 4 2.067
array4_memory_contract.c below duet 1 1.965
above 4 2.2
arraylength_memory_contract.c below duet 1 0.771
above 4 0.78
array_memory_contract.c below duet 1 1.068
above 4 1.121
GovernMental.c below duet 1 36.233
above 4 38.934 (46.981)
HelloWorld.c below duet 1 0.636
above 4 0.643
linear2_memory_contract.c below duet 1 1.312
above 4 1.454
linear2_no_memory_contract.c below duet 1 1.267
above 4 1.323
linear3_no_memory_contract.c below duet 1 1.341
above 4 1.492
Linear.c below duet 1 1.004
above 4 1.101
linear_memory_contract.c below duet 1 1.01
above 4 1.119
linear_no_memory_contract.c below duet 1 0.992
above 4 1.081
nested2_memory_contract.c below duet 1 1.542
above 4 1.731
nested2_no_memory_contract.c below duet 1 1.64
above 4 1.802
nested_memory_contract.c below duet 1 1.486
above 4 1.609
nested_no_memory_contract.c below duet 1 1.424
above 4 1.609
Total Below Time = 56.949 (was 60.154)
Above Time = 61.848 (was 70.023)

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