From c87aa8bcf8a1a3cd502d91392b71a828d93b6684 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 23 Oct 2023 15:24:27 +0200
Subject: [PATCH] fix slice_pp

---
 src/math/polysat/slicing.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index 35e93a7d2..0b3119392 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -1556,18 +1556,18 @@ namespace polysat {
 
     std::ostream& slicing::display(std::ostream& out, enode* s) const {
         out << "{id:" << s->get_id();
+        if (is_equality(s))
+            return out << ",<equality>}";
         out << ",w:" << width(s);
         out << ",root:" << s->get_root_id();
         if (slice2var(s) != null_var)
             out << ",var:v" << slice2var(s);
-        if (is_value(s))
-            out << ",value:" << get_value(s);
+        if (enode* n = get_value_node(s))
+            out << ",value:" << get_value(n);
         if (s->interpreted())
             out << ",<interpreted>";
         if (is_concat(s))
             out << ",<concat>";
-        if (is_equality(s))
-            out << ",<equality>";
         out << "}";
         return out;
     }