mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #2766

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-01 16:06:14 -08:00
parent 9ebaf19e47
commit ad309e53a1
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_dense_diff_logic_def.h
View file

@ -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);
}