[Version Information]
WALi-OpenNWA version: 35b3457467a7787c4bb3a18de8f5d4ea4d314d2c (2018-03-22 22:15:25 -0500) "Fix to e-mail text in nightly_script.sh"
duet version: 9591e574693afe4eaeeaced7a5f2ec721ac9437f (2018-03-23 10:06:44 -0400) "Merge remote-tracking branch 'origin/srk' into Newton-ark2"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-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                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-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.
mathsat            20161206  MathSAT 5 SMT solver
menhir             20171222  LR(1) parser generator
mlgmpidl            1.2.6-1  OCaml interface to the GMP library
ntl                20171120  Number Theory Library
num                       0  The Num library for arbitrary-precision integer and
oasis                0.4.10  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind           1.7.3-1  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               20170905  Recurrence solver based on operational calculus
ounit                 2.0.7  Unit testing framework loosely based on HUnit. It i
ppx_deriving            3.2  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
Z3                 20161217  Z3 SMT solver

Test Name Output Duet Output No. of Rounds Result Run Time Duet Result
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
kmp.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
qsort.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
speed_pldi09_fig1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
speed_pldi09_fig4_2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
speed_pldi09_fig4_4.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
speed_pldi09_fig4_5.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
speed_pldi10_ex1.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
speed_pldi10_ex3.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
speed_pldi10_ex4.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
speed_popl10_fig2_1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
speed_popl10_fig2_2.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
speed_popl10_nested_multiple.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
speed_popl10_nested_single.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
speed_popl10_sequential_single.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
speed_popl10_simple_multiple.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
speed_popl10_simple_single_2.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
speed_popl10_simple_single.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
t07.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
t08.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
t09.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
t10.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
t11.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
t13.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
t15.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
t16.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
t19.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
t20.c below duet EXCEPTION 0.017
above EXCEPTION 0.015
t27.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
t28.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
t30.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
t37.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
t39.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
t46.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
t47.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
Total Below Assertions (True) = 0/35
Above Assertions (True) = 0/35		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.594
Above Time = 0.567
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
qsort_full.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
rec1-param_safe.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
rec1-param_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
rec1_safe.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
rec1_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
rec2-param_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
rec2-param_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
rec2_safe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
rec2_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
rec-test.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sas03_bothbranches.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sas03.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
simulated_lese_recursive.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
Total Below Assertions (True) = 0/10
Above Assertions (True) = 0/10		 Below Assertions (False) = 0/4
Above Assertions (False) = 0/4		 Below Time = 0.236
Above Time = 0.229
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
count_up_down_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
divide.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
factor_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
for_infinite_loop_1_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
for_infinite_loop_2_safe.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
interproc.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
mult.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
pointer_arith.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
quotient.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
subtract.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum01_bug02_sum01_bug02_base.case_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
sum01_bug02_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
sum01_real_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum01_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum01_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
sum02_safe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
sum03_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum03_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.015
sum04_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum04_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
terminator_02_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
terminator_02_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
terminator_03_safe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
terminator_03_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
token_ring01_safe.c below duet EXCEPTION 0.018
above EXCEPTION 0.028
token_ring01_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.032
toy_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
trex01_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
trex01_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
trex02_safe2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
trex02_safe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
trex02_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
trex03_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
trex03_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
trex04_safe.c below duet EXCEPTION 0.018
above EXCEPTION 0.015
while_infinite_loop_1_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
while_infinite_loop_2_safe.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
while_infinite_loop_3_safe.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
Total Below Assertions (True) = 0/26
Above Assertions (True) = 0/26		 Below Assertions (False) = 0/13
Above Assertions (False) = 0/13		 Below Time = 0.661
Above Time = 0.661
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below duet EXCEPTION 0.019
above EXCEPTION 0.018
blogger_simplified1.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
divided_difference2.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
mult-proc.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
mult-proc-params.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
popall.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
simulated_scc.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
Total Below Assertions (True) = 0/7
Above Assertions (True) = 0/7		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.121
Above Time = 0.117
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
degree2_binomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
degree2_monomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
degree3_binomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
degree3_monomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
degree4_binomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
degree4_monomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
degree5_binomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
degree5_monomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/9
Above Assertions (True) = 0/9		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.153
Above Time = 0.146
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
cubic_with_square_interproc.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
cubic_with_square_nonlinear.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
cubic_with_square_nonlinear_interproc.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
cubic_with_square_nonlinear_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
cubic_with_square_unsafe.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
multi-input.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
multi-input_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
nondet_loop_bound.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
nondet_loop_bound_quartic.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
nondet_loop_bound_quartic_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
nondet_loop_bound_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
nonlinear_stratified.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
nonlinear_stratified_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
quartic_with_cube.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
quartic_with_cube_nonlinear.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
quartic_with_cube_nonlinear_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
quartic_with_cube_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
quintic_with_quartic.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
quintic_with_quartic_nonlinear.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
quintic_with_quartic_nonlinear_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
quintic_with_quartic_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/12
Above Assertions (True) = 0/12		 Below Assertions (False) = 0/10
Above Assertions (False) = 0/10		 Below Time = 0.381
Above Time = 0.369
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
degree2_FD_AllAux_AllAssm.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
degree2_FD_AllAux_FewAssm.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
degree2_FD_FewAux_FewAssm.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
degree3.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
degree3_FD.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
degree4.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/8
Above Assertions (True) = 0/8		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.134
Above Time = 0.13
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
loop_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
simulated_lese_parser.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
simulated_lese_sentinel.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/3
Above Assertions (True) = 0/3		 Below Assertions (False) = 0/1
Above Assertions (False) = 0/1		 Below Time = 0.067
Above Time = 0.064
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
Total Below Assertions (True) = 0/1
Above Assertions (True) = 0/1		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.016
Above Time = 0.015
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
Total Below Assertions (True) = 0/1
Above Assertions (True) = 0/1		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.017
Above Time = 0.017
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
array_false-unreach-call2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
array_false-unreach-call3.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
array_true-unreach-call1.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
array_true-unreach-call2.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
array_true-unreach-call3.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
array_true-unreach-call4.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
const_false-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
const_true-unreach-call1.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
diamond_false-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
diamond_true-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
diamond_true-unreach-call2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
functions_false-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
functions_true-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
multivar_false-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
multivar_true-unreach-call1.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
nested_false-unreach-call1.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
nested_true-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
overflow_true-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
phases_false-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
phases_false-unreach-call2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
phases_true-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
phases_true-unreach-call2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
simple_false-unreach-call1.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
simple_false-unreach-call2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
simple_false-unreach-call3.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
simple_false-unreach-call4.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
simple_true-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
simple_true-unreach-call2.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
simple_true-unreach-call3.c below duet EXCEPTION 0.019
above EXCEPTION 0.019
simple_true-unreach-call4.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
underapprox_false-unreach-call1.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
underapprox_false-unreach-call2.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
underapprox_true-unreach-call1.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
underapprox_true-unreach-call2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/19
Above Assertions (True) = 0/19		 Below Assertions (False) = 0/16
Above Assertions (False) = 0/16		 Below Time = 0.596
Above Time = 0.58
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
apache-get-tag_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
down_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
fragtest_simple_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
half_2_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
heapsort_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
id_build_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_trans_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
id_trans_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
large_const_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
MADWiFi-encode_ie_ok_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
nested6_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
nested9_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
nest-if3_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
NetBSD_loop_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sendmail-close-angle_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
seq_true-unreach-call.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
SpamAssassin-loop_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
string_concat-noarr_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.018
up_true-unreach-call.c below duet EXCEPTION 0.019
above EXCEPTION 0.018
Total Below Assertions (True) = 0/19
Above Assertions (True) = 0/19		 Below Assertions (False) = 0/1
Above Assertions (False) = 0/1		 Below Time = 0.347
Above Time = 0.337
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.02
bhmr2007_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
cggmp2005b_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
cggmp2005_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
cggmp2005_variant_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
css2003_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
ddlm2013_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
gcnr2008_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
gj2007b_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
gj2007_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
gr2006_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
gsv2008_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
hhk2008_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
jm2006_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
jm2006_variant_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
mcmillan2006_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/15
Above Assertions (True) = 0/15		 Below Assertions (False) = 0/1
Above Assertions (False) = 0/1		 Below Time = 0.274
Above Time = 0.268
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
count_by_1_variant_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
count_by_2_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
count_by_k_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
count_by_nondet_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
gauss_sum_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
half_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
nested_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
Total Below Assertions (True) = 0/8
Above Assertions (True) = 0/8		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.139
Above Time = 0.136
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
array_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
bubble_sort_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.02
bubble_sort_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
compact_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
count_up_down_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
count_up_down_true-unreach-call_true-termination.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
eureka_01_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
eureka_01_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
eureka_05_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
for_bounded_loop1_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
for_bounded_loop1_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
for_infinite_loop_1_true-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
for_infinite_loop_2_true-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
heavy_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
heavy_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
insertion_sort_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
insertion_sort_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
invert_string_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
invert_string_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
linear_sea.ch_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
linear_search_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
lu.cmp_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
ludcmp_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
matrix_false-unreach-call_true-termination.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
matrix_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
n.c11_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
n.c24_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
n.c40_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
nec11_false-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
nec20_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
nec40_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
string_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
string_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum01_bug02_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum01_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum01_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum03_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum03_true-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum04_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
sum04_true-unreach-call_true-termination.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
sum_array_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum_array_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
terminator_01_false-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
terminator_02_false-unreach-call_true-termination.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
terminator_02_true-unreach-call_true-termination.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
terminator_03_false-unreach-call_true-termination.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
terminator_03_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
trex01_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
trex01_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
trex02_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
trex02_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
trex03_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
trex03_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
trex04_true-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
veris.c_NetBSD-libc__loop_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
verisec_NetBSD-libc__loop_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
vogal_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
vogal_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
while_infinite_loop_1_true-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
while_infinite_loop_2_true-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
while_infinite_loop_3_true-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
while_infinite_loop_4_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/35
Above Assertions (True) = 0/35		 Below Assertions (False) = 0/32
Above Assertions (False) = 0/32		 Below Time = 1.143
Above Time = 1.114
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Ackermann02_false-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Ackermann03_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
Ackermann04_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Addition01_true-unreach-call_true-termination.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
Addition02_false-unreach-call_false-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Addition03_false-no-overflow.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
Addition03_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
EvenOdd01_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
EvenOdd03_false-unreach-call_false-termination.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
Fibonacci01_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
Fibonacci02_true-unreach-call_true-termination.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
Fibonacci03_true-unreach-call_true-termination.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
Fibonacci04_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Fibonacci05_false-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
gcd01_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
gcd02_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
McCarthy91_false-unreach-call_false-termination.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
McCarthy91_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
MultCommutative_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Primes_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
recHanoi01_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
recHanoi02_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
recHanoi03_true-unreach-call_true-termination.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/18
Above Assertions (True) = 0/18		 Below Assertions (False) = 0/7
Above Assertions (False) = 0/7		 Below Time = 0.421
Above Time = 0.411
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
afterrec_2calls_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
afterrec_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
afterrec_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
fibo_10_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
fibo_10_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
fibo_15_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
fibo_15_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
fibo_20_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
fibo_20_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
fibo_25_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
fibo_25_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
fibo_2calls_10_false-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.019
fibo_2calls_10_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
fibo_2calls_15_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.02
fibo_2calls_15_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.021
fibo_2calls_20_false-unreach-call.c below duet EXCEPTION 0.019
above EXCEPTION 0.022
fibo_2calls_20_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.02
fibo_2calls_25_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.019
fibo_2calls_25_true-unreach-call.c below duet EXCEPTION 0.024
above EXCEPTION 0.019
fibo_2calls_2_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.02
fibo_2calls_2_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.019
fibo_2calls_4_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
fibo_2calls_4_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
fibo_2calls_5_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
fibo_2calls_5_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
fibo_2calls_6_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.02
fibo_2calls_6_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
fibo_2calls_8_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.019
fibo_2calls_8_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.019
fibo_5_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
fibo_5_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
fibo_7_false-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
fibo_7_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
id2_b2_o3_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
id2_b3_o2_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id2_b3_o5_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
id2_b5_o10_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
id2_i5_o5_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
id2_i5_o5_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_b2_o3_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
id_b3_o2_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
id_b3_o5_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
id_b5_o10_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
id_i10_o10_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_i10_o10_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
id_i15_o15_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_i15_o15_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_i20_o20_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
id_i20_o20_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_i25_o25_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
id_i25_o25_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
id_i5_o5_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_i5_o5_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_o1000_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_o100_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
id_o10_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
id_o200_false-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
id_o20_false-unreach-call.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
id_o3_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum_10x0_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum_10x0_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
sum_15x0_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum_15x0_true-unreach-call.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
sum_20x0_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum_20x0_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
sum_25x0_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum_25x0_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
sum_2x3_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum_2x3_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum_non_eq_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum_non_eq_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
sum_non_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum_non_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/36
Above Assertions (True) = 0/36		 Below Assertions (False) = 0/38
Above Assertions (False) = 0/38		 Below Time = 1.282
Above Time = 1.285
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-lit
rec-afnp2014_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
rec-bhmr2007_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
rec-cggmp2005b_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
rec-cggmp2005_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
rec-cggmp2005_variant_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
rec-css2003_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
rec-ddlm2013_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
rec-gcnr2008_false-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
rec-gj2007b_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
rec-gj2007_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
rec-gr2006_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
rec-gsv2008_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
rec-hhk2008_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
rec-jm2006_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
rec-jm2006_variant_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
rec-mcmillan2006_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/15
Above Assertions (True) = 0/15		 Below Assertions (False) = 0/1
Above Assertions (False) = 0/1		 Below Time = 0.276
Above Time = 0.268
/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 EXCEPTION 0.016
above EXCEPTION 0.016
rec-count_by_1_variant_true-unreach-call.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
rec-count_by_2_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
rec-count_by_k_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
rec-count_by_nondet_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
rec-gauss_sum_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
rec-half_true-unreach-call.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
rec-nested_true-unreach-call.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/8
Above Assertions (True) = 0/8		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.136
Above Time = 0.131
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
cubic_polynomial_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
edit_distance_bottom_up.c below duet EXCEPTION 0.018
above EXCEPTION 0.02
edit_distance_top_down.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
log_log_n_solution.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
log_log_n_solution_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
log_n_solution.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
log_n_solution_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
multivariate_1.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
multivariate_1_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
multivariate_higher_order.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
multivariate_higher_order_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
n_cubed_solution.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
n_cubed_solution_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
n_log_n_solution.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
n_log_n_solution_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
n_squared_two_base_case_even.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
n_squared_two_base_case_even_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
n_squared_two_base_case_odd.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
n_squared_two_base_case_odd_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
pascals_dynamic.c below duet EXCEPTION 0.018
above EXCEPTION 0.019
pascals_dynamic_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
pascals_iterative.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
pascals_iterative_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
pascals_recursive.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
pascals_recursive_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
squared_solution.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
squared_solution_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
two_n_even.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
two_n_even_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
two_n_odd.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
two_n_odd_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
two_to_n_over_two_even.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
two_to_n_over_two_even_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
two_to_n_over_two_odd.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
two_to_n_over_two_odd_unsafe.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
two_to_n_squared.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
two_to_n_squared_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
two_to_two_to_n.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
two_to_two_to_n_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
Total Below Assertions (True) = 0/21
Above Assertions (True) = 0/21		 Below Assertions (False) = 0/19
Above Assertions (False) = 0/19		 Below Time = 0.693
Above Time = 0.667
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
adding_and_mult_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
binary_search_array_tree.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
exp_add_linear.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
exp_add_linear_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
exp_add_loop_rec.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
exp_add_loop_rec_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
exp_add_loop_variable.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
exp_add_loop_variable_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.018
exp_with_linear_inner_loop.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
exp_with_linear_inner_loop_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
halving_log1.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
linear_two_to_n.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
linear_two_to_n_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
loop_five_to_n.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
loop_five_to_n_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
non_loop_five_to_n.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
non_loop_five_to_n_unsafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
power_log_modified.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
simple_exponential.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
simple_exponential_for.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
simple_exponential_for_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
simple_exponential_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
two_to_n_minus_n.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
two_to_n_minus_n_loop.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
two_to_n_minus_n_loop_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
two_to_n_minus_n_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
Total Below Assertions (True) = 0/15
Above Assertions (True) = 0/15		 Below Assertions (False) = 0/12
Above Assertions (False) = 0/12		 Below Time = 0.462
Above Time = 0.446
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
02.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
03.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
04.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
05.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
06.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
07.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
08.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
09.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
10.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
11.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
12.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
13.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
14.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
15.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
16.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
17.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
18.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
19.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
20.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
21.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
22.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
23.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
24.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
25.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
26.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
27.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
28.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
29.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
30.c below duet EXCEPTION 0.019
above EXCEPTION 0.016
31.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
32.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
33.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
34.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
35.c below duet EXCEPTION 0.017
above EXCEPTION 0.015
36.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
37.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
38.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
39.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
40.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
41.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
42.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
43.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
44.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
45.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
46.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
Total Below Assertions (True) = 0/46
Above Assertions (True) = 0/46		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.792
Above Time = 0.76
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
AGHKTW2017_foo.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
AGHKTW2017_loginSafe.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
AGHKTW2017_loopAndBranch_safe.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
AGHKTW2017_loopAndBranch_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
BCK2011_gauss.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
BCK2011_strength_reduction.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
BCK2011_strength_reduction_linear.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
CFD17-add-const_product.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
CFD17-add-const_product-syntax.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
CFD17-add-const_self-comp.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
collatz_product-syntax.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
collatz_self-comp.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
fibonacci_information_flow.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
halving_log1_product.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
halving_log1_product-syntax.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
halving_log1_self-comp.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
loop_splitting_test_safe.c below duet EXCEPTION 0.018
above EXCEPTION 0.018
TA2005_fib2.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
TA2005_fib.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
top-level-if-add-const_product.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
top-level-if-add-const_self-comp.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/21
Above Assertions (True) = 0/21		 Below Assertions (False) = 0/1
Above Assertions (False) = 0/1		 Below Time = 0.382
Above Time = 0.365
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/canonical2017
Total Below Assertions (True) = 0/0
Above Assertions (True) = 0/0		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.0
Above Time = 0.0
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc2017
alternative_fig_1_d.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
c3_cleanup_better.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
c3_cleanup.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
c3_intermediate.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
c3_noinv.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
doublers.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
doublers_easier.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
doublers_easy.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
exp_mult.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
fig1_rotation_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
guessing_game.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
not_P_solvable.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/11
Above Assertions (True) = 0/11		 Below Assertions (False) = 0/1
Above Assertions (False) = 0/1		 Below Time = 0.2
Above Time = 0.196
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/max_equals
five_seven.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
maxequals_linear_1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
maxequals_linear_2.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
maxequals_linear_3.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
maxequals_linear_4.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
maxequals_linear_5.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
maxequals_linear_6.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
maxequals_matrix1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
maxequals_matrix2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
maxequals_quadratic1.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
maxequals_quadratic2.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
maxequals_stratified1.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
maxequals_stratified2.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
maxequals_stratified3.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
nine.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
nine_nondecreasing.c below duet EXCEPTION 0.019
above EXCEPTION 0.017
sum_interval_1.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
sum_interval_2.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
sum_interval_3.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
TrackingObjectFields.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
TrackingObjectFields_inlined.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
Total Below Assertions (True) = 0/21
Above Assertions (True) = 0/21		 Below Assertions (False) = 0/0
Above Assertions (False) = 0/0		 Below Time = 0.36
Above Time = 0.347
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/branching_loops
bobble2.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
bobble2_varloop.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
bobble3.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
bobble4.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
bobble5.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
bobble.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
inchworm2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
inchworm3.c below duet EXCEPTION 0.017
above EXCEPTION 0.023
inchworm4.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
inchworm5.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
inchworm6_unsafe.c below duet EXCEPTION 0.016
above EXCEPTION 0.018
inchworm.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
leapdiff2.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
leapfrog_annotated.c below duet EXCEPTION 0.016
above EXCEPTION 0.015
leapfrog_annotated_disjunction.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
leapfrog_asymmetric2.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
leapfrog_asymmetric3.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
leapfrog_asymmetric.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
leapfrog.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
leapfrog_materialized.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
leapfrog_verbose.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
leapspin.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
leapsum2.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
leapthree.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
microbobble2.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
microbobble3.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
microbobble_asymmetric.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
microbobble.c below duet EXCEPTION 0.018
above EXCEPTION 0.016
simple_bl2.c below duet EXCEPTION 0.016
above EXCEPTION 0.017
simple_bl3.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
simple_bl.c below duet EXCEPTION 0.016
above EXCEPTION 0.016
Total Below Assertions (True) = 0/30
Above Assertions (True) = 0/30		 Below Assertions (False) = 0/1
Above Assertions (False) = 0/1		 Below Time = 0.528
Above Time = 0.522
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/strings_numeric
binval_example_2.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
binval_example_2_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
binval_example_3_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
binval_example_4.c below duet EXCEPTION 0.018
above EXCEPTION 0.017
binval_example_4_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.017
binval_example_5.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
binval_example_5_unsafe.c below duet EXCEPTION 0.017
above EXCEPTION 0.016
Total Below Assertions (True) = 0/3
Above Assertions (True) = 0/3		 Below Assertions (False) = 0/4
Above Assertions (False) = 0/4		 Below Time = 0.121
Above Time = 0.117