From 73a652cf4b60bc382b676da2b96a8b5bd359e342 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Nov 2022 16:42:42 +0700 Subject: [PATCH] some fixes to backtracking restore points in new solver --- src/ast/simplifiers/dependent_expr_state.h | 2 +- src/sat/sat_solver/sat_smt_solver.cpp | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 54ee5626b..a65492a58 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -55,7 +55,7 @@ public: 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 index 2d95dab69..91a2bfec2 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -259,6 +259,9 @@ public: 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 @@ private: 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;