mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-15 11:45:25 -08:00
parent 4eb3f5c630
commit c9472b01fe
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/op_constraint.cpp
View file

@ -184,8 +184,8 @@ namespace polysat {
return;
}
// q != 0 & p > 0 => r < p
if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && pv <= rv) {
s.add_clause(~lshr, s.eq(q()), s.ule(p, 0), s.ult(r(), p()), true);
if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && pv.val() <= rv.val()) {
s.add_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true);
return;
}
NOT_IMPLEMENTED_YET();