From c629f09f21293f89c5e009f07c80061dce8dcdea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 29 Mar 2021 15:46:47 -0700
Subject: [PATCH] fix #5139

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

diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 3d8f0fe83..a41ff72b8 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -305,7 +305,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 if (m_euf) {
                     convert_euf(t, root, sign);  
                     return;
-                }
+                } 
                 if (!is_uninterp_const(t)) {
                     if (!is_app(t)) {
                         std::ostringstream strm;
@@ -938,14 +938,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     void user_push() {
-        push();
-        force_push();
     }
 
     void user_pop(unsigned n) {
-        m_true = sat::null_literal;
-        pop(n);
-        
+        m_true = sat::null_literal;   
     }
 
 };