[Version Information]
WALi-OpenNWA version: 088075c428c89531f84bc48ca70e4f182df9184b (2017-08-09 10:53:57 -0500) "the scripts used for POPL18 submission and fixed soundness errors for nightly run"
duet version: 7a637cd53ac9dd819b179b14263f4763715db4a5 (2017-08-21 16:13:10 -0400) "Merge remote-tracking branch 'origin/ark2' into 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.7.0  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
camlp4               4.02+7  Camlp4 is a system for writing extensible parsers f
cil                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
conf-which                1  Virtual package relying on which
cppo                  1.6.0  Equivalent of the C preprocessor for OCaml programs
cppo_ocamlbuild       1.6.0  ocamlbuild support for cppo, OCaml-friendly source 
deriving           20140904  Extension to OCaml for deriving functions from type
jbuilder         1.0+beta12  Fast, portable and opinionated build system
mathsat            20161206  MathSAT 5 SMT solver
menhir             20170712  LR(1) parser generator
mlgmpidl              1.2.4  OCaml interface to the GMP 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  A library manager for OCaml
ocamlgraph            1.8.7  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.8  Generate OCaml modules from source files
OCRS               20170817  Recurrence solver based on operational calculus
optcomp                 1.6  Optional compilation with cpp-like directives
ounit                 2.0.0  Unit testing framework loosely based on HUnit. It i
ppx_deriving            4.1  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
result                  1.2  Compatibility Result module
Z3                 20161217  Z3 SMT solver

