From bc5b68b16e0d2d46fa1487e88d0f247c31e4fd88 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 24 Mar 2020 12:44:50 -0700
Subject: [PATCH] convert term indices to columns in lar_solver::add_equality()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/lar_solver.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 4c5dd64d2..acd21b79e 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2364,6 +2364,12 @@ bool lar_solver::fetch_normalized_term_column(const lar_term& c, std::pair<mpq,
 
 std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j, lpvar k) {
     vector<std::pair<mpq, var_index>> coeffs;
+    if (tv::is_term(j))
+        j = map_term_index_to_column_index(j);
+
+    if (tv::is_term(k))
+        k = map_term_index_to_column_index(k);
+    
     coeffs.push_back(std::make_pair(mpq(1),j));
     coeffs.push_back(std::make_pair(mpq(-1),k));    
     unsigned term_index = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var