From 9af86f2d6864e66451319bbb6f5da6155de3f390 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 16 Mar 2023 16:13:13 +0100
Subject: [PATCH] debug output

---
 src/math/polysat/solver.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 31a7251b4..a3cb46fdc 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1577,8 +1577,12 @@ namespace polysat {
         out << "Clauses:\n";
         for (clause const& cl : m_constraints.clauses()) {
             out << "\t" << cl << "\n";
-            for (sat::literal lit : cl)
-                out << "\t\t" << lit_pp(*this, lit) << "\n";
+            for (sat::literal lit : cl) {
+                out << "\t\t" << lit_pp(*this, lit);
+                if (count(m_bvars.watch(lit), &cl) != 0)
+                    out << " (bool-watched)";
+                out << "\n";
+            }
         }
         return out;
     }
@@ -1612,6 +1616,7 @@ namespace polysat {
             else if (s.m_bvars.is_decision(lit))
                 out << "decide";
             out << '@' << s.m_bvars.level(lit);
+            out << " idx:" << s.m_search.get_bool_index(lit);
         }
         if (c->is_pwatched())
             out << " pwatched";