some fixes to backtracking restore points in new solver

Z3Prover · Nov 29, 2022 · 73a652c · 73a652c
1 parent dd1ca8f
commit 73a652c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
@@ -55,7 +55,7 @@ class dependent_expr_state {
     void push() { m_trail.push_scope(); }
     void pop(unsigned n) { m_trail.pop_scope(n); }
     unsigned qhead() const { return m_qhead; }
-    void advance_qhead() { m_qhead = size(); }
+    void advance_qhead() { if (m_trail.get_num_scopes() > 0) m_trail.push(value_trail(m_qhead));  m_qhead = size(); }
     unsigned num_exprs() {
         expr_fast_mark1 visited;
         unsigned r = 0;

diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp
@@ -259,6 +259,9 @@ class sat_smt_solver : public solver {
         m_map.push();
         m_preprocess_state.push();
         m_preprocess.push();
+        m_trail.push(restore_vector(m_assumptions));
+        m_trail.push(restore_vector(m_fmls));
+        m_trail.push(value_trail(m_mc_size));
     }
 
     void pop(unsigned n) override {
@@ -618,9 +621,6 @@ class sat_smt_solver : public solver {
             return l_true;
 
         unsigned qhead = m_preprocess_state.qhead();
-        m_trail.push(restore_vector(m_assumptions));
-        m_trail.push(restore_vector(m_fmls));
-        m_trail.push(value_trail(m_mc_size));
         TRACE("sat", tout << "qhead " << qhead << "\n");
 
         m_internalized_converted = false;