mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bug in context push/pop for sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
82f1e81ac2
commit
f1d9228b94
|
@ -925,7 +925,7 @@ public:
|
|||
}
|
||||
|
||||
void verify_assignment() {
|
||||
IF_VERBOSE(0, verbose_stream() << "verify assignment\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "verify assignment\n";);
|
||||
ref<solver> smt_solver = mk_smt_solver(m, m_params, symbol());
|
||||
for (unsigned i = 0; i < s().get_num_assertions(); ++i) {
|
||||
smt_solver->assert_expr(s().get_assertion(i));
|
||||
|
|
|
@ -930,8 +930,11 @@ namespace sat {
|
|||
|
||||
void solver::reinit_assumptions() {
|
||||
if (tracking_assumptions() && scope_lvl() == 0) {
|
||||
TRACE("sat", tout << m_assumptions.size() << "\n";);
|
||||
TRACE("sat", tout << m_assumptions << "\n";);
|
||||
push();
|
||||
for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
|
||||
assign(~m_user_scope_literals[i], justification());
|
||||
}
|
||||
for (unsigned i = 0; !inconsistent() && i < m_assumptions.size(); ++i) {
|
||||
assign(m_assumptions[i], justification());
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue