From 045b5ed6835b28d1bb6000b1dbacfec9ca779c8f Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 24 Oct 2023 11:22:04 +0200
Subject: [PATCH] mark

---
 src/math/polysat/slicing.cpp | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index c2e8f3739..d05516062 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -802,17 +802,26 @@ namespace polysat {
             dep_t const d = dep_t::decode(dp);
             if (d.is_null())
                 continue;
-            if (d.is_lit())
-                on_lit(d.lit());
+            if (d.is_lit()) {
+                sat::literal const lit = d.lit();
+                if (!m_marked_lits.contains(lit)) {
+                    on_lit(lit);
+                    m_marked_lits.insert(lit);
+                }
+            }
             else {
                 SASSERT(d.is_value());
-                if (get_dep_lit(d) == sat::null_literal)
+                sat::literal const lit = get_dep_lit(d);
+                if (lit == sat::null_literal)
                     on_var(get_dep_var(d));
-                else
-                    on_lit(get_dep_lit(d));
+                else if (!m_marked_lits.contains(lit)) {
+                    on_lit(lit);
+                    m_marked_lits.insert(lit);
+                }
             }
         }
         m_tmp_deps.reset();
+        m_marked_lits.reset();
     }
 
     void slicing::explain_value(pvar v, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {