mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #4430

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-03 13:47:50 -07:00
parent 9fac010d8e
commit d50fc6976b
1 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/nlsat/nlsat_solver.cpp
View file

@ -1961,6 +1961,13 @@ namespace nlsat {
return new_lvl; return new_lvl;
} }
struct scoped_reset_marks {
imp& i;
scoped_reset_marks(imp& i):i(i) {}
~scoped_reset_marks() { if (i.m_num_marks > 0) { i.m_num_marks = 0; for (char& m : i.m_marks) m = 0; } }
};
/** /**
\brief Return true if the conflict was solved. \brief Return true if the conflict was solved.
*/ */
@ -1980,7 +1987,7 @@ namespace nlsat {
m_num_marks = 0; m_num_marks = 0;
m_lemma.reset(); m_lemma.reset();
m_lemma_assumptions = nullptr; m_lemma_assumptions = nullptr;
scoped_reset_marks _sr(*this);
resolve_clause(null_bool_var, *conflict_clause); resolve_clause(null_bool_var, *conflict_clause);
unsigned top = m_trail.size(); unsigned top = m_trail.size();