From 487a544274f9986ae62c314f2c67e84e2d1a36da Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 29 Jul 2024 21:05:41 -0700
Subject: [PATCH] remove test code

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/polysat/core.cpp          | 16 ++++++++--------
 src/sat/smt/polysat/op_constraint.cpp |  2 +-
 src/sat/smt/polysat/saturation.cpp    |  3 ---
 3 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index e9833bc19..ea3be3319 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -212,11 +212,11 @@ namespace polysat {
     sat::check_result core::check() {
         lbool r = l_true;
 
-        verbose_stream() << "check-propagate\n";
+        //verbose_stream() << "check-propagate\n";
         if (propagate())
             return sat::check_result::CR_CONTINUE;
 
-        verbose_stream() << "check-assign-variable\n";
+        //verbose_stream() << "check-assign-variable\n";
         switch (assign_variable()) {
         case l_true:
             break;
@@ -230,7 +230,7 @@ namespace polysat {
             break;
         }
 
-        verbose_stream() << "check-saturate\n";
+        //verbose_stream() << "check-saturate\n";
         saturation saturate(*this);
         switch (saturate()) {
         case l_true:
@@ -239,12 +239,12 @@ namespace polysat {
             TRACE("bv", tout << "saturate\n");
             return sat::check_result::CR_CONTINUE;
         case l_undef:
-            verbose_stream() << "giveup saturate\n";
+            //verbose_stream() << "giveup saturate\n";
             r = l_undef;
             break;
         }
         
-        verbose_stream() << "check-refine\n";
+        //verbose_stream() << "check-refine\n";
         switch (m_monomials.refine()) {
         case l_true:
             break;
@@ -252,12 +252,12 @@ namespace polysat {
             TRACE("bv", tout << "refine\n");
             return sat::check_result::CR_CONTINUE;
         case l_undef:
-            verbose_stream() << "giveup refine\n";
+            //verbose_stream() << "giveup refine\n";
             r = l_undef;
             break;
         }
 
-        verbose_stream() << "check-blast\n";
+        //verbose_stream() << "check-blast\n";
         switch (m_monomials.bit_blast()) {
         case l_true:
             break;
@@ -265,7 +265,7 @@ namespace polysat {
             TRACE("bv", tout << "blast\n");
             return sat::check_result::CR_CONTINUE;
         case l_undef:
-            verbose_stream() << "giveup blast\n";
+            //verbose_stream() << "giveup blast\n";
             r = l_undef;
             break;
         }
diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp
index c6022fadd..0b4c9c8cd 100644
--- a/src/sat/smt/polysat/op_constraint.cpp
+++ b/src/sat/smt/polysat/op_constraint.cpp
@@ -456,7 +456,7 @@ namespace polysat {
         auto rv = c.subst(r);
         auto& C = c.cs();
 
-        verbose_stream() << "saturate and: " << p << " & " << q << " = " << r << "\n";
+        //verbose_stream() << "saturate and: " << p << " & " << q << " = " << r << "\n";
 
         if (!pv.is_val() || !qv.is_val() || !rv.is_val())
             return false;
diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp
index 6c77bb657..d787da491 100644
--- a/src/sat/smt/polysat/saturation.cpp
+++ b/src/sat/smt/polysat/saturation.cpp
@@ -358,10 +358,7 @@ namespace polysat {
             return;
         if (a.degree(v) < r.degree(v))
             return;
-
-        verbose_stream() << "resolve: " << a << " = " << b << " => " << r << "\n";
         add_clause("ax + b = 0 & cx + d = 0 ==> cb - da = 0", { i.dep(), j.dep(), C.eq(r) }, true);
-        exit(0);
     }