From 38e85a72881d46153bd8561e454599bdf851689f Mon Sep 17 00:00:00 2001
From: calebstanford-msr <t-casta@microsoft.com>
Date: Mon, 8 Jun 2020 13:18:40 -0400
Subject: [PATCH] remove debugging statements for PR

---
 src/ast/rewriter/seq_rewriter.cpp | 4 ----
 src/smt/seq_regex.cpp             | 9 ---------
 2 files changed, 13 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 9036a409c..c1d4b3004 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2155,14 +2155,10 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) {
 }
 
 expr_ref seq_rewriter::is_nullable_rec(expr* r) {
-    std::cout << "n";
     expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr, nullptr), m());
     if (!result) {
-        std::cout << "(m) ";
         result = is_nullable(r);
         m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result);
-    } else {
-        std::cout << "(h) ";
     }
     return result;
 }
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index b87beeeb2..6044f0275 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -101,8 +101,6 @@ namespace smt {
         expr* e = ctx.bool_var2expr(lit.var());
         VERIFY(str().is_in_re(e, s, r));
 
-        std::cout << "PI ";
-
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
         // convert negative negative membership literals to positive
@@ -144,7 +142,6 @@ namespace smt {
     }
 
     void seq_regex::propagate_accept(literal lit) {
-        std::cout << "PA ";
         if (!propagate(lit))
             m_to_propagate.push_back(lit);
     }
@@ -172,8 +169,6 @@ namespace smt {
 
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
-        std::cout << "P ";
-
         if (re().is_empty(r)) {
             th.add_axiom(~lit);
             return true;
@@ -361,10 +356,8 @@ namespace smt {
         with optimizations for if-then-else expressions involving the head.
     */
     expr_ref seq_regex::derivative_wrapper(expr* hd, expr* r) {
-        std::cout << "D ";
         expr_ref result = expr_ref(re().mk_derivative(hd, r), m);
         rewrite(result);
-        std::cout << std::endl << "Derivative result: " << result << std::endl;
         return result;
     }
 
@@ -400,7 +393,6 @@ namespace smt {
      *
      */
     void seq_regex::propagate_is_non_empty(literal lit) {
-        std::cout << "PN ";
         expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
         VERIFY(sk().is_is_non_empty(e, r, u));
         expr_ref is_nullable = seq_rw().is_nullable(r);
@@ -456,7 +448,6 @@ namespace smt {
       is_empty(r, u) is true if r is a member of u
      */
     void seq_regex::propagate_is_empty(literal lit) {
-        std::cout << "PE ";
         expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
         VERIFY(sk().is_is_empty(e, r, u));
         expr_ref is_nullable = seq_rw().is_nullable(r);