[Version Information]
WALi-OpenNWA version: 35b3457467a7787c4bb3a18de8f5d4ea4d314d2c (2018-03-22 22:15:25 -0500) "Fix to e-mail text in nightly_script.sh"
duet version: bdb80b3e64cf88f6adbffdd18bf6c10cda10bad6 (2018-03-22 19:25:29 -0400) "Fixed newton build"
# Installed packages for 4.02.1+PIC:
apron              20160125  APRON numerical abstract domain library
base-bigarray          base  Bigarray library distributed with the OCaml compile
base-bytes             base  Bytes library distributed with the OCaml compiler
base-num               base  Num library distributed with the OCaml compiler
base-ocamlbuild        base  OCamlbuild binary and libraries distributed with th
base-threads           base  Threads library distributed with the OCaml compiler
base-unix              base  Unix library distributed with the OCaml compiler
batteries             2.8.0  a community-maintained standard library extension
camlidl                1.05  Stub code generator for OCaml
cil                20150825  A front-end for the C programming language that fac
conf-gmp                  1  Virtual package relying on a GMP lib system install
conf-m4                   1  Virtual package relying on m4
conf-mathsat              1  Virtual package relying on a MathSAT system install
conf-mpfr                 1  Virtual package relying on library MPFR installatio
conf-ntl                  1  Virtual package relying on a NTL system installatio
conf-perl                 1  Virtual package relying on perl
conf-python-2-7         1.0  Virtual package relying on Python-2.7 installation.
mathsat            20161206  MathSAT 5 SMT solver
menhir             20171222  LR(1) parser generator
mlgmpidl            1.2.6-1  OCaml interface to the GMP library
ntl                20171120  Number Theory Library
num                       0  The Num library for arbitrary-precision integer and
oasis                0.4.10  Tooling for building OCaml libraries and applicatio
ocamlbuild                0  Build system distributed with the OCaml compiler si
ocamlfind           1.7.3-1  A library manager for OCaml
ocamlgraph            1.8.8  A generic graph library for OCaml
ocamlify              0.0.1  Include files in OCaml code
ocamlmod              0.0.9  Generate OCaml modules from source files
OCRS               20170905  Recurrence solver based on operational calculus
ounit                 2.0.7  Unit testing framework loosely based on HUnit. It i
ppx_deriving            3.2  Type-driven code generation for OCaml >=4.02
ppx_tools        5.0+4.02.0  Tools for authors of ppx rewriters and other syntac
Z3                 20161217  Z3 SMT solver

