diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index df494ec42..61094c29c 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -187,9 +187,11 @@ public:
         switch_inc_mode();
         m_solver1->push();
         m_solver2->push();        
+        TRACE("pop", tout << "push\n";);
     }
     
     void pop(unsigned n) override {
+        TRACE("pop", tout << n << "\n";);
         switch_inc_mode();
         m_solver1->pop(n);
         m_solver2->pop(n);
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 85d3b483d..0c791fe5a 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -122,9 +122,11 @@ void tactic2solver::assert_expr_core(expr * t) {
 void tactic2solver::push_core() {
     m_scopes.push_back(m_assertions.size());
     m_result = nullptr;
+    TRACE("pop", tout << m_scopes.size() << "\n";);
 }
 
 void tactic2solver::pop_core(unsigned n) {
+    TRACE("pop", tout << m_scopes.size() << " " << n << "\n";);
     n = std::min(m_scopes.size(), n);
     unsigned new_lvl = m_scopes.size() - n;
     unsigned old_sz  = m_scopes[new_lvl];