[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.469 (0.389) FAIL
above 4 FAIL
0.471 (0.397)
kmp.c below duet 1 PASS
1.01 (0.844) PASS
above 4 PASS
1.097 (0.874)
qsort.c below duet 4 PASS
0.96 (0.827) FAIL
above 4 FAIL
4.373 (3.727)
speed_pldi09_fig1.c below duet 1 PASS
0.482 (0.401) PASS
above 4 PASS
0.473 (0.41)
speed_pldi09_fig4_2.c below duet 1 FAIL
0.492 (0.4) FAIL
above 4 FAIL
0.478 (0.4)
speed_pldi09_fig4_4.c below duet 1 PASS
0.53 (0.458) PASS
above 4 PASS
0.577 (0.464)
speed_pldi09_fig4_5.c below duet 1 PASS
0.471 (0.399) PASS
above 4 PASS
0.478 (0.395)
speed_pldi10_ex1.c below duet 1 PASS
0.927 (0.75) PASS
above 4 PASS
0.964 (0.774)
speed_pldi10_ex3.c below duet 1 PASS
0.507 (0.432) PASS
above 4 PASS
0.544 (0.43)
speed_pldi10_ex4.c below duet 1 PASS
0.439 PASS
above 4 PASS
0.512 (0.435)
speed_popl10_fig2_1.c below duet 1 PASS
0.492 (0.421) PASS
above 4 PASS
0.526 (0.409)
speed_popl10_fig2_2.c below duet 1 FAIL
0.451 (0.383) FAIL
above 4 FAIL
0.473 (0.39)
speed_popl10_nested_multiple.c below duet 1 PASS
0.532 (0.445) PASS
above 4 PASS
0.545 (0.444)
speed_popl10_nested_single.c below duet 1 PASS
0.508 (0.418) PASS
above 4 PASS
0.495 (0.429)
speed_popl10_sequential_single.c below duet 1 PASS
0.443 (0.379) PASS
above 4 PASS
0.48 (0.374)
speed_popl10_simple_multiple.c below duet 1 PASS
0.517 (0.401) PASS
above 4 PASS
0.506 (0.405)
speed_popl10_simple_single_2.c below duet 1 PASS
0.542 (0.44) PASS
above 4 PASS
0.549 (0.458)
speed_popl10_simple_single.c below duet 1 PASS
0.444 (0.37) PASS
above 4 PASS
0.443 (0.37)
t07.c below duet 1 PASS
0.473 (0.398) PASS
above 4 PASS
0.488 (0.407)
t08.c below duet 1 PASS
0.469 (0.385) PASS
above 4 PASS
0.458 (0.381)
t09.c below duet 1 PASS
0.447 (0.372) PASS
above 4 PASS
0.426 (0.38)
t10.c below duet 1 PASS
0.456 (0.376) PASS
above 4 PASS
0.463 (0.388)
t11.c below duet 1 PASS
0.489 (0.429) PASS
above 4 PASS
0.507 (0.438)
t13.c below duet 1 FAIL
0.491 (0.409) FAIL
above 4 FAIL
0.507 (0.408)
t15.c below duet 1 PASS
0.472 (0.394) PASS
above 4 PASS
0.474 (0.396)
t16.c below duet 1 PASS
0.473 (0.382) PASS
above 4 PASS
0.457 (0.396)
t19.c below duet 1 PASS
0.454 (0.389) PASS
above 4 PASS
0.457 (0.396)
t20.c below duet 1 PASS
0.453 (0.38) PASS
above 4 PASS
0.462 (0.388)
t27.c below duet 1 PASS
0.497 (0.434) PASS
above 4 PASS
0.542 (0.428)
t28.c below duet 1 PASS
0.491 (0.417) PASS
above 4 PASS
0.538 (0.44)
t30.c below duet 1 FAIL
0.503 (0.363) FAIL
above 4 FAIL
0.452 (0.387)
t37.c below duet 2 PASS
0.626 (0.498) FAIL
above 4 PASS
0.716 (0.591)
t39.c below duet 2 PASS
0.575 (0.473) FAIL
above 4 PASS
0.625 (0.509)
t46.c below duet 1 PASS
0.462 (0.382) PASS
above 4 PASS
0.494 (0.427)
t47.c below duet 1 PASS
0.463 (0.398) PASS
above 4 PASS
0.483 (0.397)
Total Below Time = 18.51 (was 15.444)
Above Time = 22.533 (was 18.742)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below duet 2 PASS
PASS
0.462 (0.403) PASS
PASS
above 4 PASS
PASS
0.525 (0.437)
qsort_full.c below duet 4 PASS
PASS
PASS
PASS
PASS
PASS
12.978 (10.67) PASS
PASS
PASS
PASS
PASS
PASS
above 4 FAIL
PASS
PASS
PASS
PASS
PASS
33.927 (28.758)
rec1-param_safe.c below duet 2 PASS
PASS
PASS
0.456 (0.356) PASS
FAIL
FAIL
above 4 PASS
PASS
PASS
0.481 (0.4)
rec1-param_unsafe.c below duet 2 OKAY
0.455 (0.368) PASS
above 4 OKAY
0.471 (0.408)
rec1_safe.c below duet 2 PASS
PASS
PASS
0.445 (0.373) PASS
FAIL
FAIL
above 4 PASS
PASS
PASS
0.465 (0.381)
rec1_unsafe.c below duet 2 OKAY
0.429 (0.368) PASS
above 4 OKAY
0.446 (0.377)
rec2-param_safe.c below duet 2 PASS
PASS
PASS
0.462 (0.373) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.467 (0.374)
rec2-param_unsafe.c below duet 2 OKAY
0.43 (0.381) PASS
above 4 OKAY
0.445 (0.386)
rec2_safe.c below duet 2 PASS
PASS
PASS
0.441 (0.353) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.455 (0.379)
rec2_unsafe.c below duet 2 OKAY
0.442 (0.371) PASS
above 4 OKAY
0.454 (0.381)
rec-test.c below duet 2 PASS
0.447 (0.368) FAIL
above 4 PASS
0.451 (0.363)
sas03_bothbranches.c below duet 7 PASS
0.795 (0.663) PASS
above 4 FAIL
1.553 (1.36)
sas03.c below duet 2 PASS
0.801 (0.691) PASS
above 4 PASS
1.026 (0.84)
simulated_lese_recursive.c below duet 2 PASS
0.468 (0.393) PASS
above 4 PASS
0.486 (0.434)
Total Below Time = 19.511 (was 16.131)
Above Time = 41.652 (was 35.278)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below duet 1 PASS
0.416 (0.356) PASS
above 4 PASS
0.429 (0.357)
count_up_down_unsafe.c below duet 1 OKAY
0.421 (0.355) PASS
above 4 OKAY
0.426 (0.34)
divide.c below duet 1 PASS
0.424 (0.356) PASS
above 4 PASS
0.439 (0.366)
factor_unsafe.c below duet 1 OKAY
0.424 (0.354) PASS
above 4 OKAY
0.417 (0.34)
for_infinite_loop_1_safe.c below duet 1 PASS
0.414 (0.342) PASS
above 0 PASS
0.427 (0.347)
for_infinite_loop_2_safe.c below duet 1 PASS
0.406 (0.348) PASS
above 0 PASS
0.393 (0.342)
interproc.c below duet 1 PASS
0.395 (0.348) PASS
above 4 PASS
0.383 (0.346)
mult.c below duet 1 PASS
PASS
0.407 (0.35) PASS
PASS
above 4 PASS
PASS
0.414 (0.356)
pointer_arith.c below duet 1 PASS
PASS
PASS
PASS
0.37 PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
0.409 (0.329)
quotient.c below duet 3 PASS
0.521 (0.441) PASS
above 4 PASS
0.546 (0.477)
subtract.c below duet 1 PASS
0.399 (0.349) PASS
above 4 PASS
0.404 (0.341)
sum01_bug02_sum01_bug02_base.case_unsafe.c below duet 1 OKAY
0.428 (0.371) PASS
above 4 OKAY
0.451 (0.369)
sum01_bug02_unsafe.c below duet 1 OKAY
0.493 (0.405) PASS
above 4 OKAY
0.494 (0.426)
sum01_real_safe.c below duet 1 PASS
0.42 (0.354) PASS
above 4 PASS
0.426 (0.358)
sum01_safe.c below duet 1 PASS
0.402 (0.353) PASS
above 4 PASS
0.416 (0.347)
sum01_unsafe.c below duet 1 OKAY
0.431 PASS
above 4 OKAY
0.446 (0.39)
sum02_safe.c below duet 1 PASS
0.431 (0.365) PASS
above 4 PASS
0.442 (0.365)
sum03_safe.c below duet 1 PASS
0.432 (0.357) PASS
above 0 PASS
0.422 (0.363)
sum03_unsafe.c below duet 1 OKAY
0.461 (0.406) PASS
above 0 OKAY
0.478 (0.42)
sum04_safe.c below duet 1 PASS
0.44 (0.356) PASS
above 4 PASS
0.406 (0.357)
sum04_unsafe.c below duet 1 OKAY
0.451 (0.365) PASS
above 4 OKAY
0.441 (0.372)
terminator_02_safe.c below duet 1 PASS
0.434 (0.347) PASS
above 4 PASS
0.395 (0.348)
terminator_02_unsafe.c below duet 1 OKAY
0.458 (0.379) PASS
above 4 OKAY
0.438 (0.368)
terminator_03_safe.c below duet 1 PASS
0.433 (0.359) PASS
above 4 PASS
0.42 (0.357)
terminator_03_unsafe.c below duet 1 OKAY
0.403 PASS
above 4 OKAY
0.418 (0.364)
token_ring01_safe.c below duet 4 FAIL
184.135 (150.061) FAIL
above 4 TIMEOUT
300.025
token_ring01_unsafe.c below duet 4 OKAY
224.806 (178.453) PASS
above TIMEOUT
300.045
toy_safe.c below duet EXCEPTION
236.172 TIMEOUT
above EXCEPTION
256.506 (217.149)
trex01_safe.c below duet 1 PASS
0.855 (0.76) PASS
above 4 PASS
0.45 (0.409)
trex01_unsafe.c below duet 1 OKAY
0.448 (0.401) PASS
above 4 OKAY
0.461 (0.399)
trex02_safe2.c below duet 3 PASS
0.483 (0.399) PASS
above 4 PASS
0.513 (0.438)
trex02_safe.c below duet 3 PASS
0.473 (0.398) PASS
above 4 PASS
0.505 (0.447)
trex02_unsafe.c below duet 3 OKAY
0.478 (0.41) PASS
above 4 OKAY
0.51 (0.457)
trex03_safe.c below duet 1 PASS
0.482 PASS
above 4 PASS
0.522 (0.466)
trex03_unsafe.c below duet 1 OKAY
0.492 (0.44) PASS
above 4 OKAY
0.504
trex04_safe.c below duet 1 PASS
0.426 (0.372) PASS
above 4 PASS
0.449 (0.398)
while_infinite_loop_1_safe.c below duet 1 PASS
0.372 PASS
above 0 PASS
0.384 (0.344)
while_infinite_loop_2_safe.c below duet 1 PASS
0.361 PASS
above 0 PASS
0.372 (0.33)
while_infinite_loop_3_safe.c below duet 1 PASS
0.379 PASS
above 4 PASS
0.392 (0.342)
Total Below Time = 661.076 (was 578.865)
Above Time = 872.418 (was 830.849)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below duet 3 PASS
0.464 (0.412) PASS
above 4 FAIL
0.651 (0.58)
blogger_simplified1.c below duet 3 PASS
0.864 PASS
above 4 PASS
1.501 (1.301)
divided_difference2.c below duet TIMEOUT
300.009 TIMEOUT
above TIMEOUT
300.006
mult-proc.c below duet 3 PASS
PASS
0.453 (0.392) PASS
PASS
above 4 PASS
PASS
0.461 (0.419)
mult-proc-params.c below duet 3 PASS
PASS
0.481 (0.431) PASS
PASS
above 4 PASS
PASS
0.525 (0.462)
popall.c below duet 1 PASS
PASS
PASS
PASS
PASS
0.481 PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
0.504 (0.441)
simulated_scc.c below duet 1 PASS
PASS
0.562 (0.504) PASS
PASS
above 4 PASS
PASS
0.563
Total Below Time = 303.314 (was 302.986)
Above Time = 304.211 (was 303.758)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below duet 1 PASS
0.424 PASS
above 4 PASS
0.438
degree2_binomial.c below duet 1 FAIL
0.545 (0.491) PASS
above 4 FAIL
0.599
degree2_monomial.c below duet 1 PASS
0.44 PASS
above 4 PASS
0.48 (0.427)
degree3_binomial.c below duet 1 PASS
0.913 PASS
above 4 PASS
0.981 (0.869)
degree3_monomial.c below duet 1 PASS
0.528 (0.432) PASS
above 4 PASS
0.54 (0.462)
degree4_binomial.c below duet 1 FAIL
1.561 (1.398) PASS
above 4 FAIL
1.648 (1.424)
degree4_monomial.c below duet 1 PASS
0.546 PASS
above 4 PASS
0.602 (0.53)
degree5_binomial.c below duet 1 FAIL
1.704 (1.498) PASS
above 4 FAIL
1.772 (1.542)
degree5_monomial.c below duet 1 PASS
0.69 (0.586) PASS
above 4 PASS
0.732 (0.665)
Total Below Time = 7.351 (was 6.607)
Above Time = 7.792 (was 6.878)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below duet 1 FAIL
0.436 (0.393) PASS
above 4 FAIL
0.44 (0.39)
cubic_with_square_interproc.c below duet 2 FAIL
0.502 (0.446) FAIL
above 4 FAIL
0.536 (0.469)
cubic_with_square_nonlinear.c below duet 1 FAIL
0.427 (0.384) PASS
above 4 FAIL
0.436 (0.394)
cubic_with_square_nonlinear_interproc.c below duet 2 FAIL
0.473 FAIL
above 4 FAIL
0.515 (0.461)
cubic_with_square_nonlinear_unsafe.c below duet 1 OKAY
0.433 (0.384) PASS
above 4 OKAY
0.455 (0.384)
cubic_with_square_unsafe.c below duet 1 OKAY
0.444 (0.382) PASS
above 4 OKAY
0.407
multi-input.c below duet 1 FAIL
0.515 (0.443) PASS
above 4 FAIL
0.515 (0.454)
multi-input_unsafe.c below duet 1 OKAY
0.53 (0.459) PASS
above 4 OKAY
0.531 (0.462)
nondet_loop_bound.c below duet 1 FAIL
0.43 (0.38) PASS
above 4 FAIL
0.429 (0.379)
nondet_loop_bound_quartic.c below duet 1 FAIL
0.451 (0.409) PASS
above 4 FAIL
0.456 (0.408)
nondet_loop_bound_quartic_unsafe.c below duet 1 OKAY
0.448 (0.38) PASS
above 4 OKAY
0.452 (0.391)
nondet_loop_bound_unsafe.c below duet 1 OKAY
0.419 (0.373) PASS
above 4 OKAY
0.42 (0.376)
nonlinear_stratified.c below duet 1 FAIL
0.447 (0.382) FAIL
above 4 FAIL
0.452 (0.393)
nonlinear_stratified_unsafe.c below duet 1 OKAY
0.438 PASS
above 4 OKAY
0.446
quartic_with_cube.c below duet 1 FAIL
0.452 (0.397) PASS
above 4 FAIL
0.443 (0.382)
quartic_with_cube_nonlinear.c below duet 1 FAIL
0.457 (0.412) PASS
above 4 FAIL
0.449 (0.394)
quartic_with_cube_nonlinear_unsafe.c below duet 1 OKAY
0.455 (0.403) PASS
above 4 OKAY
0.481 (0.408)
quartic_with_cube_unsafe.c below duet 1 OKAY
0.458 PASS
above 4 OKAY
0.438
quintic_with_quartic.c below duet 1 PASS
0.471 (0.39) PASS
above 4 PASS
0.465 (0.403)
quintic_with_quartic_nonlinear.c below duet 1 PASS
0.501 (0.436) PASS
above 4 PASS
0.483
quintic_with_quartic_nonlinear_unsafe.c below duet 1 OKAY
0.503 (0.445) PASS
above 4 OKAY
0.498 (0.45)
quintic_with_quartic_unsafe.c below duet 1 OKAY
0.487 (0.406) PASS
above 4 OKAY
0.454 (0.412)
Total Below Time = 10.177 (was 8.962)
Above Time = 10.201 (was 9.097)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below duet 1 PASS
0.595 (0.506) PASS
above 4 PASS
0.587 (0.524)
degree2_FD_AllAux_AllAssm.c below duet 1 PASS
2.136 (1.909) PASS
above 4 PASS
2.205 (1.932)
degree2_FD_AllAux_FewAssm.c below duet 1 PASS
2.095 (1.889) PASS
above 4 PASS
2.213 (1.917)
degree2_FD_FewAux_FewAssm.c below duet 1 PASS
0.759 (0.68) PASS
above 4 PASS
0.775 (0.689)
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below duet 1 PASS
0.774 (0.683) PASS
above 4 PASS
0.774
degree3.c below duet 1 PASS
0.652 (0.546) PASS
above 4 PASS
0.631 (0.557)
degree3_FD.c below duet 1 PASS
0.788 (0.689) PASS
above 4 PASS
0.802 (0.686)
degree4.c below duet 1 PASS
0.496 (0.442) PASS
above 4 PASS
0.505 (0.452)
Total Below Time = 8.295 (was 7.344)
Above Time = 8.492 (was 7.471)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below duet 1 PASS
0.474 (0.409) PASS
above 4 PASS
0.459
loop_unsafe.c below duet 1 OKAY
0.48 (0.421) PASS
above 4 OKAY
0.478 (0.425)
simulated_lese_parser.c below duet 1 PASS
0.407 (0.342) PASS
above 4 PASS
0.407 (0.357)
simulated_lese_sentinel.c below duet 1 PASS
0.41 (0.361) PASS
above 4 PASS
0.426 (0.363)
Total Below Time = 1.771 (was 1.533)
Above Time = 1.77 (was 1.568)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below duet 1 PASS
PASS
PASS
0.427 (0.363) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.428 (0.369)
Total Below Time = 0.427 (was 0.363)
Above Time = 0.428 (was 0.369)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below duet TIMEOUT
300.008 TIMEOUT
above TIMEOUT
300.007
Total Below Time = 300.008 (was 300.008)
Above Time = 300.007 (was 300.005)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below duet 1 OKAY
0.413 (0.351) PASS
above 4 OKAY
0.406 (0.337)
array_false-unreach-call2.c below duet 1 OKAY
0.429 (0.375) PASS
above 4 OKAY
0.44 (0.353)
array_false-unreach-call3.c below duet 1 OKAY
0.401 (0.333) PASS
above 4 OKAY
0.413 (0.363)
array_true-unreach-call1.c below duet 1 FAIL
0.416 FAIL
above 4 FAIL
0.397
array_true-unreach-call2.c below duet 1 FAIL
0.42 FAIL
above 4 FAIL
0.438 (0.371)
array_true-unreach-call3.c below duet 1 PASS
0.417 (0.349) PASS
above 4 PASS
0.41 (0.36)
array_true-unreach-call4.c below duet 1 FAIL
0.41 (0.346) FAIL
above 4 FAIL
0.416 (0.355)
const_false-unreach-call1.c below duet 1 OKAY
0.4 (0.355) PASS
above 4 OKAY
0.395 (0.344)
const_true-unreach-call1.c below duet 1 PASS
0.389 (0.347) PASS
above 4 PASS
0.386 (0.335)
diamond_false-unreach-call1.c below duet 1 OKAY
0.408 (0.353) PASS
above 4 OKAY
0.42 (0.363)
diamond_true-unreach-call1.c below duet 1 PASS
0.412 (0.364) PASS
above 4 PASS
0.426 (0.352)
diamond_true-unreach-call2.c below duet 1 PASS
0.429 (0.363) PASS
above 4 PASS
0.45 (0.377)
functions_false-unreach-call1.c below duet 3 OKAY
0.448 (0.366) PASS
above 4 OKAY
0.464 (0.386)
functions_true-unreach-call1.c below duet 3 PASS
0.441 (0.355) PASS
above 4 PASS
0.46 (0.4)
multivar_false-unreach-call1.c below duet 1 OKAY
0.393 (0.348) PASS
above 4 OKAY
0.393 (0.353)
multivar_true-unreach-call1.c below duet 1 PASS
0.4 (0.347) PASS
above 4 PASS
0.399
nested_false-unreach-call1.c below duet 1 OKAY
0.415 (0.361) PASS
above 4 OKAY
0.414 (0.353)
nested_true-unreach-call1.c below duet 1 PASS
0.414 (0.359) PASS
above 4 PASS
0.404 (0.341)
overflow_true-unreach-call1.c below duet 1 PASS
0.39 (0.32) PASS
above 4 PASS
0.392 (0.333)
phases_false-unreach-call1.c below duet 1 OKAY
0.409 (0.356) PASS
above 4 OKAY
0.424 (0.343)
phases_false-unreach-call2.c below duet 1 OKAY
0.421 (0.364) PASS
above 4 OKAY
0.42 (0.367)
phases_true-unreach-call1.c below duet 1 PASS
0.422 (0.367) PASS
above 4 PASS
0.415 (0.371)
phases_true-unreach-call2.c below duet 1 PASS
0.425 (0.375) PASS
above 4 PASS
0.428 (0.371)
simple_false-unreach-call1.c below duet 1 OKAY
0.4 (0.34) PASS
above 4 OKAY
0.401 (0.339)
simple_false-unreach-call2.c below duet 1 OKAY
0.377 (0.322) PASS
above 4 OKAY
0.401 (0.33)
simple_false-unreach-call3.c below duet 1 OKAY
0.393 (0.346) PASS
above 4 OKAY
0.385 (0.346)
simple_false-unreach-call4.c below duet 1 OKAY
0.401 (0.347) PASS
above 4 OKAY
0.394 (0.351)
simple_true-unreach-call1.c below duet 1 PASS
0.394 (0.34) PASS
above 4 PASS
0.392 (0.336)
simple_true-unreach-call2.c below duet 1 PASS
0.382 (0.345) PASS
above 4 PASS
0.386 (0.331)
simple_true-unreach-call3.c below duet 1 PASS
0.403 (0.344) PASS
above 4 PASS
0.39 (0.34)
simple_true-unreach-call4.c below duet 1 PASS
0.379 PASS
above 4 PASS
0.387 (0.343)
underapprox_false-unreach-call1.c below duet 1 OKAY
0.391 PASS
above 4 OKAY
0.39 (0.351)
underapprox_false-unreach-call2.c below duet 1 OKAY
0.391 PASS
above 4 OKAY
0.4 (0.344)
underapprox_true-unreach-call1.c below duet 1 FAIL
0.399 (0.35) FAIL
above 4 FAIL
0.4 (0.358)
underapprox_true-unreach-call2.c below duet 1 PASS
0.364 PASS
above 4 PASS
0.39 (0.352)
Total Below Time = 14.196 (was 12.362)
Above Time = 14.326 (was 12.389)
/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.947 (0.784) 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
1.132 (0.946)
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.516 (0.422) 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.526 (0.447)
down_true-unreach-call.c below duet 1 PASS
0.412 (0.353) PASS
above 4 PASS
0.41 (0.343)
fragtest_simple_true-unreach-call.c below duet 1 PASS
0.474 (0.386) PASS
above 4 PASS
0.468 (0.404)
half_2_true-unreach-call.c below duet 1 PASS
0.433 (0.373) PASS
above 4 PASS
0.44 (0.364)
heapsort_true-unreach-call.c below duet 1 FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
PASS
PASS
1.986 (1.733) 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
2.067 (1.719)
id_build_true-unreach-call.c below duet 1 PASS
PASS
0.419 (0.355) PASS
PASS
above 4 PASS
PASS
0.423 (0.354)
id_trans_false-unreach-call.c below duet 1 OKAY
0.411 (0.361) PASS
above 4 OKAY
0.409 (0.352)
id_trans_true-unreach-call.c below duet 1 PASS
PASS
PASS
0.39 (0.347) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.411 (0.338)
large_const_true-unreach-call.c below duet 1 PASS
0.479 (0.397) PASS
above 4 PASS
0.497 (0.407)
MADWiFi-encode_ie_ok_true-unreach-call.c below duet 1 PASS
PASS
0.439 (0.38) PASS
PASS
above 4 PASS
PASS
0.438 (0.37)
nested6_true-unreach-call.c below duet 1 FAIL
FAIL
PASS
0.524 (0.419) FAIL
FAIL
PASS
above 4 FAIL
FAIL
PASS
0.48
nested9_true-unreach-call.c below duet 1 PASS
0.551 (0.471) PASS
above 4 PASS
0.549 (0.478)
nest-if3_true-unreach-call.c below duet 1 PASS
0.483 (0.407) PASS
above 4 PASS
0.469 (0.408)
NetBSD_loop_true-unreach-call.c below duet 1 PASS
PASS
0.426 (0.346) PASS
PASS
above 4 PASS
PASS
0.414 (0.348)
sendmail-close-angle_true-unreach-call.c below duet 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.451 (0.389) PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
above 4 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.46 (0.382)
seq_true-unreach-call.c below duet 1 PASS
0.443 (0.391) PASS
above 4 PASS
0.458 (0.395)
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.247 (1.066) 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.326 (1.096)
string_concat-noarr_true-unreach-call.c below duet 1 PASS
0.424 (0.361) PASS
above 4 PASS
0.45 (0.369)
up_true-unreach-call.c below duet 1 PASS
0.414 (0.356) PASS
above 4 PASS
0.419 (0.348)
Total Below Time = 11.869 (was 10.097)
Above Time = 12.246 (was 10.311)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below duet 1 PASS
0.401 (0.343) PASS
above 4 PASS
0.413 (0.344)
bhmr2007_true-unreach-call.c below duet 1 PASS
0.437 (0.361) PASS
above 4 PASS
0.434 (0.384)
cggmp2005b_true-unreach-call.c below duet 1 PASS
0.465 (0.365) PASS
above 4 PASS
0.453 (0.365)
cggmp2005_true-unreach-call.c below duet 1 PASS
0.396 (0.323) PASS
above 4 PASS
0.395 (0.33)
cggmp2005_variant_true-unreach-call.c below duet 1 PASS
0.399 (0.344) PASS
above 4 PASS
0.41 (0.327)
css2003_true-unreach-call.c below duet 1 PASS
0.554 (0.461) PASS
above 4 PASS
0.574 (0.49)
ddlm2013_true-unreach-call.c below duet 1 PASS
0.455 (0.397) PASS
above 4 PASS
0.469 (0.411)
gcnr2008_false-unreach-call.c below duet 1 OKAY
0.844 (0.742) PASS
above 4 OKAY
0.888 (0.78)
gj2007b_true-unreach-call.c below duet 1 PASS
FAIL
0.44 (0.377) PASS
FAIL
above 4 PASS
FAIL
0.452 (0.392)
gj2007_true-unreach-call.c below duet 1 PASS
0.432 (0.349) PASS
above 4 PASS
0.427 (0.348)
gr2006_true-unreach-call.c below duet 1 PASS
0.425 (0.36) PASS
above 4 PASS
0.46 (0.357)
gsv2008_true-unreach-call.c below duet 1 PASS
0.414 (0.347) PASS
above 4 PASS
0.423 (0.337)
hhk2008_true-unreach-call.c below duet 1 PASS
0.398 (0.337) PASS
above 4 PASS
0.401 (0.352)
jm2006_true-unreach-call.c below duet 1 PASS
0.428 (0.366) PASS
above 4 PASS
0.423 (0.383)
jm2006_variant_true-unreach-call.c below duet 1 PASS
0.449 (0.379) PASS
above 4 PASS
0.456 (0.375)
mcmillan2006_true-unreach-call.c below duet 1 FAIL
0.459 (0.382) FAIL
above 4 FAIL
0.463 (0.389)
Total Below Time = 7.396 (was 6.233)
Above Time = 7.541 (was 6.364)
/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.402 (0.342) PASS
above 4 PASS
0.385 (0.327)
count_by_1_variant_true-unreach-call.c below duet 1 PASS
0.418 (0.345) PASS
above 4 PASS
0.448 (0.344)
count_by_2_true-unreach-call.c below duet 1 PASS
0.394 (0.317) PASS
above 4 PASS
0.389 (0.341)
count_by_k_true-unreach-call.c below duet 1 PASS
0.422 (0.363) PASS
above 4 PASS
0.422 (0.364)
count_by_nondet_true-unreach-call.c below duet 1 FAIL
0.411 (0.366) FAIL
above 4 FAIL
0.419 (0.363)
gauss_sum_true-unreach-call.c below duet 1 PASS
0.416 PASS
above 4 PASS
0.431 (0.384)
half_true-unreach-call.c below duet 1 FAIL
0.443 (0.375) FAIL
above 4 FAIL
0.453 (0.39)
nested_true-unreach-call.c below duet 1 PASS
0.456 PASS
above 4 PASS
0.465
Total Below Time = 3.362 (was 2.913)
Above Time = 3.412 (was 2.936)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below duet 1 OKAY
0.469 (0.419) PASS
above 4 OKAY
0.473 (0.419)
array_true-unreach-call.c below duet 1 FAIL
0.473 (0.424) FAIL
above 4 FAIL
0.467 (0.419)
bubble_sort_false-unreach-call.c below duet 4 OKAY
OKAY
216.455 (127.404) TIMEOUT
above 4 OKAY
OKAY
243.725 (190.441)
bubble_sort_true-unreach-call.c below duet 1 2.279 (1.942)
above 4 2.234 (1.991)
compact_false-unreach-call.c below duet 1 OKAY
0.457 (0.398) PASS
above 4 OKAY
0.439 (0.394)
count_up_down_false-unreach-call_true-termination.c below duet 1 OKAY
0.419 (0.364) PASS
above 4 OKAY
0.397
count_up_down_true-unreach-call_true-termination.c below duet 1 PASS
0.406 (0.341) PASS
above 4 PASS
0.399 (0.354)
eureka_01_false-unreach-call.c below duet 1 OKAY
1.978 (1.713) PASS
above 4 OKAY
2.04 (1.686)
eureka_01_true-unreach-call.c below duet 1 FAIL
1.741 (1.503) FAIL
above 4 FAIL
1.831 (1.511)
eureka_05_true-unreach-call.c below duet 1 FAIL
0.741 FAIL
above 4 FAIL
0.785 (0.673)
for_bounded_loop1_false-unreach-call_true-termination.c below duet 1 OKAY
0.41 (0.342) PASS
above 4 OKAY
0.414 (0.369)
for_bounded_loop1_true-unreach-call_true-termination.c below duet 1 PASS
PASS
0.414 (0.37) PASS
PASS
above 4 PASS
PASS
0.416 (0.366)
for_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.396 (0.339) PASS
above 0 PASS
0.384 (0.345)
for_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.386 (0.343) PASS
above 0 PASS
0.389 (0.35)
heavy_false-unreach-call.c below duet 1 OKAY
0.549 (0.486) PASS
above 4 OKAY
0.537 (0.484)
heavy_true-unreach-call.c below duet 1 PASS
0.557 (0.468) PASS
above 4 PASS
0.533 (0.479)
insertion_sort_false-unreach-call.c below duet 1 OKAY
1.435 (1.274) PASS
above 4 OKAY
1.434 (1.287)
insertion_sort_true-unreach-call.c below duet 1 FAIL
0.717 (0.619) FAIL
above 4 FAIL
0.677 (0.589)
invert_string_false-unreach-call.c below duet 1 OKAY
0.558 (0.468) PASS
above 4 OKAY
0.547 (0.495)
invert_string_true-unreach-call.c below duet 1 FAIL
0.558 (0.498) FAIL
above 4 FAIL
0.564 (0.475)
linear_sea.ch_true-unreach-call.c below duet 1 FAIL
0.453 (0.39) FAIL
above 4 FAIL
0.461
linear_search_false-unreach-call.c below duet 1 OKAY
0.503 (0.437) PASS
above 4 OKAY
0.52 (0.421)
lu.cmp_true-unreach-call.c below duet 3 PASS
31.136 (27.201) PASS
above 4 PASS
45.961 (39.372)
ludcmp_false-unreach-call.c below duet 3 OKAY
32.201 (27.966) PASS
above 4 OKAY
46.064 (40.12)
matrix_false-unreach-call_true-termination.c below duet 1 OKAY
0.719 PASS
above 4 OKAY
0.727 (0.648)
matrix_true-unreach-call_true-termination.c below duet 1 FAIL
0.514 (0.451) FAIL
above 4 FAIL
0.519 (0.45)
n.c11_true-unreach-call.c below duet 3 FAIL
0.513 FAIL
above 4 FAIL
0.623 (0.558)
n.c24_false-unreach-call.c below duet 3 OKAY
5.985 (5.285) PASS
above 4 OKAY
18.972 (16.007)
n.c40_true-unreach-call.c below duet 1 FAIL
0.429 (0.386) FAIL
above 4 FAIL
0.443 (0.379)
nec11_false-unreach-call.c below duet 1 OKAY
0.447 (0.373) PASS
above 4 OKAY
0.431 (0.38)
nec20_false-unreach-call.c below duet 1 OKAY
0.438 (0.384) PASS
above 4 OKAY
0.459 (0.403)
nec40_true-unreach-call.c below duet 1 FAIL
0.443 (0.389) FAIL
above 4 FAIL
0.447 (0.397)
string_false-unreach-call.c below duet 1 OKAY
0.672 (0.578) PASS
above 4 OKAY
0.715 (0.615)
string_true-unreach-call.c below duet 1 FAIL
0.651 (0.579) FAIL
above 4 FAIL
0.71 (0.635)
sum01_bug02_false-unreach-call_true-termination.c below duet 1 OKAY
0.474 (0.412) PASS
above 4 OKAY
0.497 (0.421)
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c below duet 1 OKAY
0.431 (0.376) PASS
above 4 OKAY
0.425 (0.364)
sum01_false-unreach-call_true-termination.c below duet 1 OKAY
0.459 (0.384) PASS
above 4 OKAY
0.453 (0.402)
sum01_true-unreach-call_true-termination.c below duet 1 PASS
0.418 PASS
above 4 PASS
0.41 (0.366)
sum03_false-unreach-call_true-termination.c below duet 1 OKAY
0.54 (0.442) PASS
above 0 OKAY
0.518 (0.45)
sum03_true-unreach-call_false-termination.c below duet 1 PASS
0.426 (0.381) PASS
above 4 PASS
0.428 (0.374)
sum04_false-unreach-call_true-termination.c below duet 1 OKAY
0.441 (0.392) PASS
above 4 OKAY
0.441 (0.391)
sum04_true-unreach-call_true-termination.c below duet 1 PASS
0.402 (0.36) PASS
above 4 PASS
0.373
sum_array_false-unreach-call.c below duet 1 OKAY
0.645 (0.553) PASS
above 4 OKAY
0.663 (0.566)
sum_array_true-unreach-call.c below duet 1 FAIL
0.694 (0.609) FAIL
above 4 FAIL
0.707 (0.623)
terminator_01_false-unreach-call_false-termination.c below duet 1 OKAY
0.395 (0.342) PASS
above 4 OKAY
0.398 (0.348)
terminator_02_false-unreach-call_true-termination.c below duet 3 OKAY
0.496 (0.413) PASS
above 4 OKAY
0.532
terminator_02_true-unreach-call_true-termination.c below duet 2 PASS
0.422 (0.376) PASS
above 4 PASS
0.489 (0.421)
terminator_03_false-unreach-call_true-termination.c below duet 1 OKAY
0.414 (0.355) PASS
above 4 OKAY
0.414 (0.364)
terminator_03_true-unreach-call_true-termination.c below duet 1 PASS
0.405 (0.358) PASS
above 4 PASS
0.417 (0.362)
trex01_false-unreach-call_true-termination.c below duet 3 OKAY
0.538 (0.473) PASS
above 4 OKAY
0.705 (0.571)
trex01_true-unreach-call.c below duet 3 PASS
0.805 (0.722) PASS
above 4 PASS
1.77 (1.551)
trex02_false-unreach-call_true-termination.c below duet 3 OKAY
0.469 (0.408) PASS
above 4 OKAY
0.509 (0.452)
trex02_true-unreach-call_true-termination.c below duet 3 PASS
0.448 (0.406) PASS
above 4 PASS
0.519 (0.46)
trex03_false-unreach-call_true-termination.c below duet 3 OKAY
0.781 (0.694) PASS
above 4 OKAY
1.254 (1.069)
trex03_true-unreach-call.c below duet 3 PASS
0.779 (0.678) PASS
above 4 PASS
1.188 (1.061)
trex04_true-unreach-call_false-termination.c below duet 1 PASS
0.478 (0.402) PASS
above 4 PASS
0.785 (0.686)
veris.c_NetBSD-libc__loop_true-unreach-call.c below duet 1 PASS
0.409 (0.356) PASS
above 4 PASS
0.426 (0.367)
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c below duet 3 11.566 (9.919)
above 4 17.917 (15.585)
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.c below duet 1 PASS
0.454 (0.396) PASS
above 4 PASS
0.44 (0.369)
verisec_NetBSD-libc__loop_false-unreach-call.c below duet 1 OKAY
0.421 (0.346) PASS
above 4 OKAY
0.432 (0.355)
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c below duet 3 OKAY
7.087 (6.026) PASS
above 4 OKAY
12.456 (10.554)
vogal_false-unreach-call.c below duet 1 OKAY
0.793 (0.639) PASS
above 4 OKAY
0.797 (0.672)
vogal_true-unreach-call.c below duet 1 FAIL
0.777 (0.68) FAIL
above 4 FAIL
0.774 (0.688)
while_infinite_loop_1_true-unreach-call_false-termination.c below duet 1 PASS
0.384 (0.34) PASS
above 0 PASS
0.367
while_infinite_loop_2_true-unreach-call_false-termination.c below duet 1 PASS
0.374 PASS
above 0 PASS
0.399 (0.344)
while_infinite_loop_3_true-unreach-call_false-termination.c below duet 1 PASS
0.397 (0.338) PASS
above 4 PASS
0.387 (0.33)
while_infinite_loop_4_false-unreach-call_true-termination.c below duet 1 OKAY
0.393 (0.339) PASS
above 4 OKAY
0.397 (0.343)
Total Below Time = 340.917 (was 235.653)
Above Time = 424.424 (was 346.418)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/recursive
Ackermann01_true-unreach-call.c below duet 7 PASS
1.238 (1.07) FAIL
above 4 FAIL
2.333 (2.071)
Ackermann02_false-unreach-call_false-termination.c below duet 7 OKAY
1.171 (0.997) PASS
above 4 OKAY
2.273 (1.911)
Ackermann03_true-unreach-call.c below duet 7 FAIL
1.215 (1.029) FAIL
above 4 FAIL
2.307 (2.022)
Ackermann04_true-unreach-call.c below duet 7 FAIL
1.213 (1.101) FAIL
above 4 FAIL
2.275 (1.993)
Addition01_true-unreach-call_true-termination.c below duet 2 PASS
0.592 (0.502) PASS
above 4 PASS
0.691 (0.577)
Addition02_false-unreach-call_false-termination.c below duet 2 OKAY
0.563 PASS
above 4 OKAY
0.643 (0.569)
Addition03_false-no-overflow.c below duet 2 PASS
0.583 (0.52) PASS
above 4 PASS
0.645 (0.555)
Addition03_true-unreach-call.c below duet 2 PASS
0.576 (0.487) PASS
above 4 PASS
0.67 (0.546)
BallRajamani-SPIN2000-Fig1_false-unreach-call.c below duet 2 OKAY
0.499 (0.421) PASS
above 4 OKAY
0.535 (0.477)
EvenOdd01_true-unreach-call_true-termination.c below duet 2 PASS
0.502 (0.441) FAIL
above 4 PASS
0.546 (0.46)
EvenOdd03_false-unreach-call_false-termination.c below duet 2 OKAY
0.478 PASS
above 4 OKAY
0.525 (0.473)
Fibonacci01_true-unreach-call.c below duet TIMEOUT
300.009 FAIL
above 4 FAIL
1.212 (1.091)
Fibonacci02_true-unreach-call_true-termination.c below duet TIMEOUT
300.009 FAIL
above 4 FAIL
1.065 (0.943)
Fibonacci03_true-unreach-call_true-termination.c below duet TIMEOUT
300.008 FAIL
above 4 FAIL
1.214 (1.079)
Fibonacci04_false-unreach-call_true-termination.c below duet TIMEOUT
300.006 PASS
above 4 OKAY
1.613 (1.37)
Fibonacci05_false-unreach-call_true-termination.c below duet TIMEOUT
300.009 PASS
above 4 OKAY
1.206 (1.065)
gcd01_true-unreach-call_true-termination.c below duet 2 PASS
0.536 (0.479) FAIL
above 4 PASS
0.646 (0.563)
gcd02_true-unreach-call.c below duet 2 FAIL
PASS
1.022 (0.887) FAIL
PASS
above 4 FAIL
PASS
1.271 (1.071)
McCarthy91_false-unreach-call_false-termination.c below duet 7 OKAY
0.767 (0.644) PASS
above 4 OKAY
0.848 (0.71)
McCarthy91_true-unreach-call.c below duet 7 PASS
0.736 (0.626) FAIL
above 4 FAIL
0.864 (0.739)
MultCommutative_true-unreach-call_true-termination.c below duet 2 FAIL
0.569 (0.507) FAIL
above 4 FAIL
0.744 (0.619)
Primes_true-unreach-call.c below duet 3 FAIL
1.43 (1.241) FAIL
above 4 FAIL
10.588 (9.501)
recHanoi01_true-unreach-call_true-termination.c below duet 6 FAIL
13.717 FAIL
above 4 FAIL
3.512 (2.946)
recHanoi02_true-unreach-call_true-termination.c below duet 2 FAIL
0.501 (0.407) FAIL
above 4 FAIL
0.502 (0.444)
recHanoi03_true-unreach-call_true-termination.c below duet 2 FAIL
0.495 (0.402) FAIL
above 4 FAIL
0.547 (0.428)
Total Below Time = 1528.444 (was 1525.331)
Above Time = 39.275 (was 34.223)
/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.474 (0.419) PASS
PASS
above 4 OKAY
OKAY
0.5 (0.435)
afterrec_2calls_true-unreach-call.c below duet 2 PASS
PASS
0.466 (0.379) PASS
PASS
above 4 PASS
PASS
0.48 (0.423)
afterrec_false-unreach-call.c below duet 2 OKAY
0.427 (0.383) PASS
above 4 OKAY
0.446 (0.403)
afterrec_true-unreach-call.c below duet 2 PASS
0.421 (0.378) PASS
above 4 PASS
0.441 (0.399)
fibo_10_false-unreach-call.c below duet TIMEOUT
300.01 PASS
above 4 OKAY
1.052 (0.931)
fibo_10_true-unreach-call.c below duet TIMEOUT
300.009 FAIL
above 4 FAIL
1.067 (0.906)
fibo_15_false-unreach-call.c below duet TIMEOUT
300.009 PASS
above 4 OKAY
1.062 (0.932)
fibo_15_true-unreach-call.c below duet TIMEOUT
300.005 FAIL
above 4 FAIL
1.036 (0.896)
fibo_20_false-unreach-call.c below duet TIMEOUT
300.009 PASS
above 4 OKAY
1.063 (0.902)
fibo_20_true-unreach-call.c below duet TIMEOUT
300.009 FAIL
above 4 FAIL
1.054 (0.935)
fibo_25_false-unreach-call.c below duet TIMEOUT
300.009 PASS
above 4 OKAY
1.07 (0.946)
fibo_25_true-unreach-call.c below duet TIMEOUT
300.009 FAIL
above 4 FAIL
1.057 (0.918)
fibo_2calls_10_false-unreach-call.c below duet 8 OKAY
226.152 PASS
above 4 OKAY
94.08 (82.702)
fibo_2calls_10_true-unreach-call.c below duet 8 FAIL
225.542 FAIL
above 4 FAIL
93.447 (81.618)
fibo_2calls_15_false-unreach-call.c below duet 8 OKAY
226.218 PASS
above 4 OKAY
95.973 (81.982)
fibo_2calls_15_true-unreach-call.c below duet 8 FAIL
226.376 FAIL
above 4 FAIL
96.617 (81.886)
fibo_2calls_20_false-unreach-call.c below duet 8 OKAY
224.531 PASS
above 4 OKAY
93.581 (82.495)
fibo_2calls_20_true-unreach-call.c below duet 8 FAIL
227.781 (206.237) FAIL
above 4 FAIL
93.111 (82.322)
fibo_2calls_25_false-unreach-call.c below duet 8 OKAY
227.65 PASS
above 4 OKAY
93.082 (82.671)
fibo_2calls_25_true-unreach-call.c below duet 8 FAIL
231.377 FAIL
above 4 FAIL
93.947 (80.897)
fibo_2calls_2_false-unreach-call.c below duet 8 OKAY
229.396 PASS
above 4 OKAY
92.066 (80.104)
fibo_2calls_2_true-unreach-call.c below duet 8 FAIL
223.617 FAIL
above 4 PASS
92.695 (79.465)
fibo_2calls_4_false-unreach-call.c below duet 8 OKAY
225.471 PASS
above 4 OKAY
92.327 (73.636)
fibo_2calls_4_true-unreach-call.c below duet 8 FAIL
225.346 FAIL
above 4 FAIL
91.473 (79.388)
fibo_2calls_5_false-unreach-call.c below duet 8 OKAY
224.96 PASS
above 4 OKAY
94.253 (82.43)
fibo_2calls_5_true-unreach-call.c below duet 8 FAIL
229.928 FAIL
above 4 FAIL
93.495 (82.123)
fibo_2calls_6_false-unreach-call.c below duet 8 OKAY
225.619 PASS
above 4 OKAY
95.323 (80.425)
fibo_2calls_6_true-unreach-call.c below duet 8 FAIL
225.583 FAIL
above 4 FAIL
93.139 (81.789)
fibo_2calls_8_false-unreach-call.c below duet 8 OKAY
230.012 (208.434) PASS
above 4 OKAY
94.16 (75.197)
fibo_2calls_8_true-unreach-call.c below duet 8 FAIL
225.341 (204.821) FAIL
above 4 FAIL
93.436 (80.07)
fibo_5_false-unreach-call.c below duet TIMEOUT
300.006 PASS
above 4 OKAY
1.035 (0.929)
fibo_5_true-unreach-call.c below duet TIMEOUT
300.009 FAIL
above 4 FAIL
1.022 (0.882)
fibo_7_false-unreach-call.c below duet TIMEOUT
300.009 PASS
above 4 OKAY
1.063 (0.939)
fibo_7_true-unreach-call.c below duet TIMEOUT
300.008 FAIL
above 4 FAIL
1.055 (0.932)
id2_b2_o3_true-unreach-call.c below duet 2 PASS
0.753 (0.645) FAIL
above 4 PASS
0.874 (0.742)
id2_b3_o2_false-unreach-call.c below duet 2 OKAY
0.744 (0.644) PASS
above 4 OKAY
0.901 (0.786)
id2_b3_o5_true-unreach-call.c below duet 2 PASS
0.753 (0.657) FAIL
above 4 PASS
0.875 (0.785)
id2_b5_o10_true-unreach-call.c below duet 2 PASS
0.733 (0.651) FAIL
above 4 PASS
0.891 (0.729)
id2_i5_o5_false-unreach-call.c below duet 2 OKAY
0.523 (0.408) PASS
above 4 OKAY
0.532 (0.437)
id2_i5_o5_true-unreach-call.c below duet 2 PASS
0.483 (0.426) PASS
above 4 PASS
0.54 (0.454)
id_b2_o3_true-unreach-call.c below duet 2 PASS
0.568 (0.507) FAIL
above 4 PASS
0.745 (0.663)
id_b3_o2_false-unreach-call.c below duet 2 OKAY
0.6 (0.507) PASS
above 4 OKAY
0.764 (0.663)
id_b3_o5_true-unreach-call.c below duet 2 PASS
0.59 (0.513) FAIL
above 4 PASS
0.743 (0.625)
id_b5_o10_true-unreach-call.c below duet 2 PASS
0.591 (0.49) FAIL
above 4 PASS
0.725 (0.639)
id_i10_o10_false-unreach-call.c below duet 2 OKAY
0.456 PASS
above 4 OKAY
0.481 (0.418)
id_i10_o10_true-unreach-call.c below duet 2 PASS
0.447 (0.39) PASS
above 4 PASS
0.484 (0.424)
id_i15_o15_false-unreach-call.c below duet 2 OKAY
0.44 PASS
above 4 OKAY
0.472 (0.416)
id_i15_o15_true-unreach-call.c below duet 2 PASS
0.45 (0.402) PASS
above 4 PASS
0.475 (0.4)
id_i20_o20_false-unreach-call.c below duet 2 OKAY
0.444 (0.399) PASS
above 4 OKAY
0.476 (0.425)
id_i20_o20_true-unreach-call.c below duet 2 PASS
0.454 (0.4) PASS
above 4 PASS
0.461
id_i25_o25_false-unreach-call.c below duet 2 OKAY
0.441 (0.389) PASS
above 4 OKAY
0.477 (0.431)
id_i25_o25_true-unreach-call.c below duet 2 PASS
0.443 (0.395) PASS
above 4 PASS
0.46 (0.414)
id_i5_o5_false-unreach-call.c below duet 2 OKAY
0.446 (0.388) PASS
above 4 OKAY
0.497 (0.389)
id_i5_o5_true-unreach-call.c below duet 2 PASS
0.451 (0.393) PASS
above 4 PASS
0.469 (0.402)
id_o1000_false-unreach-call.c below duet 2 OKAY
0.445 (0.385) PASS
above 4 OKAY
0.492 (0.438)
id_o100_false-unreach-call.c below duet 2 OKAY
0.453 (0.393) PASS
above 4 OKAY
0.485 (0.434)
id_o10_false-unreach-call.c below duet 2 OKAY
0.443 (0.4) PASS
above 4 OKAY
0.481 (0.436)
id_o200_false-unreach-call.c below duet 2 OKAY
0.441 (0.391) PASS
above 4 OKAY
0.49 (0.423)
id_o20_false-unreach-call.c below duet 2 OKAY
0.448 (0.407) PASS
above 4 OKAY
0.486 (0.41)
id_o3_false-unreach-call.c below duet 2 OKAY
0.456 (0.382) PASS
above 4 OKAY
0.494 (0.415)
sum_10x0_false-unreach-call.c below duet 2 OKAY
0.478 (0.393) PASS
above 4 OKAY
0.505 (0.454)
sum_10x0_true-unreach-call.c below duet 2 PASS
0.457 (0.412) PASS
above 4 PASS
0.503 (0.437)
sum_15x0_false-unreach-call.c below duet 2 OKAY
0.445 PASS
above 4 OKAY
0.521 (0.457)
sum_15x0_true-unreach-call.c below duet 2 PASS
0.465 PASS
above 4 PASS
0.499 (0.446)
sum_20x0_false-unreach-call.c below duet 2 OKAY
0.473 (0.397) PASS
above 4 OKAY
0.492 (0.439)
sum_20x0_true-unreach-call.c below duet 2 PASS
0.466 (0.386) PASS
above 4 PASS
0.488 (0.419)
sum_25x0_false-unreach-call.c below duet 2 OKAY
0.471 (0.377) PASS
above 4 OKAY
0.52 (0.425)
sum_25x0_true-unreach-call.c below duet 2 PASS
0.48 (0.393) PASS
above 4 PASS
0.515 (0.435)
sum_2x3_false-unreach-call.c below duet 2 OKAY
0.463 (0.392) PASS
above 4 OKAY
0.507 (0.435)
sum_2x3_true-unreach-call.c below duet 2 PASS
0.452 (0.387) PASS
above 4 PASS
0.51 (0.413)
sum_non_eq_false-unreach-call.c below duet 2 OKAY
0.469 (0.416) PASS
above 4 OKAY
0.528 (0.47)
sum_non_eq_true-unreach-call.c below duet 2 PASS
0.469 (0.422) PASS
above 4 PASS
0.531 (0.464)
sum_non_false-unreach-call.c below duet 2 OKAY
0.466 (0.418) PASS
above 4 OKAY
0.503 (0.426)
sum_non_true-unreach-call.c below duet 2 PASS
0.468 (0.415) PASS
above 4 PASS
0.481 (0.43)
Total Below Time = 7702.807 (was 7364.772)
Above Time = 1723.081 (was 1483.276)
/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.454 (0.399) FAIL
above 4 PASS
0.467 (0.413)
rec-bhmr2007_true-unreach-call.c below duet 2 PASS
0.489 (0.417) FAIL
above 4 PASS
0.505
rec-cggmp2005b_true-unreach-call.c below duet 3 PASS
0.672 (0.589) FAIL
above 4 FAIL
2.315 (2.03)
rec-cggmp2005_true-unreach-call.c below duet 2 PASS
0.426 (0.385) FAIL
above 4 PASS
0.437 (0.396)
rec-cggmp2005_variant_true-unreach-call.c below duet 2 PASS
0.461 (0.391) FAIL
above 4 PASS
0.482 (0.409)
rec-css2003_true-unreach-call.c below duet 2 PASS
0.701 (0.622) PASS
above 4 PASS
0.762 (0.681)
rec-ddlm2013_true-unreach-call.c below duet 2 FAIL
0.534 (0.471) FAIL
above 4 FAIL
0.621 (0.535)
rec-gcnr2008_false-unreach-call.c below duet 2 OKAY
0.821 (0.698) PASS
above 4 OKAY
0.935 (0.799)
rec-gj2007b_true-unreach-call.c below duet 2 FAIL
FAIL
0.457 FAIL
FAIL
above 4 FAIL
FAIL
0.516 (0.453)
rec-gj2007_true-unreach-call.c below duet 2 FAIL
0.459 (0.414) FAIL
above 4 FAIL
0.494 (0.424)
rec-gr2006_true-unreach-call.c below duet 2 FAIL
0.466 (0.383) FAIL
above 4 FAIL
0.478
rec-gsv2008_true-unreach-call.c below duet 2 PASS
0.434 (0.376) FAIL
above 4 PASS
0.473 (0.396)
rec-hhk2008_true-unreach-call.c below duet 2 PASS
0.42 FAIL
above 4 PASS
0.453 (0.394)
rec-jm2006_true-unreach-call.c below duet 2 PASS
0.459 (0.417) PASS
above 4 PASS
0.483 (0.431)
rec-jm2006_variant_true-unreach-call.c below duet 2 PASS
0.443 PASS
above 4 PASS
0.525 (0.43)
rec-mcmillan2006_true-unreach-call.c below duet 2 FAIL
0.493 (0.419) FAIL
above 4 FAIL
0.553 (0.457)
Total Below Time = 8.189 (was 7.198)
Above Time = 10.499 (was 9.153)
/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.421 (0.352) FAIL
above 4 PASS
0.432 (0.376)
rec-count_by_1_variant_true-unreach-call.c below duet 2 PASS
0.437 (0.379) PASS
above 4 PASS
0.451 (0.409)
rec-count_by_2_true-unreach-call.c below duet 2 PASS
0.418 (0.36) FAIL
above 4 PASS
0.445 (0.378)
rec-count_by_k_true-unreach-call.c below duet 2 PASS
0.43 FAIL
above 4 PASS
0.464 (0.405)
rec-count_by_nondet_true-unreach-call.c below duet 2 FAIL
0.432 FAIL
above 4 FAIL
0.463 (0.403)
rec-gauss_sum_true-unreach-call.c below duet 2 PASS
0.466 (0.414) FAIL
above 4 PASS
0.519 (0.432)
rec-half_true-unreach-call.c below duet 2 FAIL
0.472 (0.418) FAIL
above 4 FAIL
0.512 (0.459)
rec-nested_true-unreach-call.c below duet 3 PASS
0.614 (0.535) FAIL
above 4 FAIL
1.579 (1.432)
Total Below Time = 3.69 (was 3.265)
Above Time = 4.865 (was 4.294)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/recurrences
cubic_polynomial.c below duet 2 PASS
0.568 (0.48) FAIL
above 4 PASS
0.619 (0.559)
cubic_polynomial_unsafe.c below duet 2 OKAY
0.576 (0.504) PASS
above 4 OKAY
0.616 (0.554)
edit_distance_bottom_up.c below duet 3 FAIL
88.226 (77.867) FAIL
above 4 FAIL
193.648 (164.545)
edit_distance_top_down.c below duet 3 FAIL
4.882 (4.279) FAIL
above TIMEOUT
300.111
log_log_n_solution.c below duet 3 FAIL
0.499 (0.437) FAIL
above 4 FAIL
0.604 (0.497)
log_log_n_solution_unsafe.c below duet 3 OKAY
0.523 (0.45) PASS
above 4 OKAY
0.603 (0.522)
log_n_solution.c below duet 2 FAIL
0.51 (0.443) FAIL
above 4 FAIL
0.56 (0.502)
log_n_solution_unsafe.c below duet 2 OKAY
0.466 PASS
above 4 OKAY
0.563
multivariate_1.c below duet TIMEOUT
300.009 TIMEOUT
above TIMEOUT
300.006
multivariate_1_unsafe.c below duet TIMEOUT
300.009 TIMEOUT
above TIMEOUT
300.005
multivariate_higher_order.c below duet 7 FAIL
FAIL
FAIL
2.752 (2.462) FAIL
FAIL
FAIL
above 4 FAIL
FAIL
FAIL
22.211 (19.714)
multivariate_higher_order_unsafe.c below duet 7 OKAY
OKAY
OKAY
2.776 (2.414) PASS
PASS
PASS
above 4 OKAY
OKAY
OKAY
22.315 (19.743)
n_cubed_solution.c below duet EXCEPTION
225.973 FAIL
above 4 FAIL
19.729 (17.396)
n_cubed_solution_unsafe.c below duet EXCEPTION
0.034 (0.028)
above EXCEPTION
0.034 (0.029)
n_log_n_solution.c below duet 8 FAIL
1.143 (1.006) TIMEOUT
above 4 FAIL
6.052 (4.989)
n_log_n_solution_unsafe.c below duet 8 OKAY
1.116 (0.998) TIMEOUT
above 4 OKAY
8.158 (6.716)
n_squared_two_base_case_even.c below duet 2 PASS
0.472 (0.412) FAIL
above 4 PASS
0.531 (0.464)
n_squared_two_base_case_even_unsafe.c below duet 2 OKAY
0.451 PASS
above 4 OKAY
0.5
n_squared_two_base_case_odd.c below duet 2 PASS
0.478 (0.401) FAIL
above 4 PASS
0.521 (0.452)
n_squared_two_base_case_odd_unsafe.c below duet 2 OKAY
0.468 (0.425) PASS
above 4 OKAY
0.506 (0.446)
pascals_dynamic.c below duet 3 FAIL
2.932 (2.551) FAIL
above 4 FAIL
7.603 (6.492)
pascals_dynamic_unsafe.c below duet 3 OKAY
2.898 PASS
above 4 OKAY
7.557 (6.664)
pascals_iterative.c below duet 1 FAIL
2.419 (2.167) FAIL
above 4 FAIL
2.48 (2.149)
pascals_iterative_unsafe.c below duet 1 OKAY
2.444 (2.219) PASS
above 4 OKAY
2.498 (2.219)
pascals_recursive.c below duet 8 FAIL
5.226 (4.526) FAIL
above 4 FAIL
2.077 (1.842)
pascals_recursive_unsafe.c below duet 8 OKAY
5.043 (4.436) PASS
above 4 OKAY
2.028
squared_solution.c below duet 9 FAIL
3.723 (3.33) FAIL
above 4 FAIL
4.511 (3.734)
squared_solution_unsafe.c below duet 9 OKAY
3.819 (3.429) PASS
above 4 OKAY
5.128 (4.382)
two_n_even.c below duet 2 PASS
0.472 (0.42) PASS
above 4 PASS
0.495
two_n_even_unsafe.c below duet 2 OKAY
0.465 (0.402) PASS
above 4 OKAY
0.501 (0.428)
two_n_odd.c below duet 2 PASS
0.463 (0.4) PASS
above 4 PASS
0.504 (0.442)
two_n_odd_unsafe.c below duet 2 OKAY
0.459 (0.409) PASS
above 4 OKAY
0.496 (0.44)
two_to_n_over_two_even.c below duet TIMEOUT
300.006 FAIL
above 4 FAIL
1.365 (1.234)
two_to_n_over_two_even_unsafe.c below duet TIMEOUT
300.007 PASS
above 4 OKAY
1.358 (1.176)
two_to_n_over_two_odd.c below duet TIMEOUT
300.013 FAIL
above 4 FAIL
1.381
two_to_n_over_two_odd_unsafe.c below duet TIMEOUT
300.012 PASS
above 4 OKAY
1.385 (1.245)
two_to_n_squared.c below duet 5 FAIL
20.447 (17.945) FAIL
above 4 FAIL
4.317 (3.783)
two_to_n_squared_unsafe.c below duet 5 OKAY
20.82 (18.302) PASS
above 4 OKAY
4.294 (3.753)
two_to_two_to_n.c below duet 7 FAIL
0.939 (0.805) FAIL
above 4 FAIL
1.45 (1.248)
two_to_two_to_n_unsafe.c below duet 7 OKAY
0.936 (0.835) PASS
above 4 OKAY
1.422 (1.279)
Total Below Time = 2205.474 (was 2167.685)
Above Time = 1230.742 (was 1184.316)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/exponential
adding_and_mult.c below duet 1 FAIL
0.413 (0.355) FAIL
above 4 FAIL
0.394
adding_and_mult_unsafe.c below duet 1 OKAY
0.397 PASS
above 4 OKAY
0.408 (0.357)
binary_search_array_tree.c below duet 1 FAIL
FAIL
0.652 (0.535) FAIL
FAIL
above 4 FAIL
FAIL
0.702 (0.596)
exp_add_linear.c below duet 1 FAIL
0.438 (0.373) FAIL
above 4 FAIL
0.446
exp_add_linear_unsafe.c below duet 1 OKAY
0.446 (0.397) PASS
above 4 OKAY
0.452 (0.394)
exp_add_loop_rec.c below duet 1 FAIL
0.424 (0.376) FAIL
above 4 FAIL
0.433 (0.389)
exp_add_loop_rec_unsafe.c below duet 1 OKAY
0.418 (0.373) PASS
above 4 OKAY
0.448 (0.402)
exp_add_loop_variable.c below duet 1 FAIL
0.422 FAIL
above 4 FAIL
0.448 (0.376)
exp_add_loop_variable_unsafe.c below duet 1 OKAY
0.436 (0.374) PASS
above 4 OKAY
0.413
exp_with_linear_inner_loop.c below duet 1 FAIL
0.47 (0.402) FAIL
above 4 FAIL
0.493 (0.436)
exp_with_linear_inner_loop_unsafe.c below duet 1 OKAY
0.476 (0.416) PASS
above 4 OKAY
0.493 (0.431)
halving_log1.c below duet 1 FAIL
0.47 (0.413) FAIL
above 4 FAIL
0.495
linear_two_to_n.c below duet 6 FAIL
9.846 (8.846) FAIL
above 4 FAIL
1.525 (1.278)
linear_two_to_n_unsafe.c below duet 6 OKAY
8.501 (7.609) PASS
above 4 OKAY
1.475
loop_five_to_n.c below duet 1 FAIL
0.431 (0.383) FAIL
above 4 FAIL
0.446 (0.389)
loop_five_to_n_unsafe.c below duet 1 OKAY
0.446 (0.386) PASS
above 4 OKAY
0.414 (0.37)
non_loop_five_to_n.c below duet 6 FAIL
123.17 (246.657) FAIL
above 4 FAIL
5.764 (4.934)
non_loop_five_to_n_unsafe.c below duet 6 TIMEOUT
300.011 PASS
above 4 OKAY
5.753 (4.833)
power_log.c below duet 1 FAIL
0.477 (0.408) FAIL
above 4 FAIL
0.531 (0.434)
power_log_modified.c below duet 1 FAIL
0.52 (0.405) FAIL
above 4 FAIL
0.563 (0.4)
simple_exponential.c below duet 1 FAIL
0.445 (0.362) FAIL
above 4 FAIL
0.446 (0.356)
simple_exponential_for.c below duet 1 FAIL
0.45 (0.361) FAIL
above 4 FAIL
0.491 (0.372)
simple_exponential_for_unsafe.c below duet 1 OKAY
0.449 (0.367) PASS
above 4 OKAY
0.459 (0.382)
simple_exponential_unsafe.c below duet 1 OKAY
0.439 (0.359) PASS
above 4 OKAY
0.436 (0.368)
two_to_n_minus_n.c below duet 6 FAIL
8.982 (7.886) FAIL
above 4 FAIL
2.194 (1.846)
two_to_n_minus_n_loop.c below duet 6 FAIL
9.525 (7.928) FAIL
above 4 FAIL
2.275 (1.843)
two_to_n_minus_n_loop_unsafe.c below duet 6 OKAY
9.366 (7.892) PASS
above 4 OKAY
2.226 (1.856)
two_to_n_minus_n_unsafe.c below duet 6 OKAY
8.932 (7.813) PASS
above 4 OKAY
2.192 (1.954)
Total Below Time = 487.452 (was 602.441)
Above Time = 32.815 (was 27.958)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/HOLA
01.c below duet 3 PASS
0.47 (0.412) PASS
PASS
PASS
above 4 PASS
0.509 (0.447)
02.c below duet 3 FAIL
0.643 (0.55) FAIL
PASS
PASS
above 4 FAIL
0.714 (0.621)
03.c below duet 1 PASS
0.445 (0.388) PASS
PASS
above 4 PASS
0.464 (0.393)
04.c below duet 1 PASS
0.432 (0.339) PASS
PASS
PASS
above 4 PASS
0.401 (0.34)
05.c below duet 3 PASS
0.597 (0.506) PASS
PASS
PASS
above 4 PASS
0.763 (0.646)
06.c below duet 3 FAIL
8.563 (7.51) FAIL
PASS
PASS
above 4 FAIL
10.494
07.c below duet 3 PASS
0.489 (0.422) PASS
PASS
PASS
above 4 PASS
0.592 (0.498)
08.c below duet 3 PASS
1.126 (0.939) PASS
PASS
PASS
above 4 PASS
2.768 (2.173)
09.c below duet 3 PASS
0.622 (0.525) PASS
PASS
PASS
above 4 PASS
0.976 (0.799)
10.c below duet 3 FAIL
0.764 (0.64) FAIL
PASS
PASS
above 4 FAIL
1.078 (0.907)
11.c below duet 1 PASS
0.391 (0.323) PASS
PASS
PASS
above 4 PASS
0.391 (0.33)
12.c below duet 3 PASS
0.714 (0.6) PASS
PASS
PASS
above 4 PASS
1.041 (0.871)
13.c below duet 3 PASS
0.502 (0.43) PASS
PASS
PASS
above 4 PASS
0.599 (0.51)
14.c below duet 3 PASS
PASS
0.485 (0.401) PASS
PASS
PASS
PASS
above 4 PASS
PASS
0.531 (0.435)
15.c below duet 1 PASS
0.404 (0.351) PASS
PASS
PASS
above 4 PASS
0.398 (0.351)
16.c below duet 1 PASS
0.441 (0.356) PASS
PASS
PASS
above 4 PASS
0.444 (0.378)
17.c below duet 1 PASS
0.444 (0.382) PASS
PASS
PASS
above 4 PASS
0.464 (0.391)
18.c below duet 1 PASS
0.43 (0.357) PASS
PASS
PASS
above 4 PASS
0.436 (0.375)
19.c below duet 1 PASS
0.443 (0.36) PASS
PASS
PASS
above 4 PASS
0.479 (0.378)
20.c below duet 3 PASS
PASS
FAIL
0.585 (0.48) PASS
PASS
FAIL
PASS
PASS
above 4 PASS
PASS
FAIL
0.786 (0.643)
21.c below duet 3 PASS
0.503 (0.434) PASS
PASS
PASS
above 4 PASS
0.594 (0.516)
22.c below duet 3 FAIL
PASS
0.551 (0.47) FAIL
PASS
PASS
PASS
above 4 FAIL
PASS
0.669 (0.589)
23.c below duet 1 PASS
0.397 (0.354) PASS
PASS
PASS
above 4 PASS
0.402 (0.337)
24.c below duet 1 PASS
0.452 (0.378) PASS
PASS
PASS
above 4 PASS
0.437 (0.38)
25.c below duet 3 FAIL
1.166 (0.961) FAIL
PASS
PASS
above 4 FAIL
1.952 (1.587)
26.c below duet 3 FAIL
109.993 TIMEOUT
above 4 FAIL
256.955 (225.383)
27.c below duet 1 PASS
0.475 (0.38) PASS
PASS
PASS
above 4 PASS
0.467 (0.402)
28.c below duet 3 PASS
0.482 (0.402) PASS
PASS
PASS
above 4 PASS
0.533 (0.439)
29.c below duet 3 PASS
0.894 (0.735) PASS
PASS
PASS
above 4 PASS
1.309 (1.091)
30.c below duet 1 PASS
0.385 (0.336) PASS
PASS
PASS
above 4 PASS
0.402 (0.337)
31.c below duet 3 PASS
PASS
0.77 (0.638) PASS
PASS
PASS
PASS
above 4 PASS
PASS
1.078 (0.91)
32.c below duet 1 FAIL
0.434 (0.367) FAIL
PASS
PASS
above 4 FAIL
0.437 (0.367)
33.c below duet 3 PASS
0.968 (0.804) PASS
PASS
PASS
above 4 PASS
1.584 (1.308)
34.c below duet 1 FAIL
0.428 (0.357) FAIL
PASS
PASS
above 4 FAIL
0.437 (0.369)
35.c below duet 1 PASS
0.39 (0.322) PASS
PASS
PASS
above 4 PASS
0.36
36.c below duet 3 PASS
2.318 (1.927) PASS
PASS
PASS
above 4 PASS
4.374 (3.521)
37.c below duet 3 FAIL
0.495 (0.406) FAIL
PASS
PASS
above 4 FAIL
0.572 (0.48)
38.c below duet 1 FAIL
0.419 (0.365) FAIL
PASS
PASS
above 4 FAIL
0.433 (0.366)
39.c below duet 3 PASS
PASS
0.469 (0.406) PASS
PASS
PASS
PASS
above 4 PASS
PASS
0.546 (0.464)
40.c below duet 3 PASS
0.608 (0.508) PASS
PASS
PASS
above 4 PASS
0.84 (0.702)
41.c below duet 1 PASS
0.429 (0.355) PASS
PASS
PASS
above 4 PASS
0.427 (0.372)
42.c below duet 3 PASS
0.718 (0.599) PASS
PASS
PASS
above 4 PASS
1.015 (0.821)
43.c below duet 3 PASS
0.534 (0.464) PASS
PASS
PASS
above 4 PASS
0.686 (0.573)
44.c below duet 1 PASS
0.437 (0.341) PASS
PASS
PASS
above 4 PASS
0.432 (0.373)
45.c below duet 3 FAIL
2.017 (1.745) FAIL
PASS
PASS
above 4 FAIL
3.998 (3.359)
46.c below duet 3 FAIL
1.098 (0.915) FAIL
PASS
PASS
above 4 FAIL
1.641 (1.34)
Total Below Time = 146.82 (was 133.855)
Above Time = 306.908 (was 267.784)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/frankenstein/relational
AGHKTW2017_bar.c below duet 1 PASS
0.448 (0.371) PASS
PASS
PASS
above 4 PASS
0.462 (0.386)
AGHKTW2017_foo.c below duet 1 PASS
0.445 (0.364) PASS
PASS
PASS
above 4 PASS
0.461 (0.383)
AGHKTW2017_loginSafe.c below duet 1 PASS
0.617 (0.536) PASS
PASS
PASS
above 4 PASS
0.722 (0.599)
AGHKTW2017_loopAndBranch_safe.c below duet 1 FAIL
0.47 (0.393) FAIL
PASS
PASS
above 4 FAIL
0.5 (0.418)
BCK2011_gauss.c below duet 1 PASS
0.441 (0.388) PASS
PASS
PASS
above 4 PASS
0.429 (0.374)
BCK2011_strength_reduction.c below duet 1 PASS
0.457 (0.385) PASS
PASS
PASS
above 4 PASS
0.463 (0.394)
BCK2011_strength_reduction_linear.c below duet 1 PASS
0.437 (0.365) PASS
PASS
PASS
above 4 PASS
0.448 (0.381)
fibonacci_information_flow.c below duet 1 FAIL
0.446 (0.369) FAIL
PASS
PASS
above 4 FAIL
0.476 (0.4)
TA2005_fib2.c below duet 1 FAIL
0.498 (0.442) FAIL
PASS
PASS
above 4 FAIL
0.536 (0.452)
TA2005_fib.c below duet 1 FAIL
0.459 (0.366) FAIL
PASS
PASS
above 4 FAIL
0.444
Total Below Time = 4.718 (was 3.979)
Above Time = 4.941 (was 4.203)
/bat0/stac/Code/Ark2-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/canonical2017
boildown_11A.c below duet 2 0.638 (0.542)
above 4 0.735 (0.638)
c3_system.c below duet 3 PASS
PASS
PASS
1.377 (1.142) PASS
PASS
PASS
above 4 PASS
PASS
PASS
1.777 (1.518)
canonical11A_v_selfcomp.c below duet 2 1.051 (0.874)
above 4 2.043 (1.721)
canonical12_nv_selfcomp.c below duet 3 PASS
2.689 (2.263) PASS
above 4 PASS
5.893 (4.589)
canonical14_nv_selfcomp.c below duet 3 PASS
1.152 (0.96) PASS
above 4 PASS
1.683 (1.338)
canonical1_nv_selfcomp.c below duet 1 PASS
0.491 (0.402) PASS
above 4 PASS
0.544 (0.453)
canonical1_v_selfcomp.c below duet 1 0.557 (0.458)
above 4 0.617 (0.503)
canonical3_nv_selfcomp.c below duet 1 PASS
0.607 (0.503) PASS
above 4 PASS
0.669 (0.548)
canonical3_v_selfcomp.c below duet 1 0.66 (0.564)
above 4 0.802 (0.658)
canonical5_core.c below duet 3 0.612 (0.498)
above 4 0.705 (0.612)
canonical8_core.c below duet 1 0.736 (0.622)
above 4 0.779 (0.649)
Total Below Time = 10.57 (was 8.828)
Above Time = 16.247 (was 13.227)

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