From 2be71cfc43c80a03b9bc680190b5fe8019ff8e47 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jan 2022 15:17:37 -0800 Subject: [PATCH] #5753 --- src/sat/smt/arith_internalize.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 882dd23b0..d81efc43b 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -545,11 +545,13 @@ namespace arith { } m_left_side.clear(); // reset the coefficients after they have been used. - for (unsigned i = 0; i < vars.size(); ++i) { - theory_var var = vars[i]; + for (theory_var var : vars) { rational const& r = m_columns[var]; if (!r.is_zero()) { - m_left_side.push_back(std::make_pair(r, register_theory_var_in_lar_solver(var))); + auto vi = register_theory_var_in_lar_solver(var); + if (lp::tv::is_term(vi)) + vi = lp().map_term_index_to_column_index(vi); + m_left_side.push_back(std::make_pair(r, vi)); m_columns[var].reset(); } }