Test Name Output Duet Output No. of Rounds Result Run Time (Prev.) Duet Result
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/c4b
gcd.c below duet 1 FAIL
0.388 FAIL
above 4 FAIL
0.377
kmp.c below duet 1 PASS
0.741 (0.856) PASS
above 4 PASS
0.719 (0.899)
qsort.c below duet 5 PASS
0.684 (0.907) FAIL
above 4 FAIL
1.603 (3.369)
speed_pldi09_fig1.c below duet 1 PASS
0.382 PASS
above 4 PASS
0.384
speed_pldi09_fig4_2.c below duet 1 FAIL
0.375 FAIL
above 4 FAIL
0.381
speed_pldi09_fig4_4.c below duet 1 PASS
0.495 PASS
above 4 PASS
0.518
speed_pldi09_fig4_5.c below duet 1 PASS
0.371 PASS
above 4 PASS
0.381
speed_pldi10_ex1.c below duet
above TIMEOUT
300.012 (0.844) 300.012 (0.844)
speed_pldi10_ex3.c below duet 1 PASS
0.425 (0.497) PASS
above 4 PASS
0.439
speed_pldi10_ex4.c below duet 1 PASS
0.4 (0.453) PASS
above 4 PASS
0.424 (0.48)
speed_popl10_fig2_1.c below duet 1 PASS
0.432 PASS
above 4 PASS
0.429
speed_popl10_fig2_2.c below duet 1 FAIL
0.376 FAIL
above 4 FAIL
0.385
speed_popl10_nested_multiple.c below duet 1 PASS
0.441 PASS
above 4 PASS
0.405 (0.463)
speed_popl10_nested_single.c below duet 1 PASS
0.388 PASS
above 4 PASS
0.417
speed_popl10_sequential_single.c below duet 1 PASS
0.362 PASS
above 4 PASS
0.375
speed_popl10_simple_multiple.c below duet 1 PASS
0.407 PASS
above 4 PASS
0.42
speed_popl10_simple_single_2.c below duet 1 PASS
0.427 PASS
above 4 PASS
0.437
speed_popl10_simple_single.c below duet 1 PASS
0.362 PASS
above 4 PASS
0.379
t07.c below duet 1 PASS
0.395 (0.44) PASS
above 4 PASS
0.388
t08.c below duet 1 PASS
0.376 PASS
above 4 PASS
0.373
t09.c below duet 1 PASS
0.378 PASS
above 4 PASS
0.342
t10.c below duet 1 PASS
0.385 PASS
above 4 PASS
0.367
t11.c below duet 1 PASS
0.396 PASS
above 4 PASS
0.438
t13.c below duet 1 FAIL
0.409 FAIL
above 4 FAIL
0.402
t15.c below duet 1 PASS
0.404 PASS
above 4 PASS
0.412
t16.c below duet 1 PASS
0.38 PASS
above 4 PASS
0.389
t19.c below duet 1 PASS
0.374 PASS
above 4 PASS
0.381
t20.c below duet 1 PASS
0.363 PASS
above 4 PASS
0.369
t27.c below duet 1 PASS
0.427 PASS
above 4 PASS
0.442
t28.c below duet 1 PASS
0.417 (0.479) PASS
above 4 PASS
0.421 (0.482)
t30.c below duet 1 FAIL
0.371 FAIL
above 4 FAIL
0.376
t37.c below duet 2 PASS
0.471 (0.619) FAIL
above 4 PASS
0.54 (0.769)
t39.c below duet 2 PASS
0.434 (0.54) FAIL
above 4 PASS
0.46 (0.619)
t46.c below duet 1 PASS
0.428 PASS
above 4 PASS
0.412
t47.c below duet 1 PASS
0.375 PASS
above 4 PASS
0.382
Total Below Time = 14.239 (was 16.309)
Above Time = 615.391 (was 19.161)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below duet 2 PASS
PASS
0.382 (0.444) PASS
PASS
above 4 PASS
PASS
0.392 (0.498)
qsort_full.c below duet 4 PASS
PASS
PASS
PASS
PASS
PASS
5.241 (10.6) PASS
PASS
PASS
PASS
PASS
PASS
above 4 FAIL
PASS
PASS
PASS
PASS
PASS
10.775 (30.491)
rec1-param_safe.c below duet 2 PASS
PASS
PASS
0.352 (0.42) PASS
FAIL
FAIL
above 4 PASS
PASS
PASS
0.374 (0.49)
rec1-param_unsafe.c below duet 2 OKAY
0.365 (0.414) PASS
above 4 OKAY
0.362 (0.469)
rec1_safe.c below duet 2 PASS
PASS
PASS
0.349 (0.418) PASS
FAIL
FAIL
above 4 PASS
PASS
PASS
0.362 (0.436)
rec1_unsafe.c below duet 2 OKAY
0.372 PASS
above 4 OKAY
0.363 (0.45)
rec2-param_safe.c below duet 2 PASS
PASS
PASS
0.349 (0.433) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.406 (0.462)
rec2-param_unsafe.c below duet 2 OKAY
0.348 (0.428) PASS
above 4 OKAY
0.361 (0.447)
rec2_safe.c below duet 2 PASS
PASS
PASS
0.338 (0.423) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.365 (0.444)
rec2_unsafe.c below duet 2 OKAY
0.346 (0.402) PASS
above 4 OKAY
0.347 (0.467)
rec-test.c below duet 2 PASS
0.342 (0.405) FAIL
above 4 PASS
0.357 (0.435)
sas03_bothbranches.c below duet 7 FAIL
0.542 (0.78) PASS
above 4 FAIL
0.735 (1.258)
sas03.c below duet 2 PASS
0.619 (0.707) PASS
above 4 PASS
0.725 (0.868)
simulated_lese_recursive.c below duet 2 PASS
0.403 PASS
above 4 PASS
0.414 (0.497)
Total Below Time = 10.348 (was 16.719)
Above Time = 16.338 (was 37.712)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below duet 1 PASS
0.325 PASS
above 4 PASS
0.338
count_up_down_unsafe.c below duet 1 OKAY
0.349 PASS
above 4 OKAY
0.33
divide.c below duet 1 PASS
0.362 PASS
above 4 PASS
0.361
factor_unsafe.c below duet 1 OKAY
0.327 PASS
above 4 OKAY
0.336
for_infinite_loop_1_safe.c below duet 1 PASS
0.33 PASS
above 0 PASS
0.333
for_infinite_loop_2_safe.c below duet 1 PASS
0.329 PASS
above 0 PASS
0.332
interproc.c below duet 1 PASS
0.334 PASS
above 4 PASS
0.327
mult.c below duet 1 PASS
PASS
0.351 PASS
PASS
above 4 PASS
PASS
0.338
pointer_arith.c below duet 1 PASS
PASS
PASS
PASS
0.307 PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
0.328
quotient.c below duet 3 PASS
0.436 (0.516) PASS
above 4 PASS
0.467 (0.546)
subtract.c below duet 1 PASS
0.328 PASS
above 4 PASS
0.345
sum01_bug02_sum01_bug02_base.case_unsafe.c below duet 1 OKAY
0.358 PASS
above 4 OKAY
0.364
sum01_bug02_unsafe.c below duet 1 OKAY
0.406 PASS
above 4 OKAY
0.411
sum01_real_safe.c below duet 1 PASS
0.336 PASS
above 4 PASS
0.333
sum01_safe.c below duet 1 PASS
0.33 PASS
above 4 PASS
0.334
sum01_unsafe.c below duet 1 OKAY
0.37 PASS
above 4 OKAY
0.371
sum02_safe.c below duet 1 PASS
0.357 PASS
above 4 PASS
0.355
sum03_safe.c below duet 1 PASS
0.354 PASS
above 0 PASS
0.356
sum03_unsafe.c below duet 1 OKAY
0.408 PASS
above 0 OKAY
0.393
sum04_safe.c below duet 1 PASS
0.34 PASS
above 4 PASS
0.329 (0.367)
sum04_unsafe.c below duet 1 OKAY
0.36 PASS
above 4 OKAY
0.366 (0.408)
terminator_02_safe.c below duet 1 PASS
0.342 PASS
above 4 PASS
0.349
terminator_02_unsafe.c below duet 1 OKAY
0.357 PASS
above 4 OKAY
0.352
terminator_03_safe.c below duet 1 PASS
0.341 PASS
above 4 PASS
0.35
terminator_03_unsafe.c below duet 1 OKAY
0.347 PASS
above 4 OKAY
0.36
token_ring01_safe.c below duet 4 FAIL
65.27 (118.524) TIMEOUT
above
above 4 FAIL
160.216 (300.016)
token_ring01_unsafe.c below duet 4 OKAY
90.777 (155.656) 300.008 (155.656)
speed_pldi10_ex3.c below duet 1 PASS
0.428 (0.497) PASS
above 4 PASS
0.445
speed_pldi10_ex4.c below duet 1 PASS
0.417 PASS
above 4 PASS
0.433
speed_popl10_fig2_1.c below duet 1 PASS
0.398 PASS
above 4 PASS
0.402
speed_popl10_fig2_2.c below duet 1 FAIL
0.375 FAIL
above 4 FAIL
0.388
speed_popl10_nested_multiple.c below duet 1 PASS
0.425 PASS
above 4 PASS
0.437
speed_popl10_nested_single.c below duet 1 PASS
0.389 PASS
above 4 PASS
0.404
speed_popl10_sequential_single.c below duet 1 PASS
0.36 PASS
above 4 PASS
0.365
speed_popl10_simple_multiple.c below duet 1 PASS
0.39 PASS
above 4 PASS
0.396
speed_popl10_simple_single_2.c below duet 1 PASS
0.439 PASS
above 4 PASS
0.452
speed_popl10_simple_single.c below duet 1 PASS
0.355 PASS
above 4 PASS
0.349
t07.c below duet 1 PASS
0.376 (0.44) PASS
above 4 PASS
0.385
t08.c below duet 1 PASS
0.358 PASS
above 4 PASS
0.364 (0.406)
t09.c below duet 1 PASS
0.352 PASS
above 4 PASS
0.365
t10.c below duet 1 PASS
0.359 PASS
above 4 PASS
0.357
t11.c below duet 1 PASS
0.404 PASS
above 4 PASS
0.398 (0.456)
t13.c below duet 1 FAIL
0.384 FAIL
above 4 FAIL
0.386 (0.44)
t15.c below duet 1 PASS
0.392 PASS
above 4 PASS
0.406
t16.c below duet 1 PASS
0.384 PASS
above 4 PASS
0.407
t19.c below duet 1 PASS
0.364 PASS
above 4 PASS
0.386
t20.c below duet 1 PASS
0.374 PASS
above 4 PASS
0.38
t27.c below duet 1 PASS
0.426 PASS
above 4 PASS
0.428
t28.c below duet 1 PASS
0.419 (0.479) PASS
above 4 PASS
0.42 (0.482)
t30.c below duet 1 FAIL
0.39 FAIL
above 4 FAIL
0.417 (0.363)
t37.c below duet
above 2 UNSOUND
0.493 (300.041) PASS
above 4 PASS
0.571 (0.769)
t39.c below duet 2 PASS
0.442 (0.54) FAIL
above 4 PASS
0.493 (0.619)
t46.c below duet 1 PASS
0.387 PASS
above 4 PASS
0.443
t47.c below duet 1 PASS
0.391 PASS
above 4 PASS
0.409
Total Below Time = 475.017 (was 443.44)
Above Time = 180.653 (was 778.314)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/misc-recursive
mult-rec.c below duet 2 PASS
PASS
0.385 (0.444) PASS
PASS
above 4 PASS
PASS
0.42 (0.498)
qsort_full.c below duet 4 PASS
PASS
PASS
PASS
PASS
PASS
5.604 (10.6) PASS
PASS
PASS
PASS
PASS
PASS
above 4 FAIL
PASS
PASS
PASS
PASS
PASS
11.429 (30.491)
rec1-param_safe.c below duet 2 PASS
PASS
PASS
0.351 (0.42) PASS
FAIL
FAIL
above 4 PASS
PASS
PASS
0.392 (0.49)
rec1-param_unsafe.c below duet 2 OKAY
0.363 (0.414) PASS
above 4 OKAY
0.395 (0.469)
rec1_safe.c below duet 2 PASS
PASS
PASS
0.357 (0.418) PASS
FAIL
FAIL
above 4 PASS
PASS
PASS
0.364 (0.436)
rec1_unsafe.c below duet 2 OKAY
0.353 (0.409) PASS
above 4 OKAY
0.372 (0.45)
rec2-param_safe.c below duet 2 PASS
PASS
PASS
0.369 (0.433) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.373 (0.462)
rec2-param_unsafe.c below duet 2 OKAY
0.359 (0.428) PASS
above 4 OKAY
0.373 (0.447)
rec2_safe.c below duet 2 PASS
PASS
PASS
0.357 (0.423) PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.368 (0.444)
rec2_unsafe.c below duet 2 OKAY
0.348 (0.402) PASS
above 4 OKAY
0.378 (0.467)
rec-test.c below duet 2 PASS
0.365 FAIL
above 4 PASS
0.369 (0.435)
sas03_bothbranches.c below duet 7 FAIL
0.532 (0.78) PASS
above 4 FAIL
0.784 (1.258)
sas03.c below duet 2 PASS
0.671 PASS
above 4 PASS
0.744 (0.868)
simulated_lese_recursive.c below duet 2 PASS
0.407 PASS
above 4 PASS
0.428 (0.497)
Total Below Time = 10.821 (was 16.719)
Above Time = 17.189 (was 37.712)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/duet
count_up_down_safe.c below duet 1 PASS
0.39 (0.341) PASS
above 4 PASS
0.342
count_up_down_unsafe.c below duet 1 OKAY
0.343 PASS
above 4 OKAY
0.353
divide.c below duet 1 PASS
0.378 PASS
above 4 PASS
0.375
factor_unsafe.c below duet 1 OKAY
0.329 PASS
above 4 OKAY
0.335
for_infinite_loop_1_safe.c below duet 1 PASS
0.323 PASS
above 0 PASS
0.337
for_infinite_loop_2_safe.c below duet 1 PASS
0.344 PASS
above 0 PASS
0.318
interproc.c below duet 1 PASS
0.336 PASS
above 4 PASS
0.354 (0.316)
mult.c below duet 1 PASS
PASS
0.342 PASS
PASS
above 4 PASS
PASS
0.364
pointer_arith.c below duet 1 PASS
PASS
PASS
PASS
0.33 PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
0.319
quotient.c below duet 3 PASS
0.456 (0.516) PASS
above 4 PASS
0.49 (0.546)
subtract.c below duet 1 PASS
0.336 PASS
above 4 PASS
0.333
sum01_bug02_sum01_bug02_base.case_unsafe.c below duet 1 OKAY
0.368 PASS
above 4 OKAY
0.369
sum01_bug02_unsafe.c below duet 1 OKAY
0.402 PASS
above 4 OKAY
0.412
sum01_real_safe.c below duet 1 PASS
0.343 PASS
above 4 PASS
0.372
sum01_safe.c below duet 1 PASS
0.355 PASS
above 4 PASS
0.339
sum01_unsafe.c below duet 1 OKAY
0.381 PASS
above 4 OKAY
0.397
sum02_safe.c below duet 1 PASS
0.352 PASS
above 4 PASS
0.348
sum03_safe.c below duet 1 PASS
0.347 PASS
above 0 PASS
0.389
sum03_unsafe.c below duet 1 OKAY
0.387 (0.431) PASS
above 0 OKAY
0.412
sum04_safe.c below duet 1 PASS
0.345 PASS
above 4 PASS
0.358
sum04_unsafe.c below duet 1 OKAY
0.362 PASS
above 4 OKAY
0.38
terminator_02_safe.c below duet 1 PASS
0.337 PASS
above 4 PASS
0.356
terminator_02_unsafe.c below duet 1 OKAY
0.361 PASS
above 4 OKAY
0.368
terminator_03_safe.c below duet 1 PASS
0.352 PASS
above 4 PASS
0.341
terminator_03_unsafe.c below duet 1 OKAY
0.348 PASS
above 4 OKAY
0.352
token_ring01_safe.c below duet 4 FAIL
71.537 (118.524) FAIL
above 4 TIMEOUT
300.037
toy_safe.c below duet FAIL
156.335
token_ring01_unsafe.c below duet 4 OKAY
113.498 (155.656) 196.661 (155.656) PASS
above
above TIMEOUT
300.035 (164.293)
toy_safe.c below duet EXCEPTION
150.897 251.102 (155.122)
trex01_safe.c below duet 1 PASS
0.44 (0.771) PASS
above 4 PASS
0.377 (0.425)
trex01_unsafe.c below duet 1 OKAY
0.382 PASS
above 4 OKAY
0.374 (0.416)
trex02_safe2.c below duet 3 PASS
0.383 (0.614) PASS
above 4 PASS
0.397 (0.508)
trex02_safe.c below duet 3 PASS
0.357 (0.464) PASS
above 4 PASS
0.416 (0.578)
trex02_unsafe.c below duet 3 OKAY
0.382 (0.477) PASS
above 4 OKAY
0.431 (0.519)
trex03_safe.c below duet 1 PASS
0.404 PASS
above 4 PASS
0.443
trex03_unsafe.c below duet 1 OKAY
0.416 PASS
above 4 OKAY
0.446
trex04_safe.c below duet 1 PASS
0.359 PASS
above 4 PASS
0.368
while_infinite_loop_1_safe.c below duet 1 PASS
0.323 PASS
above 0 PASS
0.313
while_infinite_loop_2_safe.c below duet 1 PASS
0.318 PASS
above 0 PASS
0.334
while_infinite_loop_3_safe.c below duet 1 PASS
0.333 PASS
above 4 PASS
0.343
Total Below Time = 953.074 (was 443.44)
Above Time = 613.427 (was 778.314)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below duet 3 PASS
0.371 (0.473) PASS
above 4 FAIL
0.455 (0.685)
blogger_simplified1.c below duet 3 PASS
0.703 (0.992) PASS
above 4 PASS
1.082 (1.473)
divided_difference2.c below duet
above TIMEOUT
300.923 (164.293) 197.797 (164.293)
trex01_safe.c below duet 1 PASS
0.713 PASS
above 4 PASS
0.382 (0.425)
trex01_unsafe.c below duet 1 OKAY
0.377 PASS
above 4 OKAY
0.375
trex02_safe2.c below duet 3 PASS
0.367 (0.614) PASS
above 4 PASS
0.404 (0.508)
trex02_safe.c below duet 3 PASS
0.37 (0.464) PASS
above 4 PASS
0.422 (0.578)
trex02_unsafe.c below duet 3 OKAY
0.381 (0.477) PASS
above 4 OKAY
0.396 (0.519)
trex03_safe.c below duet 1 PASS
0.386 (0.445) PASS
above 4 PASS
0.428
trex03_unsafe.c below duet 1 OKAY
0.415 PASS
above 4 OKAY
0.415 (0.465)
trex04_safe.c below duet 1 PASS
0.36 PASS
above 4 PASS
0.359
while_infinite_loop_1_safe.c below duet 1 PASS
0.318 PASS
above 0 PASS
0.317
while_infinite_loop_2_safe.c below duet 1 PASS
0.331 PASS
above 0 PASS
0.326
while_infinite_loop_3_safe.c below duet 1 PASS
0.343 PASS
above 4 PASS
0.316
Total Below Time = 5.435 (was 303.435)
Above Time = 504.397 (was 304.198)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests
above_litmus.c below duet 3 PASS
0.382 (0.473) PASS
above 4 FAIL
0.455 (0.685)
blogger_simplified1.c below duet 3 PASS
0.705 (0.992) PASS
above 4 PASS
1.101 (1.473)
divided_difference2.c below duet
above TIMEOUT
300.007 300.005
mult-proc.c below duet 3 PASS
PASS
0.365 (0.477) PASS
PASS
above 4 PASS
PASS
0.386 (0.5)
mult-proc-params.c below duet 3 PASS
PASS
0.393 (0.488) PASS
PASS
above 4 PASS
PASS
0.407 (0.538)
popall.c below duet 1 PASS
PASS
PASS
PASS
PASS
0.411 (0.473) PASS
PASS
PASS
PASS
PASS
above 4 PASS
PASS
PASS
PASS
PASS
0.431
simulated_scc.c below duet 1 PASS
PASS
0.469 (0.524) PASS
PASS
above 4 PASS
PASS
0.44 (0.524)
Total Below Time = 2.725 (was 303.435)
Above Time = 603.232 (was 304.198)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/polynomial/assert
degree1_monomial.c below duet 1 PASS
0.343 PASS
above 4 PASS
0.368
degree2_binomial.c below duet 1 PASS
0.447 (0.515) PASS
above 4 PASS
0.454 (0.521)
degree2_monomial.c below duet 1 PASS
0.366 PASS
above 4 PASS
0.409
degree3_binomial.c below duet 1 PASS
0.797 PASS
above 4 PASS
0.814 (0.908)
degree3_monomial.c below duet 1 PASS
0.402 (0.467) PASS
above 4 PASS
0.433
degree4_binomial.c below duet 1 PASS
0.826 (1.37) PASS
above 4 PASS
0.894 (1.456)
degree4_monomial.c below duet 1 PASS
0.498 PASS
above 4 PASS
0.54
degree5_binomial.c below duet 1 PASS
1.354 PASS
above 4 PASS
1.393
degree5_monomial.c below duet 1 PASS
0.639 PASS
above 4 PASS
0.667
Total Below Time = 5.672 (was 6.654)
Above Time = 5.972 (was 6.886)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/snlee/snlee_tests
cubic_with_square.c below duet 1 PASS
0.377 PASS
above 4 PASS
0.354
cubic_with_square_interproc.c below duet 2 PASS
0.466 FAIL
above 4 PASS
0.492
cubic_with_square_nonlinear.c below duet 1 PASS
0.351 PASS
above 4 PASS
0.352
cubic_with_square_nonlinear_interproc.c below duet 2 PASS
0.394 (0.469) FAIL
above 4 PASS
0.439 (0.522)
cubic_with_square_nonlinear_unsafe.c below duet 1 UNSOUND
0.367 FAIL
above 4 UNSOUND
0.362
cubic_with_square_unsafe.c below duet 1 OKAY
0.366 PASS
above 4 OKAY
0.384
multi-input.c below duet 1 PASS
0.465 PASS
above 4 PASS
0.454
multi-input_unsafe.c below duet 1 UNSOUND
0.465 FAIL
above 4 UNSOUND
0.453
nondet_loop_bound.c below duet 1 PASS
0.342 (0.381) PASS
above 4 PASS
0.348 (0.39)
nondet_loop_bound_quartic.c below duet 1 PASS
0.378 PASS
above 4 PASS
0.375
nondet_loop_bound_quartic_unsafe.c below duet 1 OKAY
0.387 PASS
above 4 OKAY
0.383
nondet_loop_bound_unsafe.c below duet 1 OKAY
0.379 PASS
above 4 OKAY
0.37
nonlinear_stratified.c below duet 1 PASS
0.667 (0.383) PASS
above 4 PASS
0.68 (0.388)
nonlinear_stratified_unsafe.c below duet 1 UNSOUND
0.694 (0.398) FAIL
above 4 UNSOUND
0.687 (0.388)
quartic_with_cube.c below duet 1 PASS
0.38 PASS
above 4 PASS
0.397
quartic_with_cube_nonlinear.c below duet 1 PASS
0.39 PASS
above 4 PASS
0.403
quartic_with_cube_nonlinear_unsafe.c below duet 1 UNSOUND
0.38 FAIL
above 4 UNSOUND
0.372 (0.419)
quartic_with_cube_unsafe.c below duet 1 OKAY
0.396 PASS
above 4 OKAY
0.401
quintic_with_quartic.c below duet 1 FAIL
0.529 (0.389) FAIL
above 4 FAIL
0.496 (0.393)
quintic_with_quartic_nonlinear.c below duet 1 PASS
0.535 (0.439) PASS
above 4 PASS
0.503 (0.435)
quintic_with_quartic_nonlinear_unsafe.c below duet 1 UNSOUND
0.525 (0.442) FAIL
above 4 UNSOUND
0.533 (0.421)
quintic_with_quartic_unsafe.c below duet 1 OKAY
0.511 (0.396) PASS
above 4 OKAY
0.518 (0.382)
Total Below Time = 9.744 (was 8.951)
Above Time = 9.756 (was 9.003)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/FiniteDifferencing
degree2.c below duet 1 PASS
0.501 (0.583) PASS
above 4 PASS
0.502 (0.595)
degree2_FD_AllAux_AllAssm.c below duet 1 PASS
2.473 (1.693) PASS
above 4 PASS
2.273 (1.729)
degree2_FD_AllAux_FewAssm.c below duet 1 PASS
1.912 (1.708) PASS
above 4 PASS
1.914
degree2_FD_FewAux_FewAssm.c below duet 1 PASS
0.787 PASS
above 4 PASS
0.768
degree2_FD_FewAux_FewAssm_NonLinAsrt.c below duet 1 PASS
0.777 PASS
above 4 PASS
0.781
degree3.c below duet 1 PASS
0.639 PASS
above 4 PASS
0.679
degree3_FD.c below duet 1 PASS
0.761 PASS
above 4 PASS
0.75
degree4.c below duet 1 PASS
0.452 PASS
above 4 PASS
0.472
Total Below Time = 8.302 (was 7.266)
Above Time = 8.139 (was 7.424)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LESE
loop.c below duet 1 PASS
0.372 (0.417) PASS
above 4 PASS
0.391 (0.441)
loop_unsafe.c below duet 1 OKAY
0.387 (0.435) PASS
above 4 OKAY
0.381 (0.439)
simulated_lese_parser.c below duet 1 PASS
0.354 PASS
above 4 PASS
0.339
simulated_lese_sentinel.c below duet 1 PASS
0.351 PASS
above 4 PASS
0.341
Total Below Time = 1.464 (was 1.569)
Above Time = 1.452 (was 1.597)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LowerBound
lower_bound.c below duet 1 PASS
PASS
PASS
0.35 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.343 (0.383)
Total Below Time = 0.35 (was 0.376)
Above Time = 0.343 (was 0.383)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/STAC/LZ
lz77.c below duet 3 3.068 (300.006)
above 4 4.534 (300.004)
Total Below Time = 3.068 (was 300.006)
Above Time = 4.534 (was 300.004)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-acceleration
array_false-unreach-call1.c below duet 1 OKAY
0.325 PASS
above 4 OKAY
0.342
array_false-unreach-call2.c below duet 1 OKAY
0.367 PASS
above 4 OKAY
0.345 (0.392)
array_false-unreach-call3.c below duet 1 OKAY
0.344 PASS
above 4 OKAY
0.353
array_true-unreach-call1.c below duet 1 FAIL
0.34 FAIL
above 4 FAIL
0.336
array_true-unreach-call2.c below duet 1 FAIL
0.348 FAIL
above 4 FAIL
0.351
array_true-unreach-call3.c below duet 1 PASS
0.344 PASS
above 4 PASS
0.337
array_true-unreach-call4.c below duet 1 FAIL
0.336 FAIL
above 4 FAIL
0.335
const_false-unreach-call1.c below duet 1 UNSOUND
0.332 FAIL
above 4 UNSOUND
0.343
const_true-unreach-call1.c below duet 1 PASS
0.338 PASS
above 4 PASS
0.324
diamond_false-unreach-call1.c below duet 1 OKAY
0.349 PASS
above 4 OKAY
0.335
diamond_true-unreach-call1.c below duet 1 PASS
0.339 PASS
above 4 PASS
0.325
diamond_true-unreach-call2.c below duet 1 PASS
0.37 TIMEOUT
above
above 4 PASS
0.389
functions_false-unreach-call1.c below duet 3 OKAY
0.366 (0.447) PASS
above 4 OKAY
0.373 (0.489)
functions_true-unreach-call1.c below duet 3 PASS
0.36 (0.443) PASS
above 4 PASS
0.388 (0.474)
multivar_false-unreach-call1.c below duet 1 OKAY
0.337 PASS
above 4 OKAY
0.321
multivar_true-unreach-call1.c below duet 1 PASS
0.335 PASS
above 4 PASS
0.325
nested_false-unreach-call1.c below duet 1 UNSOUND
0.351 FAIL
above 4 UNSOUND
0.336 (0.375)
nested_true-unreach-call1.c below duet 1 PASS
0.333 (0.38) PASS
above 4 PASS
0.353
overflow_true-unreach-call1.c below duet 1 PASS
0.335 PASS
above 4 PASS
0.33
phases_false-unreach-call1.c below duet 1 OKAY
0.352 PASS
above 4 OKAY
0.36
phases_false-unreach-call2.c below duet 1 OKAY
0.345 PASS
above 4 OKAY
0.356
phases_true-unreach-call1.c below duet 1 PASS
0.349 PASS
above 4 PASS
0.342
phases_true-unreach-call2.c below duet 1 PASS
0.364 PASS
above 4 PASS
0.343
simple_false-unreach-call1.c below duet 1 OKAY
0.325 PASS
above 4 OKAY
0.339
simple_false-unreach-call2.c below duet 1 OKAY
0.324 PASS
above 4 OKAY
0.319
simple_false-unreach-call3.c below duet 1 OKAY
0.337 PASS
above 4 OKAY
0.332
simple_false-unreach-call4.c below duet 1 OKAY
0.331 PASS
above 4 OKAY
0.324
simple_true-unreach-call1.c below duet 1 PASS
0.31 (0.345) PASS
above 4 PASS
0.32 (0.361)
simple_true-unreach-call2.c below duet 1 PASS
0.324 PASS
above 4 PASS
0.33
simple_true-unreach-call3.c below duet 1 PASS
0.342 PASS
above 4 PASS
0.332
simple_true-unreach-call4.c below duet 1 PASS
0.333 PASS
above 4 PASS
0.318
underapprox_false-unreach-call1.c below duet 1 OKAY
0.338 PASS
above 4 OKAY
0.335
underapprox_false-unreach-call2.c below duet 1 OKAY
0.337 PASS
above 4 OKAY
0.337
underapprox_true-unreach-call1.c below duet 1 FAIL
0.332 FAIL
above 4 FAIL
0.337
underapprox_true-unreach-call2.c below duet 1 PASS
0.328 PASS
above 4 PASS
0.333
Total Below Time = 11.92 (was 12.614)
Above Time = 11.898 (was 12.74)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-invgen
apache-escape-absolute_true-unreach-call.c below duet 1 PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
PASS
0.716 (1.303) 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.852 (1.449)
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.437 (0.528) 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.438 (0.545)
down_true-unreach-call.c below duet 1 PASS
0.355 PASS
above 4 PASS
0.348 (0.388)
fragtest_simple_true-unreach-call.c below duet 1 PASS
0.387 (0.452) PASS
above 4 PASS
0.387 (0.435)
half_2_true-unreach-call.c below duet 1 PASS
0.346 (0.391) PASS
above 4 PASS
0.35
heapsort_true-unreach-call.c below duet 1 FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
PASS
PASS
PASS
PASS
2.553 (1.844) 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.512 (1.758)
id_build_true-unreach-call.c below duet 1 PASS
PASS
0.349 PASS
PASS
above 4 PASS
PASS
0.337
id_trans_false-unreach-call.c below duet 1 OKAY
0.339 PASS
above 4 OKAY
0.343
id_trans_true-unreach-call.c below duet 1 PASS
PASS
PASS
0.349 PASS
PASS
PASS
above 4 PASS
PASS
PASS
0.342 (0.385)
large_const_true-unreach-call.c below duet 1 PASS
0.397 PASS
above 4 PASS
0.384 (0.435)
MADWiFi-encode_ie_ok_true-unreach-call.c below duet 1 PASS
PASS
0.365 (0.414) PASS
PASS
above 4 PASS
PASS
0.366
nested6_true-unreach-call.c below duet 1 FAIL
FAIL
PASS
0.401 (0.481) FAIL
FAIL
PASS
above 4 FAIL
FAIL
PASS
0.399 (0.466)
nested9_true-unreach-call.c below duet 1 PASS
0.42 (0.519) PASS
above 4 PASS
0.475
nest-if3_true-unreach-call.c below duet 1 PASS
0.389 PASS
above 4 PASS
0.395 (0.45)
NetBSD_loop_true-unreach-call.c below duet 1 PASS
PASS
0.391 (0.352) PASS
PASS
above 4 PASS
PASS
0.346
sendmail-close-angle_true-unreach-call.c below duet 1 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.374 (0.437) PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
above 4 PASS
FAIL
PASS
FAIL
PASS
FAIL
PASS
FAIL
0.398
seq_true-unreach-call.c below duet 1 PASS
0.398 PASS
above 4 PASS
0.4
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
0.94 (1.208) 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
0.946 (1.235)
string_concat-noarr_true-unreach-call.c below duet 1 PASS
0.363 PASS
above 4 PASS
0.4
up_true-unreach-call.c below duet 1 PASS
0.355 PASS
above 4 PASS
0.375
Total Below Time = 10.624 (was 11.435)
Above Time = 10.793 (was 11.564)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-lit
afnp2014_true-unreach-call.c below duet 1 PASS
0.356 PASS
above 4 PASS
0.338
bhmr2007_true-unreach-call.c below duet 1 PASS
0.368 PASS
above 4 PASS
0.364
cggmp2005b_true-unreach-call.c below duet 1 PASS
0.378 (0.448) PASS
above 4 PASS
0.365 (0.436)
cggmp2005_true-unreach-call.c below duet 1 PASS
0.356 PASS
above 4 PASS
0.346
cggmp2005_variant_true-unreach-call.c below duet 1 PASS
0.382 (0.343) PASS
above 4 PASS
0.339
css2003_true-unreach-call.c below duet 1 PASS
0.505 PASS
above 4 PASS
0.512
ddlm2013_true-unreach-call.c below duet 1 PASS
0.417 PASS
above 4 PASS
0.415
gcnr2008_false-unreach-call.c below duet 1 OKAY
0.631 PASS
above 4 OKAY
0.67
gj2007b_true-unreach-call.c below duet 1 PASS
PASS
0.367 PASS
PASS
above 4 PASS
PASS
0.361
gj2007_true-unreach-call.c below duet 1 PASS
0.353 PASS
above 4 PASS
0.35
gr2006_true-unreach-call.c below duet 1 PASS
0.362 PASS
above 4 PASS
0.359
gsv2008_true-unreach-call.c below duet 1 PASS
0.344 PASS
above 4 PASS
0.326
hhk2008_true-unreach-call.c below duet 1 PASS
0.35 PASS
above 4 PASS
0.349
jm2006_true-unreach-call.c below duet 1 PASS
0.366 PASS
above 4 PASS
0.37
jm2006_variant_true-unreach-call.c below duet 1 PASS
0.37 PASS
above 4 PASS
0.398
mcmillan2006_true-unreach-call.c below duet 1 FAIL
0.379 FAIL
above 4 FAIL
0.386
Total Below Time = 6.284 (was 6.511)
Above Time = 6.248 (was 6.526)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loop-new
count_by_1_true-unreach-call.c below duet 1 PASS
0.339 PASS
above 4 PASS
0.315
count_by_1_variant_true-unreach-call.c below duet 1 PASS
0.383 PASS
above 4 PASS
0.341
count_by_2_true-unreach-call.c below duet 1 PASS
0.339 PASS
above 4 PASS
0.324
count_by_k_true-unreach-call.c below duet 1 PASS
0.942 (0.354) PASS
above 4 PASS
0.946 (0.362)
count_by_nondet_true-unreach-call.c below duet 1 FAIL
0.355 FAIL
above 4 FAIL
0.347
gauss_sum_true-unreach-call.c below duet 1 PASS
0.358 PASS
above 4 PASS
0.346
half_true-unreach-call.c below duet 1 FAIL
0.363 FAIL
above 4 FAIL
0.344
nested_true-unreach-call.c below duet 1 PASS
0.409 PASS
above 4 PASS
0.398
Total Below Time = 3.488 (was 2.9)
Above Time = 3.361 (was 2.889)
/bat0/stac/Code/WALi-Sandbox/WALi-OpenNWA/Examples/cprover/tests/sv-benchmarks/loops
array_false-unreach-call.c below duet 1 OKAY
0.399 PASS
above 4 OKAY
0.395
array_true-unreach-call.c below duet 1 FAIL
0.395 FAIL
above 4 FAIL
0.384
bubble_sort_false-unreach-call.c below duet 4 OKAY
OKAY
83.28 (96.945) 300.003 (96.945)
mult-proc.c below duet FAIL
PASS
PASS