From 885dfad237e897920618641fafe1f1dd31c4a4f9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Feb 2018 20:54:21 -0800
Subject: [PATCH] fix #1458

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 91bff7406..4cb7339d1 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2715,6 +2715,7 @@ namespace sat {
 
     void solver::user_pop(unsigned num_scopes) {
         pop_to_base_level();
+        TRACE("sat", display(tout););
         while (num_scopes > 0) {
             literal lit = m_user_scope_literals.back();
             m_user_scope_literals.pop_back();
@@ -2734,8 +2735,10 @@ namespace sat {
                     break;
                 }
             }
-            gc_var(lit.var());
+            gc_var(lit.var());            
         }
+        m_qhead = 0;
+        propagate(false);
     }
 
     void solver::pop_to_base_level() {