From 58be77730746a357bf3d7123df9d5ceac49cc40f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 20:32:37 -0800 Subject: [PATCH] fix #1358 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/diff_neq_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 651000297..c66483750 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -95,13 +95,13 @@ class diff_neq_tactic : public tactic { if (is_uninterp_const(lhs) && u.is_numeral(rhs, k) && m_max_neg_k <= k && k <= m_max_k) { var x = mk_var(lhs); int _k = static_cast(k.get_int64()); - m_upper[x] = _k; + m_upper[x] = std::min(m_upper[x], _k); } else if (is_uninterp_const(rhs) && u.is_numeral(lhs, k) && m_max_neg_k <= k && k <= m_max_k) { var x = mk_var(rhs); int _k = static_cast(k.get_int64()); - m_lower[x] = _k; + m_lower[x] = std::max(m_lower[x], _k); } else { throw_not_supported();