From e9069309229259f9c13b38d01f4ca00104351772 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Sat, 23 Jun 2018 00:06:27 -0400
Subject: [PATCH] Debug code

---
 src/muz/spacer/spacer_iuc_solver.cpp | 34 ++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp
index a68db4c0a..27b8ee357 100644
--- a/src/muz/spacer/spacer_iuc_solver.cpp
+++ b/src/muz/spacer/spacer_iuc_solver.cpp
@@ -322,6 +322,24 @@ void iuc_solver::get_iuc(expr_ref_vector &core)
         // -- new hypothesis reducer
         else
         {
+#if 0
+            static unsigned bcnt = 0;
+            {
+                bcnt++;
+                TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";);
+                if (bcnt == 123) {
+                    std::ofstream ofs;
+                    ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot");
+                    iuc_proof iuc_pf_before(m, res.get(), core_lits);
+                    iuc_pf_before.display_dot(ofs);
+                    ofs.close();
+
+                    proof_checker pc(m);
+                    expr_ref_vector side(m);
+                    ENSURE(pc.check(res, side));
+                }
+            }
+#endif
             scoped_watch _t_ (m_hyp_reduce2_sw);
 
             // pre-process proof for better iuc extraction
@@ -356,6 +374,22 @@ void iuc_solver::get_iuc(expr_ref_vector &core)
 
         iuc_proof iuc_pf(m, res, core_lits);
 
+#if 0
+        static unsigned cnt = 0;
+        {
+            cnt++;
+            TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";);
+            if (cnt == 123) {
+                std::ofstream ofs;
+                ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot");
+                iuc_pf.display_dot(ofs);
+                ofs.close();
+                proof_checker pc(m);
+                expr_ref_vector side(m);
+                ENSURE(pc.check(res, side));
+            }
+        }
+#endif
         unsat_core_learner learner(m, iuc_pf);
 
         unsat_core_plugin* plugin;