Test Name Output Duet Output No. of Rounds Result Run Time (Prev.) Duet Result
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below duet 1 FAIL
0.363 (0.469) FAIL
above 4 FAIL
0.371 (0.471)
kmp.c below duet 1 PASS
0.83 (1.01) PASS
above 4 PASS
0.862 (1.097)
qsort.c below duet 4 PASS
0.803 (0.96) FAIL
above 4 FAIL
3.615 (4.373)
speed_pldi09_fig1.c below duet 1 PASS
0.373 (0.482) PASS
above 4 PASS
0.385 (0.473)
speed_pldi09_fig4_2.c below duet 1 FAIL
0.38 (0.492) FAIL
above 4 FAIL
0.395 (0.478)
speed_pldi09_fig4_4.c below duet 1 PASS
0.428 (0.53) PASS
above 4 PASS
0.441 (0.577)
speed_pldi09_fig4_5.c below duet 1 PASS
0.369 (0.471) PASS
above 4 PASS
0.399 (0.478)
speed_pldi10_ex1.c below duet 1 PASS
0.737 (0.927) PASS
above 4 PASS
0.744 (0.964)
speed_pldi10_ex3.c below duet 1 PASS
0.413 (0.507) PASS
above 4 PASS
0.431 (0.544)
speed_pldi10_ex4.c below duet 1 PASS
0.399 PASS
above 4 PASS
0.417 (0.512)
speed_popl10_fig2_1.c below duet 1 PASS
0.392 (0.492) PASS
above 4 PASS
0.422 (0.526)
speed_popl10_fig2_2.c below duet 1 FAIL
0.364 (0.451) FAIL
above 4 FAIL
0.375 (0.473)
speed_popl10_nested_multiple.c below duet 1 PASS
0.406 (0.532) PASS
above 4 PASS
0.424 (0.545)
speed_popl10_nested_single.c below duet 1 PASS
0.401 (0.508) PASS
above 4 PASS
0.396 (0.495)
speed_popl10_sequential_single.c below duet 1 PASS
0.373 (0.443) PASS
above 4 PASS
0.377 (0.48)
speed_popl10_simple_multiple.c below duet 1 PASS
0.41 (0.517) PASS
above 4 PASS
0.402 (0.506)
speed_popl10_simple_single_2.c below duet 1 PASS
0.418 (0.542) PASS
above 4 PASS
0.439 (0.549)
speed_popl10_simple_single.c below duet 1 PASS
0.346 (0.444) PASS
above 4 PASS
0.363 (0.443)
t07.c below duet 1 PASS
0.391 (0.473) PASS
above 4 PASS
0.384 (0.488)
t08.c below duet 1 PASS
0.368 (0.469) PASS
above 4 PASS
0.363 (0.458)
t09.c below duet 1 PASS
0.356 (0.447) PASS
above 4 PASS
0.36 (0.426)
t10.c below duet 1 PASS
0.353 (0.456) PASS
above 4 PASS
0.373 (0.463)
t11.c below duet 1 PASS
0.396 (0.489) PASS
above 4 PASS
0.401 (0.507)
t13.c below duet 1 FAIL
0.39 (0.491) FAIL
above 4 FAIL
0.402 (0.507)
t15.c below duet 1 PASS
0.381 (0.472) PASS
above 4 PASS
0.385 (0.474)
t16.c below duet 1 PASS
0.37 (0.473) PASS
above 4 PASS
0.378 (0.457)
t19.c below duet 1 PASS
0.362 (0.454) PASS
above 4 PASS
0.372 (0.457)
t20.c below duet 1 PASS
0.355 (0.453) PASS
above 4 PASS
0.358 (0.462)
t27.c below duet 1 PASS
0.407 (0.497) PASS
above 4 PASS
0.414 (0.542)
t28.c below duet 1 PASS
0.412 (0.491) PASS
above 4 PASS
0.405 (0.538)
t30.c below duet 1 FAIL
0.368 (0.503) FAIL
above 4 FAIL
0.37 (0.452)
t37.c below duet 2 PASS
0.467 (0.626) FAIL
above 4 PASS
0.582 (0.716)
t39.c below duet 2 PASS
0.464 (0.575) FAIL
above 4 PASS
0.498 (0.625)
t46.c below duet 1 PASS
0.369 (0.462) PASS
above 4 PASS
0.414 (0.494)
t47.c below duet 1 PASS
0.369 (0.463) PASS
above 4 PASS
0.38 (0.483)
Total Below Time = 14.783 (was 18.51)
Above Time = 18.097 (was 22.533)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below duet 2 PASS
PASS
0.386 (0.462) PASS
PASS
above 4 PASS
PASS
0.424 (0.525)
qsort_full.c below duet 4 PASS
PASS
PASS
PASS
PASS
PASS
10.277 (12.978) PASS
PASS
PASS
PASS
PASS
PASS
above 4 FAIL
PASS
PASS
PASS
PASS
PASS
26.867 (33.927)
rec1-param_safe.c below duet 2 PASS
PASS
PASS
0.359 (0.456) PASS
FAIL
FAIL
above 4 PASS
PASS
PASS
0.374 (0.481)
rec1-param_unsafe.c below duet 2 OKAY
0.381 (0.455) PASS
above 4 OKAY
0.39 (0.471)
rec1_safe.c below duet 2 PASS
PASS
PASS
0.347 (0.445) PASS
FAIL
FAIL
above 4 PASS
PASS
PASS
0.36 (0.465)
rec1_unsafe.c below duet 2 OKAY
0.349 (0.429) PASS
above 4 OKAY
0.357 (0.446)
rec2-param_safe.c below duet 2 PASS
PASS
PASS
0.355 (0.462) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.371 (0.467)
rec2-param_unsafe.c below duet 2 OKAY
0.362 (0.43) PASS
above 4 OKAY
0.38 (0.445)
rec2_safe.c below duet 2 PASS
PASS
PASS
0.342 (0.441) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.359 (0.455)
rec2_unsafe.c below duet 2 OKAY
0.342 (0.442) PASS
above 4 OKAY
0.358 (0.454)
rec-test.c below duet 2 PASS
0.343 (0.447) FAIL
above 4 PASS
0.354 (0.451)
sas03_bothbranches.c below duet 7 PASS
0.642 (0.795) PASS
above 4 FAIL
1.316 (1.553)
sas03.c below duet 2 PASS
0.643 (0.801) PASS
above 4 PASS
0.789 (1.026)
simulated_lese_recursive.c below duet 2 PASS
0.364 (0.468) PASS
above 4 PASS
0.421 (0.486)
Total Below Time = 15.492 (was 19.511)
Above Time = 33.12 (was 41.652)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below duet 1 PASS
0.336 (0.416) PASS
above 4 PASS
0.342 (0.429)
count_up_down_unsafe.c below duet 1 OKAY
0.335 (0.421) PASS
above 4 OKAY
0.33 (0.426)
divide.c below duet 1 PASS
0.336 (0.424) PASS
above 4 PASS
0.338 (0.439)
factor_unsafe.c below duet 1 OKAY
0.337 (0.424) PASS
above 4 OKAY
0.33 (0.417)
for_infinite_loop_1_safe.c below duet 1 PASS
0.322 (0.414) PASS
above 0 PASS
0.32 (0.427)
for_infinite_loop_2_safe.c below duet 1 PASS
0.325 (0.406) PASS
above 0 PASS
0.323 (0.393)
interproc.c below duet 1 PASS
0.319 (0.395) PASS
above 4 PASS
0.336 (0.383)
mult.c below duet 1 PASS
PASS
0.335 (0.407) PASS
PASS
above 4 PASS
PASS
0.333 (0.414)
pointer_arith.c below duet 1 PASS
PASS
PASS
PASS
0.328 (0.37) PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
0.324 (0.409)
quotient.c below duet 3 PASS
0.41 (0.521) PASS
above 4 PASS
0.454 (0.546)
subtract.c below duet 1 PASS
0.325 (0.399) PASS
above 4 PASS
0.329 (0.404)
sum01_bug02_sum01_bug02_base.case_unsafe.c below duet 1 OKAY
0.352 (0.428) PASS
above 4 OKAY
0.348 (0.451)
sum01_bug02_unsafe.c below duet 1 OKAY
0.391 (0.493) PASS
above 4 OKAY
0.407 (0.494)
sum01_real_safe.c below duet 1 PASS
0.332 (0.42) PASS
above 4 PASS
0.336 (0.426)
sum01_safe.c below duet 1 PASS
0.333 (0.402) PASS
above 4 PASS
0.342 (0.416)
sum01_unsafe.c below duet 1 OKAY
0.371 (0.431) PASS
above 4 OKAY
0.387 (0.446)
sum02_safe.c below duet 1 PASS
0.347 (0.431) PASS
above 4 PASS
0.347 (0.442)
sum03_safe.c below duet 1 PASS
0.348 (0.432) PASS
above 0 PASS
0.35 (0.422)
sum03_unsafe.c below duet 1 OKAY
0.393 (0.461) PASS
above 0 OKAY
0.391 (0.478)
sum04_safe.c below duet 1 PASS
0.331 (0.44) PASS
above 4 PASS
0.337 (0.406)
sum04_unsafe.c below duet 1 OKAY
0.358 (0.451) PASS
above 4 OKAY
0.37 (0.441)
terminator_02_safe.c below duet 1 PASS
0.337 (0.434) PASS
above 4 PASS
0.343 (0.395)
terminator_02_unsafe.c below duet 1 OKAY
0.359 (0.458) PASS
above 4 OKAY
0.354 (0.438)
terminator_03_safe.c below duet 1 PASS
0.333 (0.433) PASS
above 4 PASS
0.339 (0.42)
terminator_03_unsafe.c below duet 1 OKAY
0.334 (0.403) PASS
above 4 OKAY
0.351 (0.418)
token_ring01_safe.c below duet 4 FAIL
141.092 (184.135) FAIL
above 4 TIMEOUT
300.023
token_ring01_unsafe.c below duet 4 OKAY
179.684 (224.806) PASS
above 4 TIMEOUT
300.027
toy_safe.c below duet EXCEPTION
174.952 (236.172) TIMEOUT
above EXCEPTION
180.462 (256.506)
trex01_safe.c below duet 1 PASS
0.746 (0.855) PASS
above 4 PASS
0.381 (0.45)
trex01_unsafe.c below duet 1 OKAY
0.371 (0.448) PASS
above 4 OKAY
0.375 (0.461)
trex02_safe2.c below duet 3 PASS
0.382 (0.483) PASS
above 4 PASS
0.42 (0.513)
trex02_safe.c below duet 3 PASS
0.394 (0.473) PASS
above 4 PASS
0.415 (0.505)
trex02_unsafe.c below duet 3 OKAY
0.386 (0.478) PASS
above 4 OKAY
0.419 (0.51)
trex03_safe.c below duet 1 PASS
0.422 (0.482) PASS
above 4 PASS
0.453 (0.522)
trex03_unsafe.c below duet 1 OKAY
0.402 (0.492) PASS
above 4 OKAY
0.435 (0.504)
trex04_safe.c below duet 1 PASS
0.354 (0.426) PASS
above 4 PASS
0.375 (0.449)
while_infinite_loop_1_safe.c below duet 1 PASS
0.327 (0.372) PASS
above 0 PASS
0.326 (0.384)
while_infinite_loop_2_safe.c below duet 1 PASS
0.314 (0.361) PASS
above 0 PASS
0.324 (0.372)
while_infinite_loop_3_safe.c below duet 1 PASS
0.325 (0.379) PASS
above 4 PASS
0.32 (0.392)
Total Below Time = 508.778 (was 661.076)
Above Time = 793.516 (was 872.418)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below duet 3 PASS
0.382 (0.464) PASS
above 4 FAIL
0.572 (0.651)
blogger_simplified1.c below duet 3 PASS
0.75 (0.864) PASS
above 4 PASS
1.217 (1.501)
divided_difference2.c below duet TIMEOUT
300.006 TIMEOUT
above TIMEOUT
300.007
mult-proc.c below duet 3 PASS
PASS
0.379 (0.453) PASS
PASS
above 4 PASS
PASS
0.404 (0.461)
mult-proc-params.c below duet 3 PASS
PASS
0.394 (0.481) PASS
PASS
above 4 PASS
PASS
0.418 (0.525)
popall.c below duet 1 PASS
PASS
PASS
PASS
PASS
0.411 (0.481) PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
0.414 (0.504)
simulated_scc.c below duet 1 PASS
PASS
0.473 (0.562) PASS
PASS
above 4 PASS
PASS
0.473 (0.563)
Total Below Time = 302.795 (was 303.314)
Above Time = 303.505 (was 304.211)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below duet 1 PASS
0.353 (0.424) PASS
above 4 PASS
0.382 (0.438)
degree2_binomial.c below duet 1 FAIL
0.465 (0.545) PASS
above 4 FAIL
0.509 (0.599)
degree2_monomial.c below duet 1 PASS
0.369 (0.44) PASS
above 4 PASS
0.395 (0.48)
degree3_binomial.c below duet 1 PASS
0.765 (0.913) PASS
above 4 PASS
0.843 (0.981)
degree3_monomial.c below duet 1 PASS
0.412 (0.528) PASS
above 4 PASS
0.439 (0.54)
degree4_binomial.c below duet 1 FAIL
1.324 (1.561) PASS
above 4 FAIL
1.391 (1.648)
degree4_monomial.c below duet 1 PASS
0.474 (0.546) PASS
above 4 PASS
0.515 (0.602)
degree5_binomial.c below duet 1 FAIL
1.386 (1.704) PASS
above 4 FAIL
1.428 (1.772)
degree5_monomial.c below duet 1 PASS
0.582 (0.69) PASS
above 4 PASS
0.609 (0.732)
Total Below Time = 6.13 (was 7.351)
Above Time = 6.511 (was 7.792)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below duet 1 FAIL
0.362 (0.436) PASS
above 4 FAIL
0.362 (0.44)
cubic_with_square_interproc.c below duet 2 FAIL
0.415 (0.502) FAIL
above 4 FAIL
0.437 (0.536)
cubic_with_square_nonlinear.c below duet 1 FAIL
0.367 (0.427) PASS
above 4 FAIL
0.365 (0.436)
cubic_with_square_nonlinear_interproc.c below duet 2 FAIL
0.411 (0.473) FAIL
above 4 FAIL
0.436 (0.515)
cubic_with_square_nonlinear_unsafe.c below duet 1 OKAY
0.364 (0.433) PASS
above 4 OKAY
0.383 (0.455)
cubic_with_square_unsafe.c below duet 1 OKAY
0.366 (0.444) PASS
above 4 OKAY
0.377
multi-input.c below duet 1 FAIL
0.422 (0.515) PASS
above 4 FAIL
0.421 (0.515)
multi-input_unsafe.c below duet 1 OKAY
0.444 (0.53) PASS
above 4 OKAY
0.44 (0.531)
nondet_loop_bound.c below duet 1 FAIL
0.371 (0.43) PASS
above 4 FAIL
0.365 (0.429)
nondet_loop_bound_quartic.c below duet 1 FAIL
0.377 (0.451) PASS
above 4 FAIL
0.376 (0.456)
nondet_loop_bound_quartic_unsafe.c below duet 1 OKAY
0.372 (0.448) PASS
above 4 OKAY
0.372 (0.452)
nondet_loop_bound_unsafe.c below duet 1 OKAY
0.367 (0.419) PASS
above 4 OKAY
0.378 (0.42)
nonlinear_stratified.c below duet 1 FAIL
0.373 (0.447) FAIL
above 4 FAIL
0.374 (0.452)
nonlinear_stratified_unsafe.c below duet 1 OKAY
0.37 (0.438) PASS
above 4 OKAY
0.386 (0.446)
quartic_with_cube.c below duet 1 FAIL
0.372 (0.452) PASS
above 4 FAIL
0.38 (0.443)
quartic_with_cube_nonlinear.c below duet 1 FAIL
0.39 (0.457) PASS
above 4 FAIL
0.383 (0.449)
quartic_with_cube_nonlinear_unsafe.c below duet 1 OKAY
0.384 (0.455) PASS
above 4 OKAY
0.396 (0.481)
quartic_with_cube_unsafe.c below duet 1 OKAY
0.395 (0.458) PASS
above 4 OKAY
0.397
quintic_with_quartic.c below duet 1 PASS
0.376 (0.471) PASS
above 4 PASS
0.38 (0.465)
quintic_with_quartic_nonlinear.c below duet 1 PASS
0.413 (0.501) PASS
above 4 PASS
0.41 (0.483)
quintic_with_quartic_nonlinear_unsafe.c below duet 1 OKAY
0.43 (0.503) PASS
above 4 OKAY
0.409 (0.498)
quintic_with_quartic_unsafe.c below duet 1 OKAY
0.394 (0.487) PASS
above 4 OKAY
0.387 (0.454)
Total Below Time = 8.535 (was 10.177)
Above Time = 8.614 (was 10.201)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below duet 1 PASS
0.5 (0.595) PASS
above 4 PASS
0.49 (0.587)
degree2_FD_AllAux_AllAssm.c below duet 1 PASS
1.788 (2.136) PASS
above 4 PASS
1.806 (2.205)
degree2_FD_AllAux_FewAssm.c below duet 1 PASS
1.805 (2.095) PASS
above 4 PASS
1.838 (2.213)
degree2_FD_FewAux_FewAssm.c below duet 1 PASS
0.638 (0.759) PASS
above 4 PASS
0.658 (0.775)
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below duet 1 PASS
0.663 (0.774) PASS
above 4 PASS
0.648 (0.774)
degree3.c below duet 1 PASS
0.545 (0.652) PASS
above 4 PASS
0.553 (0.631)
degree3_FD.c below duet 1 PASS
0.644 (0.788) PASS
above 4 PASS
0.689 (0.802)
degree4.c below duet 1 PASS
0.412 (0.496) PASS
above 4 PASS
0.417 (0.505)
Total Below Time = 6.995 (was 8.295)
Above Time = 7.099 (was 8.492)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below duet 1 PASS
0.394 (0.474) PASS
above 4 PASS
0.4 (0.459)
loop_unsafe.c below duet 1 OKAY
0.398 (0.48) PASS
above 4 OKAY
0.408 (0.478)
simulated_lese_parser.c below duet 1 PASS
0.332 (0.407) PASS
above 4 PASS
0.334 (0.407)
simulated_lese_sentinel.c below duet 1 PASS
0.352 (0.41) PASS
above 4 PASS
0.356 (0.426)
Total Below Time = 1.476 (was 1.771)
Above Time = 1.498 (was 1.77)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below duet 1 PASS
PASS
PASS
0.343 (0.427) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.346 (0.428)
Total Below Time = 0.343 (was 0.427)
Above Time = 0.346 (was 0.428)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below duet TIMEOUT
300.005 TIMEOUT
above TIMEOUT
300.006
Total Below Time = 300.005 (was 300.008)
Above Time = 300.006 (was 300.007)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below duet 1 OKAY
0.363 (0.413) PASS
above 4 OKAY
0.359 (0.406)
array_false-unreach-call2.c below duet 1 OKAY
0.361 (0.429) PASS
above 4 OKAY
0.372 (0.44)
array_false-unreach-call3.c below duet 1 OKAY
0.354 (0.401) PASS
above 4 OKAY
0.36 (0.413)
array_true-unreach-call1.c below duet 1 FAIL
0.354 (0.416) FAIL
above 4 FAIL
0.355 (0.397)
array_true-unreach-call2.c below duet 1 FAIL
0.366 (0.42) FAIL
above 4 FAIL
0.371 (0.438)
array_true-unreach-call3.c below duet 1 PASS
0.347 (0.417) PASS
above 4 PASS
0.351 (0.41)
array_true-unreach-call4.c below duet 1 FAIL
0.346 (0.41) FAIL
above 4 FAIL
0.344 (0.416)
const_false-unreach-call1.c below duet 1 OKAY
0.33 (0.4) PASS
above 4 OKAY
0.329 (0.395)
const_true-unreach-call1.c below duet 1 PASS
0.33 (0.389) PASS
above 4 PASS
0.326 (0.386)
diamond_false-unreach-call1.c below duet 1 OKAY
0.34 (0.408) PASS
above 4 OKAY
0.353 (0.42)
diamond_true-unreach-call1.c below duet 1 PASS
0.339 (0.412) PASS
above 4 PASS
0.34 (0.426)
diamond_true-unreach-call2.c below duet 1 PASS
0.373 (0.429) PASS
above 4 PASS
0.385 (0.45)
functions_false-unreach-call1.c below duet 3 OKAY
0.367 (0.448) PASS
above 4 OKAY
0.382 (0.464)
functions_true-unreach-call1.c below duet 3 PASS
0.371 (0.441) PASS
above 4 PASS
0.389 (0.46)
multivar_false-unreach-call1.c below duet 1 OKAY
0.326 (0.393) PASS
above 4 OKAY
0.33 (0.393)
multivar_true-unreach-call1.c below duet 1 PASS
0.337 (0.4) PASS
above 4 PASS
0.328 (0.399)
nested_false-unreach-call1.c below duet 1 OKAY
0.351 (0.415) PASS
above 4 OKAY
0.347 (0.414)
nested_true-unreach-call1.c below duet 1 PASS
0.339 (0.414) PASS
above 4 PASS
0.341 (0.404)
overflow_true-unreach-call1.c below duet 1 PASS
0.323 (0.39) PASS
above 4 PASS
0.328 (0.392)
phases_false-unreach-call1.c below duet 1 OKAY
0.341 (0.409) PASS
above 4 OKAY
0.35 (0.424)
phases_false-unreach-call2.c below duet 1 OKAY
0.362 (0.421) PASS
above 4 OKAY
0.353 (0.42)
phases_true-unreach-call1.c below duet 1 PASS
0.341 (0.422) PASS
above 4 PASS
0.343 (0.415)
phases_true-unreach-call2.c below duet 1 PASS
0.364 (0.425) PASS
above 4 PASS
0.359 (0.428)
simple_false-unreach-call1.c below duet 1 OKAY
0.326 (0.4) PASS
above 4 OKAY
0.327 (0.401)
simple_false-unreach-call2.c below duet 1 OKAY
0.324 (0.377) PASS
above 4 OKAY
0.324 (0.401)
simple_false-unreach-call3.c below duet 1 OKAY
0.327 (0.393) PASS
above 4 OKAY
0.322 (0.385)
simple_false-unreach-call4.c below duet 1 OKAY
0.323 (0.401) PASS
above 4 OKAY
0.322 (0.394)
simple_true-unreach-call1.c below duet 1 PASS
0.338 (0.394) PASS
above 4 PASS
0.324 (0.392)
simple_true-unreach-call2.c below duet 1 PASS
0.325 (0.382) PASS
above 4 PASS
0.319 (0.386)
simple_true-unreach-call3.c below duet 1 PASS
0.331 (0.403) PASS
above 4 PASS
0.329 (0.39)
simple_true-unreach-call4.c below duet 1 PASS
0.331 (0.379) PASS
above 4 PASS
0.323 (0.387)
underapprox_false-unreach-call1.c below duet 1 OKAY
0.322 (0.391) PASS
above 4 OKAY
0.339 (0.39)
underapprox_false-unreach-call2.c below duet 1 OKAY
0.329 (0.391) PASS
above 4 OKAY
0.341 (0.4)
underapprox_true-unreach-call1.c below duet 1 FAIL
0.337 (0.399) FAIL
above 4 FAIL
0.332 (0.4)
underapprox_true-unreach-call2.c below duet 1 PASS
0.328 PASS
above 4 PASS
0.327 (0.39)
Total Below Time = 11.966 (was 14.196)
Above Time = 12.024 (was 14.326)
/bat0/stac/Code/Ark2-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
0.886 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
0.968 (1.132)
apache-get-tag_true-unreach-call.c below duet 1 PASS
PASS
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
0.427 (0.516) PASS
PASS
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
above 4 PASS
PASS
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
PASS
PASS
FAIL
PASS
FAIL
0.428 (0.526)
down_true-unreach-call.c below duet 1 PASS
0.337 (0.412) PASS
above 4 PASS
0.345 (0.41)
fragtest_simple_true-unreach-call.c below duet 1 PASS
0.381 (0.474) PASS
above 4 PASS
0.389 (0.468)
half_2_true-unreach-call.c below duet 1 PASS
0.352 (0.433) PASS
above 4 PASS
0.36 (0.44)
heapsort_true-unreach-call.c below duet 1 FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
PASS
PASS
1.703 (1.986) FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
PASS
PASS
above 4 FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
PASS
PASS
1.715 (2.067)
id_build_true-unreach-call.c below duet 1 PASS
PASS
0.352 (0.419) PASS
PASS
above 4 PASS
PASS
0.359 (0.423)
id_trans_false-unreach-call.c below duet 1 OKAY
0.338 (0.411) PASS
above 4 OKAY
0.344 (0.409)
id_trans_true-unreach-call.c below duet 1 PASS
PASS
PASS
0.338 (0.39) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.343 (0.411)
large_const_true-unreach-call.c below duet 1 PASS
0.413 (0.479) PASS
above 4 PASS
0.408 (0.497)
MADWiFi-encode_ie_ok_true-unreach-call.c below duet 1 PASS
PASS
0.38 (0.439) PASS
PASS
above 4 PASS
PASS
0.378 (0.438)
nested6_true-unreach-call.c below duet 1 FAIL
FAIL
PASS
0.416 (0.524) FAIL
FAIL
PASS
above 4 FAIL
FAIL
PASS
0.436
nested9_true-unreach-call.c below duet 1 PASS
0.464 (0.551) PASS
above 4 PASS
0.468 (0.549)
nest-if3_true-unreach-call.c below duet 1 PASS
0.409 (0.483) PASS
above 4 PASS
0.389 (0.469)
NetBSD_loop_true-unreach-call.c below duet 1 PASS
PASS
0.369 (0.426) PASS
PASS
above 4 PASS
PASS
0.345 (0.414)
sendmail-close-angle_true-unreach-call.c below duet 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.373 (0.451) PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
above 4 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.372 (0.46)
seq_true-unreach-call.c below duet 1 PASS
0.385 (0.443) PASS
above 4 PASS
0.389 (0.458)
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
1.06 (1.247) 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.067 (1.326)
string_concat-noarr_true-unreach-call.c below duet 1 PASS
0.36 (0.424) PASS
above 4 PASS
0.365 (0.45)
up_true-unreach-call.c below duet 1 PASS
0.349 (0.414) PASS
above 4 PASS
0.342 (0.419)
Total Below Time = 10.092 (was 11.869)
Above Time = 10.21 (was 12.246)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below duet 1 PASS
0.334 (0.401) PASS
above 4 PASS
0.347 (0.413)
bhmr2007_true-unreach-call.c below duet 1 PASS
0.359 (0.437) PASS
above 4 PASS
0.355 (0.434)
cggmp2005b_true-unreach-call.c below duet 1 PASS
0.389 (0.465) PASS
above 4 PASS
0.388 (0.453)
cggmp2005_true-unreach-call.c below duet 1 PASS
0.323 (0.396) PASS
above 4 PASS
0.329 (0.395)
cggmp2005_variant_true-unreach-call.c below duet 1 PASS
0.33 (0.399) PASS
above 4 PASS
0.339 (0.41)
css2003_true-unreach-call.c below duet 1 PASS
0.455 (0.554) PASS
above 4 PASS
0.469 (0.574)
ddlm2013_true-unreach-call.c below duet 1 PASS
0.384 (0.455) PASS
above 4 PASS
0.41 (0.469)
gcnr2008_false-unreach-call.c below duet 1 OKAY
0.722 (0.844) PASS
above 4 OKAY
0.763 (0.888)
gj2007b_true-unreach-call.c below duet 1 PASS
FAIL
0.359 (0.44) PASS
FAIL
above 4 PASS
FAIL
0.374 (0.452)
gj2007_true-unreach-call.c below duet 1 PASS
0.355 (0.432) PASS
above 4 PASS
0.357 (0.427)
gr2006_true-unreach-call.c below duet 1 PASS
0.348 (0.425) PASS
above 4 PASS
0.351 (0.46)
gsv2008_true-unreach-call.c below duet 1 PASS
0.341 (0.414) PASS
above 4 PASS
0.342 (0.423)
hhk2008_true-unreach-call.c below duet 1 PASS
0.337 (0.398) PASS
above 4 PASS
0.339 (0.401)
jm2006_true-unreach-call.c below duet 1 PASS
0.354 (0.428) PASS
above 4 PASS
0.359 (0.423)
jm2006_variant_true-unreach-call.c below duet 1 PASS
0.363 (0.449) PASS
above 4 PASS
0.377 (0.456)
mcmillan2006_true-unreach-call.c below duet 1 FAIL
0.378 (0.459) FAIL
above 4 FAIL
0.386 (0.463)
Total Below Time = 6.131 (was 7.396)
Above Time = 6.285 (was 7.541)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below duet 1 PASS
0.327 (0.402) PASS
above 4 PASS
0.331 (0.385)
count_by_1_variant_true-unreach-call.c below duet 1 PASS
0.335 (0.418) PASS
above 4 PASS
0.336 (0.448)
count_by_2_true-unreach-call.c below duet 1 PASS
0.327 (0.394) PASS
above 4 PASS
0.321 (0.389)
count_by_k_true-unreach-call.c below duet 1 PASS
0.342 (0.422) PASS
above 4 PASS
0.341 (0.422)
count_by_nondet_true-unreach-call.c below duet 1 FAIL
0.351 (0.411) FAIL
above 4 FAIL
0.344 (0.419)
gauss_sum_true-unreach-call.c below duet 1 PASS
0.355 (0.416) PASS
above 4 PASS
0.355 (0.431)
half_true-unreach-call.c below duet 1 FAIL
0.363 (0.443) FAIL
above 4 FAIL
0.377 (0.453)
nested_true-unreach-call.c below duet 1 PASS
0.397 (0.456) PASS
above 4 PASS
0.391 (0.465)
Total Below Time = 2.797 (was 3.362)
Above Time = 2.796 (was 3.412)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below duet 1 OKAY
0.397 (0.469) PASS
above 4 OKAY
0.405 (0.473)
array_true-unreach-call.c below duet 1 FAIL
0.399 (0.473) FAIL
above 4 FAIL
0.401 (0.467)
bubble_sort_false-unreach-call.c below duet 4 OKAY
OKAY
102.613 (216.455) PASS
PASS
above 4 OKAY
OKAY
144.11 (243.725)
bubble_sort_true-unreach-call.c below duet 1 1.841 (2.279)
above 4 1.868 (2.234)
compact_false-unreach-call.c below duet 1 OKAY
0.372 (0.457) PASS
above 4 OKAY
0.38 (0.439)
count_up_down_false-unreach-call_true-termination.c below duet 1 OKAY
0.331 (0.419) PASS
above 4 OKAY
0.337 (0.397)
count_up_down_true-unreach-call_true-termination.c below duet 1 PASS
0.323 (0.406) PASS
above 4 PASS
0.337 (0.399)
eureka_01_false-unreach-call.c below duet 1 OKAY
1.57 (1.978) PASS
above 4 OKAY
1.586 (2.04)
eureka_01_true-unreach-call.c below duet 1 FAIL
1.406 (1.741) FAIL
above 4 FAIL
1.391 (1.831)
eureka_05_true-unreach-call.c below duet 1 FAIL
0.644 (0.741) FAIL
above 4 FAIL
0.664 (0.785)
for_bounded_loop1_false-unreach-call_true-termination.c below duet 1 OKAY
0.343 (0.41) PASS
above 4 OKAY
0.335 (0.414)
for_bounded_loop1_true-unreach-call_true-termination.c below duet 1 PASS
PASS
0.333 (0.414) PASS
PASS
above 4 PASS
PASS
0.339 (0.416)
for_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.321 (0.396) PASS
above 0 PASS
0.32 (0.384)
for_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.329 (0.386) PASS
above 0 PASS
0.329 (0.389)
heavy_false-unreach-call.c below duet 1 OKAY
0.461 (0.549) PASS
above 4 OKAY
0.455 (0.537)
heavy_true-unreach-call.c below duet 1 PASS
0.446 (0.557) PASS
above 4 PASS
0.447 (0.533)
insertion_sort_false-unreach-call.c below duet 1 OKAY
1.218 (1.435) PASS
above 4 OKAY
1.208 (1.434)
insertion_sort_true-unreach-call.c below duet 1 FAIL
0.575 (0.717) FAIL
above 4 FAIL
0.596 (0.677)
invert_string_false-unreach-call.c below duet 1 OKAY
0.475 (0.558) PASS
above 4 OKAY
0.463 (0.547)
invert_string_true-unreach-call.c below duet 1 FAIL
0.462 (0.558) FAIL
above 4 FAIL
0.473 (0.564)
linear_sea.ch_true-unreach-call.c below duet 1 FAIL
0.385 (0.453) FAIL
above 4 FAIL
0.398 (0.461)
linear_search_false-unreach-call.c below duet 1 OKAY
0.415 (0.503) PASS
above 4 OKAY
0.425 (0.52)
lu.cmp_true-unreach-call.c below duet 3 PASS
25.434 (31.136) PASS
above 4 PASS
37.408 (45.961)
ludcmp_false-unreach-call.c below duet 3 OKAY
25.941 (32.201) PASS
above 4 OKAY
37.239 (46.064)
matrix_false-unreach-call_true-termination.c below duet 1 OKAY
0.627 (0.719) PASS
above 4 OKAY
0.644 (0.727)
matrix_true-unreach-call_true-termination.c below duet 1 FAIL
0.446 (0.514) FAIL
above 4 FAIL
0.438 (0.519)
n.c11_true-unreach-call.c below duet 3 FAIL
0.44 (0.513) FAIL
above 4 FAIL
0.526 (0.623)
n.c24_false-unreach-call.c below duet 3 OKAY
4.932 (5.985) PASS
above 4 OKAY
14.569 (18.972)
n.c40_true-unreach-call.c below duet 1 FAIL
0.368 (0.429) FAIL
above 4 FAIL
0.377 (0.443)
nec11_false-unreach-call.c below duet 1 OKAY
0.371 (0.447) PASS
above 4 OKAY
0.371 (0.431)
nec20_false-unreach-call.c below duet 1 OKAY
0.381 (0.438) PASS
above 4 OKAY
0.378 (0.459)
nec40_true-unreach-call.c below duet 1 FAIL
0.374 (0.443) FAIL
above 4 FAIL
0.389 (0.447)
string_false-unreach-call.c below duet 1 OKAY
0.554 (0.672) PASS
above 4 OKAY
0.588 (0.715)
string_true-unreach-call.c below duet 1 FAIL
0.546 (0.651) FAIL
above 4 FAIL
0.595 (0.71)
sum01_bug02_false-unreach-call_true-termination.c below duet 1 OKAY
0.388 (0.474) PASS
above 4 OKAY
0.404 (0.497)
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below duet 1 OKAY
0.357 (0.431) PASS
above 4 OKAY
0.351 (0.425)
sum01_false-unreach-call_true-termination.c below duet 1 OKAY
0.371 (0.459) PASS
above 4 OKAY
0.384 (0.453)
sum01_true-unreach-call_true-termination.c below duet 1 PASS
0.341 (0.418) PASS
above 4 PASS
0.356 (0.41)
sum03_false-unreach-call_true-termination.c below duet 1 OKAY
0.433 (0.54) PASS
above 0 OKAY
0.435 (0.518)
sum03_true-unreach-call_false-termination.c below duet 1 PASS
0.359 (0.426) PASS
above 4 PASS
0.356 (0.428)
sum04_false-unreach-call_true-termination.c below duet 1 OKAY
0.362 (0.441) PASS
above 4 OKAY
0.365 (0.441)
sum04_true-unreach-call_true-termination.c below duet 1 PASS
0.329 (0.402) PASS
above 4 PASS
0.332 (0.373)
sum_array_false-unreach-call.c below duet 1 OKAY
0.536 (0.645) PASS
above 4 OKAY
0.55 (0.663)
sum_array_true-unreach-call.c below duet 1 FAIL
0.582 (0.694) FAIL
above 4 FAIL
0.611 (0.707)
terminator_01_false-unreach-call_false-termination.c below duet 1 OKAY
0.347 (0.395) PASS
above 4 OKAY
0.339 (0.398)
terminator_02_false-unreach-call_true-termination.c below duet 3 OKAY
0.401 (0.496) PASS
above 4 OKAY
0.468 (0.532)
terminator_02_true-unreach-call_true-termination.c below duet 2 PASS
0.36 (0.422) PASS
above 4 PASS
0.407 (0.489)
terminator_03_false-unreach-call_true-termination.c below duet 1 OKAY
0.334 (0.414) PASS
above 4 OKAY
0.335 (0.414)
terminator_03_true-unreach-call_true-termination.c below duet 1 PASS
0.346 (0.405) PASS
above 4 PASS
0.35 (0.417)
trex01_false-unreach-call_true-termination.c below duet 3 OKAY
0.438 (0.538) PASS
above 4 OKAY
0.585 (0.705)
trex01_true-unreach-call.c below duet 3 PASS
0.688 (0.805) PASS
above 4 PASS
1.402 (1.77)
trex02_false-unreach-call_true-termination.c below duet 3 OKAY
0.378 (0.469) PASS
above 4 OKAY
0.427 (0.509)
trex02_true-unreach-call_true-termination.c below duet 3 PASS
0.378 (0.448) PASS
above 4 PASS
0.432 (0.519)
trex03_false-unreach-call_true-termination.c below duet 3 OKAY
0.654 (0.781) PASS
above 4 OKAY
1.009 (1.254)
trex03_true-unreach-call.c below duet 3 PASS
0.641 (0.779) PASS
above 4 PASS
0.988 (1.188)
trex04_true-unreach-call_false-termination.c below duet 1 PASS
0.392 (0.478) PASS
above 4 PASS
0.632 (0.785)
veris.c_NetBSD-libc__loop_true-unreach-call.c below duet 1 PASS
0.352 (0.409) PASS
above 4 PASS
0.351 (0.426)
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below duet 3 9.437 (11.566)
above 4 14.576 (17.917)
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below duet 1 PASS
0.354 (0.454) PASS
above 4 PASS
0.359 (0.44)
verisec_NetBSD-libc__loop_false-unreach-call.c below duet 1 OKAY
0.353 (0.421) PASS
above 4 OKAY
0.357 (0.432)
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below duet 3 OKAY
5.885 (7.087) PASS
above 4 OKAY
10.074 (12.456)
vogal_false-unreach-call.c below duet 1 OKAY
0.64 (0.793) PASS
above 4 OKAY
0.64 (0.797)
vogal_true-unreach-call.c below duet 1 FAIL
0.649 (0.777) FAIL
above 4 FAIL
0.671 (0.774)
while_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.323 (0.384) PASS
above 0 PASS
0.335
while_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.328 (0.374) PASS
above 0 PASS
0.318 (0.399)
while_infinite_loop_3_true-unreach-call_false-termination.c below duet 1 PASS
0.33 (0.397) PASS
above 4 PASS
0.319 (0.387)
while_infinite_loop_4_false-unreach-call_true-termination.c below duet 1 OKAY
0.331 (0.393) PASS
above 4 OKAY
0.322 (0.397)
Total Below Time = 204.47 (was 340.917)
Above Time = 290.629 (was 424.424)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below duet 7 PASS
1.007 (1.238) FAIL
above 4 FAIL
1.963 (2.333)
Ackermann02_false-unreach-call_false-termination.c below duet 7 OKAY
1.008 (1.171) PASS
above 4 OKAY
1.896 (2.273)
Ackermann03_true-unreach-call.c below duet 7 FAIL
1.034 (1.215) FAIL
above 4 FAIL
1.953 (2.307)
Ackermann04_true-unreach-call.c below duet 7 FAIL
1.006 (1.213) FAIL
above 4 FAIL
1.919 (2.275)
Addition01_true-unreach-call_true-termination.c below duet 2 PASS
0.481 (0.592) PASS
above 4 PASS
0.558 (0.691)
Addition02_false-unreach-call_false-termination.c below duet 2 OKAY
0.476 (0.563) PASS
above 4 OKAY
0.55 (0.643)
Addition03_false-no-overflow.c below duet 2 PASS
0.476 (0.583) PASS
above 4 PASS
0.543 (0.645)
Addition03_true-unreach-call.c below duet 2 PASS
0.514 (0.576) PASS
above 4 PASS
0.55 (0.67)
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below duet 2 OKAY
0.417 (0.499) PASS
above 4 OKAY
0.463 (0.535)
EvenOdd01_true-unreach-call_true-termination.c below duet 2 PASS
0.421 (0.502) FAIL
above 4 PASS
0.441 (0.546)
EvenOdd03_false-unreach-call_false-termination.c below duet 2 OKAY
0.41 (0.478) PASS
above 4 OKAY
0.447 (0.525)
Fibonacci01_true-unreach-call.c below duet TIMEOUT
300.007 FAIL
above 4 FAIL
1.061 (1.212)
Fibonacci02_true-unreach-call_true-termination.c below duet TIMEOUT
300.004 FAIL
above 4 FAIL
0.889 (1.065)
Fibonacci03_true-unreach-call_true-termination.c below duet TIMEOUT
300.007 FAIL
above 4 FAIL
1.048 (1.214)
Fibonacci04_false-unreach-call_true-termination.c below duet TIMEOUT
300.007 PASS
above 4 OKAY
1.339 (1.613)
Fibonacci05_false-unreach-call_true-termination.c below duet TIMEOUT
300.007 PASS
above 4 OKAY
1.033 (1.206)
gcd01_true-unreach-call_true-termination.c below duet 2 PASS
0.464 (0.536) FAIL
above 4 PASS
0.526 (0.646)
gcd02_true-unreach-call.c below duet 2 FAIL
PASS
0.834 (1.022) FAIL
PASS
above 4 FAIL
PASS
1.059 (1.271)
McCarthy91_false-unreach-call_false-termination.c below duet 7 OKAY
0.628 (0.767) PASS
above 4 OKAY
0.717 (0.848)
McCarthy91_true-unreach-call.c below duet 7 PASS
0.619 (0.736) FAIL
above 4 FAIL
0.694 (0.864)
MultCommutative_true-unreach-call_true-termination.c below duet 2 FAIL
0.485 (0.569) FAIL
above 4 FAIL
0.579 (0.744)
Primes_true-unreach-call.c below duet 3 FAIL
1.183 (1.43) FAIL
above 4 FAIL
9.29 (10.588)
recHanoi01_true-unreach-call_true-termination.c below duet 6 FAIL
11.967 (13.717) FAIL
above 4 FAIL
2.895 (3.512)
recHanoi02_true-unreach-call_true-termination.c below duet 2 FAIL
0.37 (0.501) FAIL
above 4 FAIL
0.427 (0.502)
recHanoi03_true-unreach-call_true-termination.c below duet 2 FAIL
0.386 (0.495) FAIL
above 4 FAIL
0.404 (0.547)
Total Below Time = 1524.218 (was 1528.444)
Above Time = 33.244 (was 39.275)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive-simple
afterrec_2calls_false-unreach-call.c below duet 2 OKAY
OKAY
0.397 (0.474) PASS
PASS
above 4 OKAY
OKAY
0.429 (0.5)
afterrec_2calls_true-unreach-call.c below duet 2 PASS
PASS
0.383 (0.466) PASS
PASS
above 4 PASS
PASS
0.411 (0.48)
afterrec_false-unreach-call.c below duet 2 OKAY
0.359 (0.427) PASS
above 4 OKAY
0.376 (0.446)
afterrec_true-unreach-call.c below duet 2 PASS
0.352 (0.421) PASS
above 4 PASS
0.369 (0.441)
fibo_10_false-unreach-call.c below duet TIMEOUT
300.004 PASS
above 4 OKAY
0.897 (1.052)
fibo_10_true-unreach-call.c below duet TIMEOUT
300.008 FAIL
above 4 FAIL
0.915 (1.067)
fibo_15_false-unreach-call.c below duet TIMEOUT
300.008 PASS
above 4 OKAY
0.881 (1.062)
fibo_15_true-unreach-call.c below duet TIMEOUT
300.004 FAIL
above 4 FAIL
0.889 (1.036)
fibo_20_false-unreach-call.c below duet TIMEOUT
300.008 PASS
above 4 OKAY
0.897 (1.063)
fibo_20_true-unreach-call.c below duet TIMEOUT
300.008 FAIL
above 4 FAIL
0.9 (1.054)
fibo_25_false-unreach-call.c below duet TIMEOUT
300.005 PASS
above 4 OKAY
0.901 (1.07)
fibo_25_true-unreach-call.c below duet TIMEOUT
300.004 FAIL
above 4 FAIL
0.896 (1.057)
fibo_2calls_10_false-unreach-call.c below duet 8 OKAY
203.669 PASS
above 4 OKAY
74.785 (94.08)
fibo_2calls_10_true-unreach-call.c below duet 8 FAIL
202.24 (225.542) FAIL
above 4 FAIL
77.134 (93.447)
fibo_2calls_15_false-unreach-call.c below duet 8 OKAY
201.43 (226.218) PASS
above 4 OKAY
72.187 (95.973)
fibo_2calls_15_true-unreach-call.c below duet 8 FAIL
200.809 (226.376) FAIL
above 4 FAIL
77.89 (96.617)
fibo_2calls_20_false-unreach-call.c below duet 8 OKAY
200.731 (224.531) PASS
above 4 OKAY
77.493 (93.581)
fibo_2calls_20_true-unreach-call.c below duet 8 FAIL
199.746 (227.781) FAIL
above 4 FAIL
77.21 (93.111)
fibo_2calls_25_false-unreach-call.c below duet 8 OKAY
202.238 (227.65) PASS
above 4 OKAY
77.441 (93.082)
fibo_2calls_25_true-unreach-call.c below duet 8 FAIL
205.836 (231.377) FAIL
above 4 FAIL
77.234 (93.947)
fibo_2calls_2_false-unreach-call.c below duet 8 OKAY
208.397 PASS
above 4 OKAY
75.53 (92.066)
fibo_2calls_2_true-unreach-call.c below duet 8 FAIL
201.361 FAIL
above 4 PASS
71.106 (92.695)
fibo_2calls_4_false-unreach-call.c below duet 8 OKAY
201.568 (225.471) PASS
above 4 OKAY
75.41 (92.327)
fibo_2calls_4_true-unreach-call.c below duet 8 FAIL
200.64 (225.346) FAIL
above 4 FAIL
75.394 (91.473)
fibo_2calls_5_false-unreach-call.c below duet 8 OKAY
202.818 PASS
above 4 OKAY
77.608 (94.253)
fibo_2calls_5_true-unreach-call.c below duet 8 FAIL
202.072 (229.928) FAIL
above 4 FAIL
72.69 (93.495)
fibo_2calls_6_false-unreach-call.c below duet 8 OKAY
202.65 (225.619) PASS
above 4 OKAY
77.14 (95.323)
fibo_2calls_6_true-unreach-call.c below duet 8 FAIL
201.124 (225.583) FAIL
above 4 FAIL
75.717 (93.139)
fibo_2calls_8_false-unreach-call.c below duet 8 OKAY
202.707 (230.012) PASS
above 4 OKAY
77.355 (94.16)
fibo_2calls_8_true-unreach-call.c below duet 8 FAIL
207.45 FAIL
above 4 FAIL
72.074 (93.436)
fibo_5_false-unreach-call.c below duet TIMEOUT
300.008 PASS
above 4 OKAY
0.924 (1.035)
fibo_5_true-unreach-call.c below duet TIMEOUT
300.008 FAIL
above 4 FAIL
0.891 (1.022)
fibo_7_false-unreach-call.c below duet TIMEOUT
300.007 PASS
above 4 OKAY
0.914 (1.063)
fibo_7_true-unreach-call.c below duet TIMEOUT
300.005 FAIL
above 4 FAIL
0.889 (1.055)
id2_b2_o3_true-unreach-call.c below duet 2 PASS
0.606 (0.753) FAIL
above 4 PASS
0.727 (0.874)
id2_b3_o2_false-unreach-call.c below duet 2 OKAY
0.627 (0.744) PASS
above 4 OKAY
0.746 (0.901)
id2_b3_o5_true-unreach-call.c below duet 2 PASS
0.618 (0.753) FAIL
above 4 PASS
0.743 (0.875)
id2_b5_o10_true-unreach-call.c below duet 2 PASS
0.634 (0.733) FAIL
above 4 PASS
0.751 (0.891)
id2_i5_o5_false-unreach-call.c below duet 2 OKAY
0.426 (0.523) PASS
above 4 OKAY
0.44 (0.532)
id2_i5_o5_true-unreach-call.c below duet 2 PASS
0.399 (0.483) PASS
above 4 PASS
0.442 (0.54)
id_b2_o3_true-unreach-call.c below duet 2 PASS
0.489 (0.568) FAIL
above 4 PASS
0.63 (0.745)
id_b3_o2_false-unreach-call.c below duet 2 OKAY
0.481 (0.6) PASS
above 4 OKAY
0.626 (0.764)
id_b3_o5_true-unreach-call.c below duet 2 PASS
0.495 (0.59) FAIL
above 4 PASS
0.623 (0.743)
id_b5_o10_true-unreach-call.c below duet 2 PASS
0.483 (0.591) FAIL
above 4 PASS
0.628 (0.725)
id_i10_o10_false-unreach-call.c below duet 2 OKAY
0.384 (0.456) PASS
above 4 OKAY
0.401 (0.481)
id_i10_o10_true-unreach-call.c below duet 2 PASS
0.367 (0.447) PASS
above 4 PASS
0.395 (0.484)
id_i15_o15_false-unreach-call.c below duet 2 OKAY
0.371 (0.44) PASS
above 4 OKAY
0.402 (0.472)
id_i15_o15_true-unreach-call.c below duet 2 PASS
0.368 (0.45) PASS
above 4 PASS
0.398 (0.475)
id_i20_o20_false-unreach-call.c below duet 2 OKAY
0.371 (0.444) PASS
above 4 OKAY
0.399 (0.476)
id_i20_o20_true-unreach-call.c below duet 2 PASS
0.373 (0.454) PASS
above 4 PASS
0.395 (0.461)
id_i25_o25_false-unreach-call.c below duet 2 OKAY
0.372 (0.441) PASS
above 4 OKAY
0.399 (0.477)
id_i25_o25_true-unreach-call.c below duet 2 PASS
0.374 (0.443) PASS
above 4 PASS
0.41 (0.46)
id_i5_o5_false-unreach-call.c below duet 2 OKAY
0.371 (0.446) PASS
above 4 OKAY
0.399 (0.497)
id_i5_o5_true-unreach-call.c below duet 2 PASS
0.367 (0.451) PASS
above 4 PASS
0.405 (0.469)
id_o1000_false-unreach-call.c below duet 2 OKAY
0.372 (0.445) PASS
above 4 OKAY
0.396 (0.492)
id_o100_false-unreach-call.c below duet 2 OKAY
0.374 (0.453) PASS
above 4 OKAY
0.412 (0.485)
id_o10_false-unreach-call.c below duet 2 OKAY
0.37 (0.443) PASS
above 4 OKAY
0.407 (0.481)
id_o200_false-unreach-call.c below duet 2 OKAY
0.384 (0.441) PASS
above 4 OKAY
0.415 (0.49)
id_o20_false-unreach-call.c below duet 2 OKAY
0.381 (0.448) PASS
above 4 OKAY
0.403 (0.486)
id_o3_false-unreach-call.c below duet 2 OKAY
0.371 (0.456) PASS
above 4 OKAY
0.405 (0.494)
sum_10x0_false-unreach-call.c below duet 2 OKAY
0.382 (0.478) PASS
above 4 OKAY
0.424 (0.505)
sum_10x0_true-unreach-call.c below duet 2 PASS
0.376 (0.457) PASS
above 4 PASS
0.416 (0.503)
sum_15x0_false-unreach-call.c below duet 2 OKAY
0.382 (0.445) PASS
above 4 OKAY
0.422 (0.521)
sum_15x0_true-unreach-call.c below duet 2 PASS
0.386 (0.465) PASS
above 4 PASS
0.418 (0.499)
sum_20x0_false-unreach-call.c below duet 2 OKAY
0.384 (0.473) PASS
above 4 OKAY
0.417 (0.492)
sum_20x0_true-unreach-call.c below duet 2 PASS
0.385 (0.466) PASS
above 4 PASS
0.431 (0.488)
sum_25x0_false-unreach-call.c below duet 2 OKAY
0.394 (0.471) PASS
above 4 OKAY
0.419 (0.52)
sum_25x0_true-unreach-call.c below duet 2 PASS
0.377 (0.48) PASS
above 4 PASS
0.42 (0.515)
sum_2x3_false-unreach-call.c below duet 2 OKAY
0.381 (0.463) PASS
above 4 OKAY
0.418 (0.507)
sum_2x3_true-unreach-call.c below duet 2 PASS
0.379 (0.452) PASS
above 4 PASS
0.415 (0.51)
sum_non_eq_false-unreach-call.c below duet 2 OKAY
0.411 (0.469) PASS
above 4 OKAY
0.455 (0.528)
sum_non_eq_true-unreach-call.c below duet 2 PASS
0.397 (0.469) PASS
above 4 PASS
0.463 (0.531)
sum_non_false-unreach-call.c below duet 2 OKAY
0.385 (0.466) PASS
above 4 OKAY
0.412 (0.503)
sum_non_true-unreach-call.c below duet 2 PASS
0.372 (0.468) PASS
above 4 PASS
0.413 (0.481)
Total Below Time = 7265.673 (was 7702.807)
Above Time = 1392.517 (was 1723.081)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/rec-sv-benchmarks/rec-loop-lit
rec-afnp2014_true-unreach-call.c below duet 2 PASS
0.37 (0.454) FAIL
above 4 PASS
0.391 (0.467)
rec-bhmr2007_true-unreach-call.c below duet 2 PASS
0.405 (0.489) FAIL
above 4 PASS
0.442 (0.505)
rec-cggmp2005b_true-unreach-call.c below duet 3 PASS
0.556 (0.672) FAIL
above 4 FAIL
2.039 (2.315)
rec-cggmp2005_true-unreach-call.c below duet 2 PASS
0.353 (0.426) FAIL
above 4 PASS
0.371 (0.437)
rec-cggmp2005_variant_true-unreach-call.c below duet 2 PASS
0.365 (0.461) FAIL
above 4 PASS
0.385 (0.482)
rec-css2003_true-unreach-call.c below duet 2 PASS
0.584 (0.701) PASS
above 4 PASS
0.653 (0.762)
rec-ddlm2013_true-unreach-call.c below duet 2 FAIL
0.44 (0.534) FAIL
above 4 FAIL
0.51 (0.621)
rec-gcnr2008_false-unreach-call.c below duet 2 OKAY
0.666 (0.821) PASS
above 4 OKAY
0.776 (0.935)
rec-gj2007b_true-unreach-call.c below duet 2 FAIL
FAIL
0.398 (0.457) FAIL
FAIL
above 4 FAIL
FAIL
0.427 (0.516)
rec-gj2007_true-unreach-call.c below duet 2 FAIL
0.388 (0.459) FAIL
above 4 FAIL
0.413 (0.494)
rec-gr2006_true-unreach-call.c below duet 2 FAIL
0.39 (0.466) FAIL
above 4 FAIL
0.418 (0.478)
rec-gsv2008_true-unreach-call.c below duet 2 PASS
0.358 (0.434) FAIL
above 4 PASS
0.388 (0.473)
rec-hhk2008_true-unreach-call.c below duet 2 PASS
0.354 (0.42) FAIL
above 4 PASS
0.376 (0.453)
rec-jm2006_true-unreach-call.c below duet 2 PASS
0.38 (0.459) PASS
above 4 PASS
0.405 (0.483)
rec-jm2006_variant_true-unreach-call.c below duet 2 PASS
0.388 (0.443) PASS
above 4 PASS
0.426 (0.525)
rec-mcmillan2006_true-unreach-call.c below duet 2 FAIL
0.418 (0.493) FAIL
above 4 FAIL
0.455 (0.553)
Total Below Time = 6.813 (was 8.189)
Above Time = 8.875 (was 10.499)
/bat0/stac/Code/Ark2-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.347 (0.421) FAIL
above 4 PASS
0.367 (0.432)
rec-count_by_1_variant_true-unreach-call.c below duet 2 PASS
0.359 (0.437) PASS
above 4 PASS
0.372 (0.451)
rec-count_by_2_true-unreach-call.c below duet 2 PASS
0.349 (0.418) FAIL
above 4 PASS
0.357 (0.445)
rec-count_by_k_true-unreach-call.c below duet 2 PASS
0.365 (0.43) FAIL
above 4 PASS
0.377 (0.464)
rec-count_by_nondet_true-unreach-call.c below duet 2 FAIL
0.371 (0.432) FAIL
above 4 FAIL
0.402 (0.463)
rec-gauss_sum_true-unreach-call.c below duet 2 PASS
0.398 (0.466) FAIL
above 4 PASS
0.418 (0.519)
rec-half_true-unreach-call.c below duet 2 FAIL
0.408 (0.472) FAIL
above 4 FAIL
0.436 (0.512)
rec-nested_true-unreach-call.c below duet 3 PASS
0.531 (0.614) FAIL
above 4 FAIL
1.373 (1.579)
Total Below Time = 3.128 (was 3.69)
Above Time = 4.102 (was 4.865)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below duet 2 PASS
0.457 (0.568) FAIL
above 4 PASS
0.518 (0.619)
cubic_polynomial_unsafe.c below duet 2 OKAY
0.463 (0.576) PASS
above 4 OKAY
0.521 (0.616)
edit_distance_bottom_up.c below duet 3 FAIL
75.098 (88.226) FAIL
above 4 FAIL
165.395 (193.648)
edit_distance_top_down.c below duet 3 FAIL
4.09 (4.882) FAIL
above TIMEOUT
300.112
log_log_n_solution.c below duet 3 FAIL
0.412 (0.499) FAIL
above 4 FAIL
0.496 (0.604)
log_log_n_solution_unsafe.c below duet 3 OKAY
0.428 (0.523) PASS
above 4 OKAY
0.489 (0.603)
log_n_solution.c below duet 2 FAIL
0.417 (0.51) FAIL
above 4 FAIL
0.485 (0.56)
log_n_solution_unsafe.c below duet 2 OKAY
0.423 PASS
above 4 OKAY
0.486 (0.563)
multivariate_1.c below duet TIMEOUT
300.007 TIMEOUT
above TIMEOUT
300.005
multivariate_1_unsafe.c below duet TIMEOUT
300.007 TIMEOUT
above TIMEOUT
300.004
multivariate_higher_order.c below duet 7 FAIL
FAIL
FAIL
2.299 (2.752) FAIL
FAIL
FAIL
above 4 FAIL
FAIL
FAIL
18.79 (22.211)
multivariate_higher_order_unsafe.c below duet 7 OKAY
OKAY
OKAY
2.319 (2.776) PASS
PASS
PASS
above 4 OKAY
OKAY
OKAY
18.62 (22.315)
n_cubed_solution.c below duet EXCEPTION
198.922 (225.973) FAIL
above 4 FAIL
16.343 (19.729)
n_cubed_solution_unsafe.c below duet EXCEPTION
0.026 (0.034)
above EXCEPTION
0.026 (0.034)
n_log_n_solution.c below duet 8 FAIL
0.949 (1.143) TIMEOUT
above 4 FAIL
4.737 (6.052)
n_log_n_solution_unsafe.c below duet 8 OKAY
0.916 (1.116) TIMEOUT
above 4 OKAY
6.427 (8.158)
n_squared_two_base_case_even.c below duet 2 PASS
0.398 (0.472) FAIL
above 4 PASS
0.429 (0.531)
n_squared_two_base_case_even_unsafe.c below duet 2 OKAY
0.389 (0.451) PASS
above 4 OKAY
0.422 (0.5)
n_squared_two_base_case_odd.c below duet 2 PASS
0.394 (0.478) FAIL
above 4 PASS
0.425 (0.521)
n_squared_two_base_case_odd_unsafe.c below duet 2 OKAY
0.387 (0.468) PASS
above 4 OKAY
0.429 (0.506)
pascals_dynamic.c below duet 3 FAIL
2.486 (2.932) FAIL
above 4 FAIL
6.252 (7.603)
pascals_dynamic_unsafe.c below duet 3 OKAY
2.461 (2.898) PASS
above 4 OKAY
6.164 (7.557)
pascals_iterative.c below duet 1 FAIL
2.097 (2.419) FAIL
above 4 FAIL
2.11 (2.48)
pascals_iterative_unsafe.c below duet 1 OKAY
2.095 (2.444) PASS
above 4 OKAY
2.097 (2.498)
pascals_recursive.c below duet 8 FAIL
4.267 (5.226) FAIL
above 4 FAIL
1.736 (2.077)
pascals_recursive_unsafe.c below duet 8 OKAY
4.318 (5.043) PASS
above 4 OKAY
1.702 (2.028)
squared_solution.c below duet 9 FAIL
3.155 (3.723) FAIL
above 4 FAIL
3.562 (4.511)
squared_solution_unsafe.c below duet 9 OKAY
3.205 (3.819) PASS
above 4 OKAY
4.099 (5.128)
two_n_even.c below duet 2 PASS
0.378 (0.472) PASS
above 4 PASS
0.407 (0.495)
two_n_even_unsafe.c below duet 2 OKAY
0.394 (0.465) PASS
above 4 OKAY
0.417 (0.501)
two_n_odd.c below duet 2 PASS
0.387 (0.463) PASS
above 4 PASS
0.409 (0.504)
two_n_odd_unsafe.c below duet 2 OKAY
0.38 (0.459) PASS
above 4 OKAY
0.414 (0.496)
two_to_n_over_two_even.c below duet TIMEOUT
300.005 FAIL
above 4 FAIL
1.157 (1.365)
two_to_n_over_two_even_unsafe.c below duet TIMEOUT
300.006 PASS
above 4 OKAY
1.151 (1.358)
two_to_n_over_two_odd.c below duet TIMEOUT
300.01 FAIL
above 4 FAIL
1.17 (1.381)
two_to_n_over_two_odd_unsafe.c below duet TIMEOUT
300.012 PASS
above 4 OKAY
1.166 (1.385)
two_to_n_squared.c below duet 5 FAIL
16.656 (20.447) FAIL
above 4 FAIL
3.441 (4.317)
two_to_n_squared_unsafe.c below duet 5 OKAY
16.948 (20.82) PASS
above 4 OKAY
3.429 (4.294)
two_to_two_to_n.c below duet 7 FAIL
0.775 (0.939) FAIL
above 4 FAIL
1.241 (1.45)
two_to_two_to_n_unsafe.c below duet 7 OKAY
0.765 (0.936) PASS
above 4 OKAY
1.213 (1.422)
Total Below Time = 2149.601 (was 2205.474)
Above Time = 1178.496 (was 1230.742)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below duet 1 FAIL
0.331 (0.413) FAIL
above 4 FAIL
0.367
adding_and_mult_unsafe.c below duet 1 OKAY
0.329 (0.397) PASS
above 4 OKAY
0.336 (0.408)
binary_search_array_tree.c below duet 1 FAIL
FAIL
0.539 (0.652) FAIL
FAIL
above 4 FAIL
FAIL
0.595 (0.702)
exp_add_linear.c below duet 1 FAIL
0.361 (0.438) FAIL
above 4 FAIL
0.383 (0.446)
exp_add_linear_unsafe.c below duet 1 OKAY
0.362 (0.446) PASS
above 4 OKAY
0.386 (0.452)
exp_add_loop_rec.c below duet 1 FAIL
0.349 (0.424) FAIL
above 4 FAIL
0.361 (0.433)
exp_add_loop_rec_unsafe.c below duet 1 OKAY
0.361 (0.418) PASS
above 4 OKAY
0.371 (0.448)
exp_add_loop_variable.c below duet 1 FAIL
0.368 (0.422) FAIL
above 4 FAIL
0.38 (0.448)
exp_add_loop_variable_unsafe.c below duet 1 OKAY
0.359 (0.436) PASS
above 4 OKAY
0.37 (0.413)
exp_with_linear_inner_loop.c below duet 1 FAIL
0.388 (0.47) FAIL
above 4 FAIL
0.413 (0.493)
exp_with_linear_inner_loop_unsafe.c below duet 1 OKAY
0.41 (0.476) PASS
above 4 OKAY
0.398 (0.493)
halving_log1.c below duet 1 FAIL
0.403 (0.47) FAIL
above 4 FAIL
0.413 (0.495)
linear_two_to_n.c below duet 6 FAIL
8.428 (9.846) FAIL
above 4 FAIL
1.259 (1.525)
linear_two_to_n_unsafe.c below duet 6 OKAY
7.333 (8.501) PASS
above 4 OKAY
1.27 (1.475)
loop_five_to_n.c below duet 1 FAIL
0.35 (0.431) FAIL
above 4 FAIL
0.37 (0.446)
loop_five_to_n_unsafe.c below duet 1 OKAY
0.354 (0.446) PASS
above 4 OKAY
0.373
non_loop_five_to_n.c below duet 6 TIMEOUT
300.005 (123.17) FAIL
above 4 FAIL
4.62 (5.764)
non_loop_five_to_n_unsafe.c below duet 6 OKAY
128.374 (300.011) PASS
above 4 OKAY
4.626 (5.753)
power_log.c below duet 1 FAIL
0.373 (0.477) FAIL
above 4 FAIL
0.4 (0.531)
power_log_modified.c below duet 1 FAIL
0.392 (0.52) FAIL
above 4 FAIL
0.422 (0.563)
simple_exponential.c below duet 1 FAIL
0.364 (0.445) FAIL
above 4 FAIL
0.366 (0.446)
simple_exponential_for.c below duet 1 FAIL
0.364 (0.45) FAIL
above 4 FAIL
0.367 (0.491)
simple_exponential_for_unsafe.c below duet 1 OKAY
0.41 PASS
above 4 OKAY
0.38 (0.459)
simple_exponential_unsafe.c below duet 1 OKAY
0.352 (0.439) PASS
above 4 OKAY
0.38 (0.436)
two_to_n_minus_n.c below duet 6 FAIL
8.0 (8.982) FAIL
above 4 FAIL
1.821 (2.194)
two_to_n_minus_n_loop.c below duet 6 FAIL
7.972 (9.525) FAIL
above 4 FAIL
1.825 (2.275)
two_to_n_minus_n_loop_unsafe.c below duet 6 OKAY
7.951 (9.366) PASS
above 4 OKAY
1.833 (2.226)
two_to_n_minus_n_unsafe.c below duet 6 OKAY
7.723 (8.932) PASS
above 4 OKAY
1.831 (2.192)
Total Below Time = 483.305 (was 487.452)
Above Time = 26.916 (was 32.815)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below duet 3 PASS
0.373 (0.47) PASS
PASS
PASS
above 4 PASS
0.425 (0.509)
02.c below duet 3 FAIL
0.516 (0.643) FAIL
PASS
PASS
above 4 FAIL
0.599 (0.714)
03.c below duet 1 PASS
0.382 (0.445) PASS
PASS
above 4 PASS
0.393 (0.464)
04.c below duet 1 PASS
0.323 (0.432) PASS
PASS
PASS
above 4 PASS
0.324 (0.401)
05.c below duet 3 PASS
0.487 (0.597) PASS
PASS
PASS
above 4 PASS
0.642 (0.763)
06.c below duet 5 FAIL
14.698 (8.563) FAIL
PASS
PASS
above 4 FAIL
9.144 (10.494)
07.c below duet 3 PASS
0.419 (0.489) PASS
PASS
PASS
above 4 PASS
0.482 (0.592)
08.c below duet 3 PASS
0.922 (1.126) PASS
PASS
PASS
above 4 PASS
2.182 (2.768)
09.c below duet 3 PASS
0.507 (0.622) PASS
PASS
PASS
above 4 PASS
0.789 (0.976)
10.c below duet 3 FAIL
0.632 (0.764) FAIL
PASS
PASS
above 4 FAIL
0.904 (1.078)
11.c below duet 1 PASS
0.332 (0.391) PASS
PASS
PASS
above 4 PASS
0.332 (0.391)
12.c below duet 3 PASS
0.591 (0.714) PASS
PASS
PASS
above 4 PASS
0.856 (1.041)
13.c below duet 3 PASS
0.418 (0.502) PASS
PASS
PASS
above 4 PASS
0.494 (0.599)
14.c below duet 3 PASS
PASS
0.387 (0.485) PASS
PASS
PASS
PASS
above 4 PASS
PASS
0.434 (0.531)
15.c below duet 1 PASS
0.339 (0.404) PASS
PASS
PASS
above 4 PASS
0.339 (0.398)
16.c below duet 1 PASS
0.353 (0.441) PASS
PASS
PASS
above 4 PASS
0.372 (0.444)
17.c below duet 1 PASS
0.373 (0.444) PASS
PASS
PASS
above 4 PASS
0.388 (0.464)
18.c below duet 1 PASS
0.349 (0.43) PASS
PASS
PASS
above 4 PASS
0.366 (0.436)
19.c below duet 1 PASS
0.368 (0.443) PASS
PASS
PASS
above 4 PASS
0.371 (0.479)
20.c below duet 3 PASS
PASS
FAIL
0.474 (0.585) PASS
PASS
FAIL
PASS
PASS
above 4 PASS
PASS
FAIL
0.647 (0.786)
21.c below duet 3 PASS
0.432 (0.503) PASS
PASS
PASS
above 4 PASS
0.506 (0.594)
22.c below duet 3 FAIL
PASS
0.459 (0.551) FAIL
PASS
PASS
PASS
above 4 FAIL
PASS
0.563 (0.669)
23.c below duet 1 PASS
0.338 (0.397) PASS
PASS
PASS
above 4 PASS
0.333 (0.402)
24.c below duet 1 PASS
0.369 (0.452) PASS
PASS
PASS
above 4 PASS
0.369 (0.437)
25.c below duet 3 FAIL
0.965 (1.166) FAIL
PASS
PASS
above 4 FAIL
1.577 (1.952)
26.c below duet 3 FAIL
97.481 (109.993) TIMEOUT
above 4 FAIL
217.993 (256.955)
27.c below duet 1 PASS
0.388 (0.475) PASS
PASS
PASS
above 4 PASS
0.404 (0.467)
28.c below duet 3 PASS
0.388 (0.482) PASS
PASS
PASS
above 4 PASS
0.428 (0.533)
29.c below duet 3 PASS
0.761 (0.894) PASS
PASS
PASS
above 4 PASS
1.083 (1.309)
30.c below duet 1 PASS
0.327 (0.385) PASS
PASS
PASS
above 4 PASS
0.329 (0.402)
31.c below duet 3 PASS
PASS
0.635 (0.77) PASS
PASS
PASS
PASS
above 4 PASS
PASS
0.923 (1.078)
32.c below duet 1 FAIL
0.35 (0.434) FAIL
PASS
PASS
above 4 FAIL
0.357 (0.437)
33.c below duet 3 PASS
0.801 (0.968) PASS
PASS
PASS
above 4 PASS
1.312 (1.584)
34.c below duet 1 FAIL
0.361 (0.428) FAIL
PASS
PASS
above 4 FAIL
0.36 (0.437)
35.c below duet 1 PASS
0.327 (0.39) PASS
PASS
PASS
above 4 PASS
0.323 (0.36)
36.c below duet 3 PASS
1.874 (2.318) PASS
PASS
PASS
above 4 PASS
3.398 (4.374)
37.c below duet 3 FAIL
0.391 (0.495) FAIL
PASS
PASS
above 4 FAIL
0.466 (0.572)
38.c below duet 1 FAIL
0.354 (0.419) FAIL
PASS
PASS
above 4 FAIL
0.358 (0.433)
39.c below duet 3 PASS
PASS
0.394 (0.469) PASS
PASS
PASS
PASS
above 4 PASS
PASS
0.452 (0.546)
40.c below duet 3 PASS
0.51 (0.608) PASS
PASS
PASS
above 4 PASS
0.697 (0.84)
41.c below duet 1 PASS
0.338 (0.429) PASS
PASS
PASS
above 4 PASS
0.366 (0.427)
42.c below duet 3 PASS
0.597 (0.718) PASS
PASS
PASS
above 4 PASS
0.82 (1.015)
43.c below duet 3 PASS
0.463 (0.534) PASS
PASS
PASS
above 4 PASS
0.57 (0.686)
44.c below duet 1 PASS
0.363 (0.437) PASS
PASS
PASS
above 4 PASS
0.361 (0.432)
45.c below duet 3 FAIL
1.644 (2.017) FAIL
PASS
PASS
above 4 FAIL
3.294 (3.998)
46.c below duet 3 FAIL
0.909 (1.098) FAIL
PASS
PASS
above 4 FAIL
1.367 (1.641)
Total Below Time = 135.462 (was 146.82)
Above Time = 259.492 (was 306.908)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below duet 1 PASS
0.365 (0.448) PASS
PASS
PASS
above 4 PASS
0.38 (0.462)
AGHKTW2017_foo.c below duet 1 PASS
0.357 (0.445) PASS
PASS
PASS
above 4 PASS
0.371 (0.461)
AGHKTW2017_loginSafe.c below duet 1 PASS
0.527 (0.617) PASS
PASS
PASS
above 4 PASS
0.578 (0.722)
AGHKTW2017_loopAndBranch_safe.c below duet 1 FAIL
0.39 (0.47) FAIL
PASS
PASS
above 4 FAIL
0.409 (0.5)
BCK2011_gauss.c below duet 1 PASS
0.367 (0.441) PASS
PASS
PASS
above 4 PASS
0.378 (0.429)
BCK2011_strength_reduction.c below duet 1 PASS
0.372 (0.457) PASS
PASS
PASS
above 4 PASS
0.381 (0.463)
BCK2011_strength_reduction_linear.c below duet 1 PASS
0.363 (0.437) PASS
PASS
PASS
above 4 PASS
0.369 (0.448)
fibonacci_information_flow.c below duet 1 FAIL
0.373 (0.446) FAIL
PASS
PASS
above 4 FAIL
0.391 (0.476)
TA2005_fib2.c below duet 1 FAIL
0.436 (0.498) FAIL
PASS
PASS
above 4 FAIL
0.437 (0.536)
TA2005_fib.c below duet 1 FAIL
0.361 (0.459) FAIL
PASS
PASS
above 4 FAIL
0.363 (0.444)
Total Below Time = 3.911 (was 4.718)
Above Time = 4.057 (was 4.941)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/canonical2017
boildown_11A.c below duet 2 0.531 (0.638)
above 4 0.624 (0.735)
c3_system.c below duet 3 PASS
PASS
PASS
1.136 (1.377) PASS
PASS
PASS
above 4 PASS
PASS
PASS
1.482 (1.777)
canonical11A_v_selfcomp.c below duet 2 0.875 (1.051)
above 4 1.657 (2.043)
canonical12_nv_selfcomp.c below duet 3 PASS
2.188 (2.689) PASS
above 4 PASS
4.558 (5.893)
canonical14_nv_selfcomp.c below duet 3 PASS
0.947 (1.152) PASS
above 4 PASS
1.344 (1.683)
canonical1_nv_selfcomp.c below duet 1 PASS
0.414 (0.491) PASS
above 4 PASS
0.447 (0.544)
canonical1_v_selfcomp.c below duet 1 0.467 (0.557)
above 4 0.504 (0.617)
canonical3_nv_selfcomp.c below duet 1 PASS
0.49 (0.607) PASS
above 4 PASS
0.556 (0.669)
canonical3_v_selfcomp.c below duet 1 0.56 (0.66)
above 4 0.66 (0.802)
canonical5_core.c below duet 3 0.505 (0.612)
above 4 0.595 (0.705)
canonical8_core.c below duet 1 0.603 (0.736)
above 4 0.663 (0.779)
Total Below Time = 8.716 (was 10.57)
Above Time = 13.09 (was 16.247)

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