mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

fix #1358

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-15 20:32:37 -08:00
parent 61d149a724
commit 58be777307
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/arith/diff_neq_tactic.cpp
View file

@ -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) { if (is_uninterp_const(lhs) && u.is_numeral(rhs, k) && m_max_neg_k <= k && k <= m_max_k) {
var x = mk_var(lhs); var x = mk_var(lhs);
int _k = static_cast<int>(k.get_int64()); int _k = static_cast<int>(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) { 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); var x = mk_var(rhs);
int _k = static_cast<int>(k.get_int64()); int _k = static_cast<int>(k.get_int64());
m_lower[x] = _k; m_lower[x] = std::max(m_lower[x], _k);
} }
else { else {
throw_not_supported(); throw_not_supported();