mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

fix bug in rule

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-10 05:49:54 +02:00
parent 18e5a3a991
commit ba5e2a8d2b
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/polysat/saturation.cpp
View file

@ -245,7 +245,7 @@ namespace polysat {
/** /**
* Implement the inferences * Implement the inferences
* [x] zx > yx ==> Ω*(x,y) \/ z > y * [x] zx > yx ==> Ω*(x,y) \/ z > y
* [x] yx <= zx ==> Ω*(x,y) \/ y <= z * [x] yx <= zx ==> Ω*(x,y) \/ y <= z \/ x = 0
*/ */
bool inf_saturate::try_ugt_x(pvar v, conflict_core& core, inequality const& c) { bool inf_saturate::try_ugt_x(pvar v, conflict_core& core, inequality const& c) {
pdd x = s().var(v); pdd x = s().var(v);
@ -255,10 +255,13 @@ namespace polysat {
return false; return false;
if (!is_non_overflow(x, y)) if (!is_non_overflow(x, y))
return false; return false;
if (!c.is_strict && s().get_value(v).is_zero())
return false;
unsigned const lvl = c.src->level(); unsigned const lvl = c.src->level();
clause_builder reason(s()); clause_builder reason(s());
if (!c.is_strict)
reason.push(s().m_constraints.eq(lvl, x - x.manager().mk_val(rational(0))));
reason.push(~c.as_signed_constraint()); reason.push(~c.as_signed_constraint());
push_omega(reason, lvl, x, y); push_omega(reason, lvl, x, y);
return propagate(core, lvl, c.is_strict, y, z, reason); return propagate(core, lvl, c.is_strict, y, z, reason);