From 7343783efef12b657d451729cab40ef3bc0fffd1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 1 Jun 2020 15:40:02 -0700
Subject: [PATCH] finetune

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 8775785b3..1f7094886 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2424,11 +2424,13 @@ public:
     }
 
     void add_eq(lpvar u, lpvar v, lp::explanation const& e) {
+        if (ctx().inconsistent())
+            return;
         theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations
         theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
         enode* n1 = get_enode(uv);
         enode* n2 = get_enode(vv);
-        if (n1 == n2)
+        if (n1->get_root() == n2->get_root())
             return;
         reset_evidence();
         for (auto const& ev : e) 
@@ -2442,7 +2444,6 @@ public:
         ctx().assign_eq(n1, n2, eq_justification(js));        
     }
 
-
     literal_vector m_core2;
 
     void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params) {