From d3a7ebee02f7e35e2ac9450bff1a4f3db4ec7883 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Mar 2020 10:01:32 -0700
Subject: [PATCH] fix #3338

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/emonics.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 7af42e855..1aeec2a2d 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -514,6 +514,10 @@ bool emonics::invariant() const {
                     auto w1 = m_ve.find(w);
                     found |= v1 == w1;
                 }
+                for (lp::var_index w : m.rvars()) {
+                    auto w1 = m_ve.find(w);
+                    found |= v1 == w1;
+                }
                 CTRACE("nla_solver_mons", !found, tout << v << ": " << m << "\n";);
                 SASSERT(found);
                 c = c->m_next;