mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
bug fixes exposed from regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8fa0d6e4f3
commit
d6f0c13f2a
|
@ -645,7 +645,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
// perform unit propagation
|
||||
if (false && maxsum >= c.k() && maxsum - mininc < c.k()) {
|
||||
if (maxsum >= c.k() && maxsum - mininc < c.k()) {
|
||||
literal_vector& lits = get_unhelpful_literals(c, true);
|
||||
lits.push_back(c.lit());
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
|
|
Loading…
Reference in a new issue