From ad309e53a12d41c2b7a2dd50093052619a02fb60 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Dec 2019 16:06:14 -0800 Subject: [PATCH] fix #2766 --- src/smt/theory_dense_diff_logic_def.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 864ead77e..13b7f5dc4 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -150,13 +150,13 @@ namespace smt { numeral offset(_k); app * s, * t; expr *arg1, *arg2; - if (m_autil.is_add(lhs, arg1, arg2) && is_times_minus_one(arg2, s)) { + if (m_autil.is_add(lhs, arg1, arg2) && is_times_minus_one(arg2, s) && !m_autil.is_arith_expr(s) && !m_autil.is_arith_expr(arg1)) { t = to_app(arg1); } - else if (m_autil.is_add(lhs, arg1, arg2) && is_times_minus_one(arg1, s)) { + else if (m_autil.is_add(lhs, arg1, arg2) && is_times_minus_one(arg1, s) && !m_autil.is_arith_expr(s) && !m_autil.is_arith_expr(arg2)) { t = to_app(arg2); } - else if (m_autil.is_mul(lhs, arg1, arg2) && m_autil.is_minus_one(arg1)) { + else if (m_autil.is_mul(lhs, arg1, arg2) && m_autil.is_minus_one(arg1) && !m_autil.is_arith_expr(arg2)) { s = to_app(arg2); t = mk_zero_for(s); }