From cd48a5164e8009271fed347d8599ddf2f39f3c46 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 29 Mar 2013 17:05:17 -0700
Subject: [PATCH] fix bug in hilbert_basis reset method. Missing reset of
 m_iseq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/hilbert_basis.cpp | 22 ++++++++++++++++------
 src/test/hilbert_basis.cpp   | 20 +++++++++++++++++++-
 2 files changed, 35 insertions(+), 7 deletions(-)

diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp
index 7aed98487..7b3e67487 100644
--- a/src/muz_qe/hilbert_basis.cpp
+++ b/src/muz_qe/hilbert_basis.cpp
@@ -731,16 +731,26 @@ bool hilbert_basis::is_invalid_offset(offset_t offs) {
 
 void hilbert_basis::reset() {
     m_ineqs.reset();
-    m_basis.reset();
+    m_iseq.reset();
     m_store.reset();
+    m_basis.reset();
     m_free_list.reset();
-    m_active.reset();
-    m_passive->reset();
-    m_passive2->reset();
+    m_sos.reset();
     m_zero.reset();
-    m_index->reset(1);
-    m_ints.reset();
+    m_active.reset();
+    if (m_passive) {
+        m_passive->reset();
+    }
+    if (m_passive2) {
+        m_passive2->reset();
+    }
     m_cancel = false;
+    if (m_index) {
+        m_index->reset(1);
+    }
+    m_ints.reset();
+    m_current_ineq = 0;
+    
 }
 
 void hilbert_basis::collect_statistics(statistics& st) const {
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index 2f58cc3c8..e0a4a8370 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -524,6 +524,20 @@ static void tst17() {
 
 }
 
+static void tst18() {
+    hilbert_basis hb;
+    hb.add_eq(vec(0, 1), R(0));
+    hb.add_eq(vec(1, -1), R(2));
+    saturate_basis(hb);    
+}
+
+static void tst19() {
+    hilbert_basis hb;
+    hb.add_eq(vec(0,  1, 0), R(0));
+    hb.add_eq(vec(1, -1, 0), R(2));
+    saturate_basis(hb);    
+}
+
 void tst_hilbert_basis() {
     std::cout << "hilbert basis test\n";
 //    tst3();
@@ -531,9 +545,13 @@ void tst_hilbert_basis() {
 
     g_use_ordered_support = true;
 
-    tst17();
+    tst18();
     return;
 
+    tst19();
+    return;
+    tst17();
+
     if (true) {
         tst1();
         tst2();