mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Fixed interruption cleanup bug in sat_solver. Relates to #570.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-10 16:52:56 +00:00
parent d099e26342
commit 520e868add
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/sat_solver.h
View file

@ -237,7 +237,10 @@ namespace sat {
lbool status(clause const & c) const; lbool status(clause const & c) const;
clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); } clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
void checkpoint() { void checkpoint() {
if (!m_rlimit.inc()) { throw solver_exception(Z3_CANCELED_MSG); } if (!m_rlimit.inc()) {
m_mc.reset();
throw solver_exception(Z3_CANCELED_MSG);
}
++m_num_checkpoints; ++m_num_checkpoints;
if (m_num_checkpoints < 10) return; if (m_num_checkpoints < 10) return;
m_num_checkpoints = 0; m_num_checkpoints = 0;