fix #5139

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Mar 29, 2021 · c629f09 · c629f09
1 parent 94b4d1b
commit c629f09
Showing 1 changed file with 2 additions and 6 deletions.
diff --git 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;   
     }
 
 };