From fc3a7018888c1f507d191d6c4799ea966bd8de70 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Oct 2021 15:36:48 -0700
Subject: [PATCH] push-pop

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

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 0bbce0993..2af8485c1 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -528,6 +528,7 @@ namespace euf {
         m_egraph.push();
         if (m_dual_solver)
             m_dual_solver->push();
+        push_relevant();
     }
 
     void solver::pop(unsigned n) {
@@ -537,6 +538,7 @@ namespace euf {
             e->pop(n);
         si.pop(n);
         m_egraph.pop(n);
+        pop_relevant(n);
         scope const & sc = m_scopes[m_scopes.size() - n];
         for (unsigned i = m_var_trail.size(); i-- > sc.m_var_lim; ) {
             bool_var v = m_var_trail[i];