From 846a9fc25f4d0d18aa15be4c0a0e446b872171df Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 12 Mar 2020 19:08:15 -0700
Subject: [PATCH] consistent

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/emonics.cpp  |  3 ++-
 src/math/lp/emonics.h    | 11 ++++++++++-
 src/math/lp/nla_core.cpp |  1 +
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 85ceb41c1..61a619169 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -42,6 +42,7 @@ void emonics::push() {
     m_region.push_scope();
     m_ve.push();
     SASSERT(monics_are_canonized());
+    SASSERT(consistent());
 }
 
 void emonics::pop(unsigned n) {
@@ -63,6 +64,7 @@ void emonics::pop(unsigned n) {
     m_monics.shrink(old_sz);
     m_region.pop_scope(n);
     m_lim.shrink(m_lim.size() - n);
+    SASSERT(consistent());
     SASSERT(monics_are_canonized());
     m_u_f_stack.pop_scope(n);
 }
@@ -288,7 +290,6 @@ void emonics::add(lpvar v, unsigned sz, lpvar const* vs) {
     lpvar last_var = UINT_MAX;
     for (unsigned i = 0; i < sz; ++i) {
         lpvar w = vs[i];
-        SASSERT(m_ve.is_root(w));
         if (w != last_var) {
             m_use_lists.reserve(w + 1);
             insert_cell(m_use_lists[w], idx);
diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h
index 7daa1281f..260c29159 100644
--- a/src/math/lp/emonics.h
+++ b/src/math/lp/emonics.h
@@ -107,7 +107,6 @@ class emonics {
     void insert_cg_mon(monic & m);
     void remove_cg_mon(const monic & m);
     void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); }
-
     void do_canonize(monic& m) const; 
     cell* head(lpvar v) const;
     void set_visited(monic& m) const;
@@ -328,6 +327,16 @@ public:
     bool is_used_in_monic(lpvar v) const { return v < m_use_lists.size() && m_use_lists[v].m_head != nullptr; }
 
     bool elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector> &lists) const;
+
+    bool consistent() const {
+        unsigned mons = 0;
+        for (lpvar v = 0; v < m_var2index.size(); v++) {
+            if (is_monic_var(v)) {
+                mons ++;
+            }
+        }
+        return m_monics.size() == mons;
+    }
     
 }; // end of emonics
 
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 2a2043604..e3adfd7fa 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -960,6 +960,7 @@ void core::clear() {
 void core::init_search() {
     clear();
     init_vars_equivalence();
+    SASSERT(m_emons.consistent());
     SASSERT(elists_are_consistent(false));
 }