Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 27 May 2021 17:11:57 +0000 (10:11 -0700)
committerGitHub <noreply@github.com>
Thu, 27 May 2021 17:11:57 +0000 (17:11 +0000)
commit1483676841847216a7cfe15e5d201a924739d014
tree263936671433981b14fa9543ddd26638eb9492f1
parent7120cf46b38f0bede1ab8d17453ae925aa2d27fd
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.
src/theory/bv/theory_bv_rewriter.cpp
test/regress/CMakeLists.txt
test/regress/regress0/fp/bvcomp-rewrite.smt2 [new file with mode: 0644]
test/unit/theory/theory_bv_rewriter_white.cpp