From c9472b01fe5792507fe63fb53f60aac0bce35666 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Dec 2021 11:45:25 -0800 Subject: [PATCH] fixes Signed-off-by: Nikolaj Bjorner --- src/math/polysat/op_constraint.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 203693221..17f3164c7 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -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();