mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-02 15:40:45 -07:00
parent 3f3bd5948f
commit 48e663776b
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -425,11 +425,13 @@ namespace polysat {
new_constraints.push_back(c.as_signed_constraint());
if (c.is_strict) {
new_constraints.push_back(s.ule(l_val, c.lhs));
return propagate(core, c, c, s.ult(r_val, c.rhs), new_constraints);
auto conseq = s.ult(r_val, c.rhs);
return propagate(core, c, c, conseq, new_constraints);
}
else {
new_constraints.push_back(s.ule(c.rhs, r_val));
return propagate(core, c, c, s.ule(c.lhs, r_val), new_constraints);
auto conseq = s.ule(c.lhs, r_val);
return propagate(core, c, c, conseq, new_constraints);
}
}