From 285ff9540d0d64dcf33aa4787f61903f271faacf Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 9 Mar 2020 11:01:10 -0700 Subject: [PATCH] make sure that the term external index has not been used Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index ecf34e18a..50ca3375f 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -2371,6 +2371,8 @@ std::pair lar_solver::add_equality(lpvar j, coeffs.push_back(std::make_pair(mpq(1),j)); coeffs.push_back(std::make_pair(mpq(-1),k)); unsigned ext_term_index = m_terms.size(); + while (m_term_register.external_is_used(ext_term_index)) + ext_term_index *= 2; unsigned term_index = add_term(coeffs, ext_term_index); return std::pair( add_var_bound(term_index, lconstraint_kind::LE, mpq(0)),