From 13f000942a96d872c017084c61524808b4d5836b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 3 Aug 2023 11:41:13 +0200
Subject: [PATCH] fix viable

---
 src/math/polysat/forbidden_intervals.cpp |  4 ++++
 src/math/polysat/forbidden_intervals.h   | 10 +++++++++-
 src/math/polysat/viable.cpp              |  4 +---
 3 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index 0642c23aa..ffafdde59 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -29,6 +29,10 @@ namespace polysat {
      * \returns True iff a forbidden interval exists and the output parameters were set.
      */
     bool forbidden_intervals::get_interval(signed_constraint const& c, pvar v, fi_record& fi) {
+        // verbose_stream() << "get_interval for v" << v << "    " << c << "\n";
+        SASSERT(fi.side_cond.empty());
+        SASSERT(fi.src.empty());
+        fi.bit_width = s.size(v);  // TODO: preliminary
         if (c->is_ule())
             return get_interval_ule(c, v, fi);
         if (c->is_umul_ovfl())
diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h
index f53baf489..3c549131f 100644
--- a/src/math/polysat/forbidden_intervals.h
+++ b/src/math/polysat/forbidden_intervals.h
@@ -25,11 +25,19 @@ namespace polysat {
         vector<signed_constraint>   side_cond;
         vector<signed_constraint>   src;        // only units may have multiple src (as they can consist of contracted bit constraints)
         rational                    coeff;
-        unsigned                    bit_width;  // number of lower bits
+        unsigned                    bit_width = 0;  // number of lower bits
 
         /** Create invalid fi_record */
         fi_record(): interval(eval_interval::full()) {}
 
+        void reset() {
+            interval = eval_interval::full();
+            side_cond.reset();
+            src.reset();
+            coeff.reset();
+            bit_width = 0;
+        }
+
         struct less {
             bool operator()(fi_record const& a, fi_record const& b) const {
                 return a.interval.lo_val() < b.interval.lo_val();
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index a3ef3605e..cc7298b88 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -78,10 +78,8 @@ namespace polysat {
         if (m_alloc.empty())
             return alloc(entry);
         auto* e = m_alloc.back();
-        e->src.reset();
-        e->side_cond.reset();
+        e->fi_record::reset();
         e->refined.reset();
-        e->coeff = 1;
         m_alloc.pop_back();
         return e;
     }