From b70cc47a9d5b60aa11db97a93774fbd429cbc70d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 23 Aug 2016 18:46:14 +0100
Subject: [PATCH] x64 clause allocator fix for del_clause

---
 src/sat/sat_clause.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index 845f864f7..0f7d0d8a4 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -207,6 +207,11 @@ namespace sat {
     void clause_allocator::del_clause(clause * cls) {
         TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
         m_id_gen.recycle(cls->id());
+#if defined(_AMD64_)
+#if defined(Z3DEBUG)
+        m_last_seg_id2cls.remove(cls->id());
+#endif
+#endif
         size_t size = clause::get_obj_size(cls->m_capacity);
         cls->~clause();
         m_allocator.deallocate(size, cls);