From 1e9206e01aaf2eeb9407cc58791e3dbd185387c2 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Fri, 1 Jul 2022 14:11:30 +0200
Subject: [PATCH] Remove error output.

---
 libsolutil/BooleanLP.cpp | 6 +++---
 libsolutil/CDCL.cpp      | 2 ++
 libsolutil/CDCL.h        | 2 ++
 tools/solsmt.cpp         | 2 ++
 4 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index dea26412e..457a4309f 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -306,7 +306,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
 			else
 			{
 				cerr << _expr.toString() << endl;
-				cerr << "Expected linear arguments." << endl;
+				cerr << "; Expected linear arguments." << endl;
 				solAssert(false);
 			}
 		}
@@ -372,7 +372,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
 	}
 	else
 	{
-		cerr << "Unknown operator " << _expr.name << endl;
+		cerr << "; Unknown operator " << _expr.name << endl;
 		solAssert(false);
 	}
 }
@@ -558,7 +558,7 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
 Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr)
 {
 	if (_expr.sort->kind != Kind::Bool)
-		cerr << "expected bool: " << _expr.toString() << endl;
+		cerr << "; expected bool: " << _expr.toString() << endl;
 	solAssert(_expr.sort->kind == Kind::Bool);
 	// TODO when can this fail?
 	if (optional<Literal> literal = parseLiteral(_expr))
diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index 8e60dab2b..0548c1d89 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -84,10 +84,12 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
 		if (conflictClause)
 		{
 			conflicts++;
+#ifdef DEBUG
 			m_sumConflicts++;
 			if (m_sumConflicts % 1000 == 999) {
 				cerr << "c confl: " << m_sumConflicts << std::endl;
 			}
+#endif
 			if (currentDecisionLevel() == 0)
 			{
 //				cout << "Unsatisfiable" << endl;
diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h
index 39e45f5f0..6cecd1dce 100644
--- a/libsolutil/CDCL.h
+++ b/libsolutil/CDCL.h
@@ -124,7 +124,9 @@ private:
 	std::map<size_t, size_t> m_levelForVariable;
 	/// TODO wolud be good to not have to copy the clauses
 	std::map<Literal, Clause const*> m_reason;
+#ifdef DEBUG
 	uint64_t m_sumConflicts = 0;
+#endif
 
 	// Var activity
 	Heap<VarOrderLt> order;
diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp
index 6ee08df8a..35353eac8 100644
--- a/tools/solsmt.cpp
+++ b/tools/solsmt.cpp
@@ -266,7 +266,9 @@ void SolSMT::run()
 		}
 		else if (cmd == "define-fun")
 		{
+#ifdef DEBUG
 			cerr << "Ignoring 'define-fun'" << endl;
+#endif
 		}
 		else if (cmd == "assert")
 		{