From bffe7a2215032116cc0d9d0ae45988d61b19bfbc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 12:19:34 -0700 Subject: [PATCH] fix #3783 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arith_plugin.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index f72c9fbe1..20ea09d2f 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -1031,26 +1031,27 @@ namespace qe { app_ref x(m_ctx.get_var(index-1), m); app_ref z(m); expr_ref p1(m); + sort* s = m.get_sort(p); if (is_aux) { // An auxiliary variable was introduced in lieu of 'x'. // it has coefficient 'm' = values[index]. SASSERT(values[index] >= rational(3)); - z = m.mk_fresh_const("x", m_arith.mk_int()); + z = m.mk_fresh_const("x", s); add_var(z); - p1 = m_arith.mk_mul(m_arith.mk_numeral(values[index], true), z); + p1 = m_arith.mk_mul(m_arith.mk_numeral(values[index], s), z); } else { // the coefficient to 'x' is -1. - p1 = m_arith.mk_numeral(numeral(0), true); + p1 = m_arith.mk_numeral(numeral(0), s); } for (unsigned i = 1; i <= num_vars; ++i) { numeral k = values[i]; if (!k.is_zero() && i != index) { - p1 = m_arith.mk_add(p1, m_arith.mk_mul(m_arith.mk_numeral(k, true), m_ctx.get_var(i-1))); + p1 = m_arith.mk_add(p1, m_arith.mk_mul(m_arith.mk_numeral(k, s), m_ctx.get_var(i-1))); } } - p1 = m_arith.mk_add(p1, m_arith.mk_numeral(values[0], true)); + p1 = m_arith.mk_add(p1, m_arith.mk_numeral(values[0], s)); TRACE("qe", tout << "is linear:\n"