mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Fix unsoundness in ule_constraint lemma

Browse source
This commit is contained in:
Jakob Rath 2023-01-23 13:59:00 +01:00
parent c6cd35508b
commit 46147c2fc3
1 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/polysat/ule_constraint.cpp
View file

@ -240,14 +240,13 @@ namespace polysat {
s.m_viable.intersect(p, q, sc); s.m_viable.intersect(p, q, sc);
if (first && !is_positive) { if (first && !is_positive && !lhs().is_val() && !rhs().is_val()) {
if (!p.is_val()) // lhs > rhs ==> -1 > rhs
// -1 > q s.add_clause(~sc, s.ult(rhs(), -1), false);
s.add_clause(~sc, s.ult(q, -1), false); // lhs > rhs ==> lhs > 0
if (!q.is_val()) s.add_clause(~sc, s.ult(0, lhs()), false);
// p > 0
s.add_clause(~sc, s.ult(0, p), false);
} }
#if 0 #if 0
propagate_bits(s, is_positive); propagate_bits(s, is_positive);
#endif #endif