From 46c6a5492e9a60e1bee7cdba70304eb49cc58cbb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Mar 2020 18:22:04 -0700
Subject: [PATCH] fix assertion in emonics, exposed by #3318

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/emonics.cpp  | 8 +++++---
 src/math/lp/nla_core.cpp | 1 +
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index e110c3092..dab621bf9 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -225,6 +225,7 @@ void emonics::insert_cg(lpvar v) {
     do {
         unsigned idx = c->m_index;
         c = c->m_next;
+        TRACE("nla_solver_mons", tout << "inserting v" << v << " for " << idx << "\n";);
         monic & m = m_monics[idx];
         if (!is_visited(m)) {
             set_visited(m);
@@ -459,7 +460,7 @@ std::ostream& emonics::display(std::ostream& out) const {
         out << "m" << (idx++) << ": " << m << "\n";
     }    
     display_use(out);
-    //display_uf(out);
+    display_uf(out);
     out << "table:\n";
     for (auto const& k : m_cg_table) {
         out << k.m_key << ": " << k.m_value << "\n";
@@ -506,6 +507,7 @@ std::ostream& emonics::display(std::ostream& out, cell* c) const {
 
 
 bool emonics::invariant() const {
+    TRACE("nla_solver_mons", display(tout););
     // the varible index contains exactly the active monomials
     unsigned mons = 0;
     for (lpvar v = 0; v < m_var2index.size(); v++) {
@@ -528,11 +530,11 @@ bool emonics::invariant() const {
                 bool found = false;
                 for (lp::var_index w : m.vars()) {
                     auto w1 = m_ve.find(w);
-                    found |= v1 == w1;
+                    found |= v1.var() == w1.var();
                 }
                 for (lp::var_index w : m.rvars()) {
                     auto w1 = m_ve.find(w);
-                    found |= v1 == w1;
+                    found |= v1.var() == w1.var();
                 }
                 CTRACE("nla_solver_mons", !found, tout << v << ": " << m << "\n";);
                 SASSERT(found);
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index ae17a646a..422947b1a 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -950,6 +950,7 @@ void core::clear() {
     
 void core::init_search() {
     TRACE("nla_solver_mons", tout << "init\n";);
+    SASSERT(m_emons.invariant());
     clear();
     init_vars_equivalence();
     SASSERT(m_emons.invariant());