diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-27 10:11:57 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-27 17:11:57 +0000 |
| commit | 1483676841847216a7cfe15e5d201a924739d014 (patch) | |
| tree | 263936671433981b14fa9543ddd26638eb9492f1 /test/regress | |
| parent | 7120cf46b38f0bede1ab8d17453ae925aa2d27fd (diff) | |
Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)
This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/bvcomp-rewrite.smt2 | 5 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a3244ff4a..817ddc2ba 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -582,6 +582,7 @@ set(regress_0_tests regress0/fmf/tail_rec.smt2 regress0/fp/abs-unsound.smt2 regress0/fp/abs-unsound2.smt2 + regress0/fp/bvcomp-rewrite.smt2 regress0/fp/down-cast-RNA.smt2 regress0/fp/ext-rew-test.smt2 regress0/fp/from_ubv.smt2 diff --git a/test/regress/regress0/fp/bvcomp-rewrite.smt2 b/test/regress/regress0/fp/bvcomp-rewrite.smt2 new file mode 100644 index 000000000..7c14ee58e --- /dev/null +++ b/test/regress/regress0/fp/bvcomp-rewrite.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_FP) +(declare-const x Float64) +(assert (fp.isNaN (fp.sub roundNearestTiesToEven (fp.mul roundNearestTiesToEven x (fp (_ bv0 1) (_ bv2047 11) (_ bv1 52))) (fp.mul roundNearestTiesToEven x x)))) +(set-info :status sat) +(check-sat) |