From 2683a2d6ed9039ddd1a59aeccbdd91f67f7b708a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Mar 2023 08:49:33 +0100 Subject: [PATCH] fix #6637 --- src/math/lp/nla_divisions.cpp | 5 +++-- src/sat/smt/euf_proof_checker.h | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_divisions.cpp b/src/math/lp/nla_divisions.cpp index 91b674d58..cbb30d9d9 100644 --- a/src/math/lp/nla_divisions.cpp +++ b/src/math/lp/nla_divisions.cpp @@ -58,10 +58,11 @@ namespace nla { auto monotonicity1 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { - if (y1val >= y2val && y2val > 0 && x1val <= x2val && q1val > q2val) { - new_lemma lemma(c, "y1 >= y2 > 0 & x1 <= x2 => x1/y1 <= x2/y2"); + if (y1val >= y2val && y2val > 0 && 0 <= x1val && x1val <= x2val && q1val > q2val) { + new_lemma lemma(c, "y1 >= y2 > 0 & 0 <= x1 <= x2 => x1/y1 <= x2/y2"); lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0); lemma |= ineq(y2, llc::LE, 0); + lemma |= ineq(x1, llc::LT, 0); lemma |= ineq(term(x1, rational(-1), x2), llc::GT, 0); lemma |= ineq(term(q1, rational(-1), q2), llc::LE, 0); return true; diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h index 9a84015e4..d84e4d19f 100644 --- a/src/sat/smt/euf_proof_checker.h +++ b/src/sat/smt/euf_proof_checker.h @@ -35,7 +35,7 @@ namespace euf { virtual bool check(app* jst) = 0; virtual expr_ref_vector clause(app* jst) = 0; virtual void register_plugins(theory_checker& pc) = 0; - virtual bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) { v.reset(); v.append(this->clause(jst)); return false; } + virtual bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) { v.append(this->clause(jst)); return false; } }; class theory_checker {