From 586dcba661f7823d6e4e593ef14cc68ff8a08bf5 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 11 Aug 2023 14:49:17 +0200
Subject: [PATCH] slicing::collect_fixed should start at low-order base slice

---
 src/math/polysat/slicing.cpp | 6 ++++--
 src/math/polysat/slicing.h   | 4 +++-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index ff2bfa577..c846aff4f 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -1371,14 +1371,16 @@ namespace polysat {
         get_base(var2slice(v), base);
         rational a;
         unsigned lo = 0;
-        for (enode* n : base) {
-            enode* r = n->get_root();
+        for (auto it = base.rbegin(); it != base.rend(); ++it) {
+            enode* const n = *it;
+            enode* const r = n->get_root();
             unsigned const w = width(n);
             unsigned const hi = lo + w - 1;
             if (try_get_value(r, a))
                 out.push_back({hi, lo, a, n});
             lo += w;
         }
+        base.reset();
     }
 
     void slicing::explain_fixed(euf::enode* const n, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index 33bd859ce..41aeec8c3 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -39,9 +39,11 @@ namespace polysat {
 
         friend class test_slicing;
 
+    public:
         using enode = euf::enode;
         using enode_vector = euf::enode_vector;
 
+    private:
         class dep_t {
             std::variant<std::monostate, sat::literal, unsigned> m_data;
         public:
@@ -351,7 +353,7 @@ namespace polysat {
 
         /** Collect fixed portions of the variable v */
         void collect_fixed(pvar v, justified_fixed_bits_vector& out);
-        void explain_fixed(euf::enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
+        void explain_fixed(enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
 
         std::ostream& display(std::ostream& out) const;
         std::ostream& display_tree(std::ostream& out) const;