projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0c16abf) | patch
bv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 2 Nov 2021 22:01:01 +0000 (15:01 -0700)
committerGitHub <noreply@github.com>
Tue, 2 Nov 2021 22:01:01 +0000 (22:01 +0000)
commit217a258f4b52d8776c344f9c3d0d9e79aec060a5
tree4d79f8e5543f5620b3975155c3f6229899e5a461tree
parent0c16abf2d7fe9a18494d3c9867567c43a1655200commit | diff
bv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)

When we eagerly bitblast to the main SAT solver, we have to make sure that we don't use the equality engine in order to not start propagating equalities below BITVECTOR_EAGER_ATOM predicates.

Fixes the nightly failure.
src/theory/bv/bv_solver_bitblast_internal.cpp diff | blob | history
src/theory/bv/bv_solver_bitblast_internal.h diff | blob | history