From 40d90a951c56c273764897ec7dad051ecb5326ba Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 10 Nov 2016 16:52:56 +0000
Subject: [PATCH] Fixed interruption cleanup bug in sat_solver. Relates to
 #570.

---
 src/sat/sat_solver.h | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 85836b889..c0d736ebf 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -237,7 +237,10 @@ namespace sat {
         lbool status(clause const & c) const;        
         clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
         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;
             if (m_num_checkpoints < 10) return;
             m_num_checkpoints = 0;