mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #2586

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-26 08:59:52 -07:00
parent 79d4502771
commit deb45c09e8
1 changed files with 8 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/smt/theory_arith_core.h
View file

@ -280,14 +280,13 @@ namespace smt {
SASSERT(m_util.is_add(n)); SASSERT(m_util.is_add(n));
unsigned r_id = mk_row(); unsigned r_id = mk_row();
scoped_row_vars _sc(m_row_vars, m_row_vars_top); scoped_row_vars _sc(m_row_vars, m_row_vars_top);
unsigned num_args = n->get_num_args(); for (expr* arg : *n) {
for (unsigned i = 0; i < num_args; i++) { if (is_var(arg)) {
if (is_var(n->get_arg(i))) {
std::ostringstream strm; std::ostringstream strm;
strm << mk_pp(n, get_manager()) << " contains a free variable"; strm << mk_pp(n, get_manager()) << " contains a free variable";
throw default_exception(strm.str()); throw default_exception(strm.str());
} }
internalize_internal_monomial(to_app(n->get_arg(i)), r_id); internalize_internal_monomial(to_app(arg), r_id);
} }
enode * e = mk_enode(n); enode * e = mk_enode(n);
theory_var v = e->get_th_var(get_id()); theory_var v = e->get_th_var(get_id());
@ -315,13 +314,11 @@ namespace smt {
theory_var theory_arith<Ext>::internalize_mul_core(app * m) { theory_var theory_arith<Ext>::internalize_mul_core(app * m) {
TRACE("internalize_mul_core", tout << "internalizing...\n" << mk_pp(m,get_manager()) << "\n";); TRACE("internalize_mul_core", tout << "internalizing...\n" << mk_pp(m,get_manager()) << "\n";);
if (!m_util.is_mul(m)) if (!m_util.is_mul(m))
return internalize_term_core(m); return internalize_term_core(m);
for (unsigned i = 0; i < m->get_num_args(); i++) { for (expr* arg : *m) {
app * arg = to_app(m->get_arg(i)); theory_var v = internalize_term_core(to_app(arg));
SASSERT(!m_util.is_numeral(arg));
theory_var v = internalize_term_core(arg);
if (v == null_theory_var) { if (v == null_theory_var) {
mk_var(mk_enode(arg)); mk_var(mk_enode(to_app(arg)));
} }
} }
enode * e = mk_enode(m); enode * e = mk_enode(m);
@ -346,9 +343,7 @@ namespace smt {
if (m_util.is_numeral(arg1)) { if (m_util.is_numeral(arg1)) {
std::swap(arg0, arg1); std::swap(arg0, arg1);
} }
SASSERT(!m_util.is_numeral(arg1)); if (m_util.is_numeral(arg0, _val) && !m_util.is_numeral(arg1) && m->get_num_args() == 2) {
if (m_util.is_numeral(arg0, _val)) {
SASSERT(m->get_num_args() == 2);
numeral val(_val); numeral val(_val);
if (_val.is_zero()) { if (_val.is_zero()) {
return internalize_numeral(m, val); return internalize_numeral(m, val);