From fe15610ba46bdecf2f4437bb1adbe8a50b1c302c Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 3 Mar 2022 19:50:27 +0100
Subject: [PATCH] some more debugging output

---
 libsmtutil/SolverInterface.h                  | 5 ++++-
 libsolutil/BooleanLP.cpp                      | 1 +
 libyul/optimiser/ReasoningBasedSimplifier.cpp | 7 +++++++
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h
index 4eaebf46a..f46ea38d5 100644
--- a/libsmtutil/SolverInterface.h
+++ b/libsmtutil/SolverInterface.h
@@ -497,7 +497,10 @@ public:
 		std::vector<std::string> argsAsString;
 		for (auto const& arg: arguments)
 			argsAsString.emplace_back(arg.toString());
-		return name + "(" + util::joinHumanReadable(argsAsString) + ")";
+		if (arguments.size() == 2)
+			return "(" + argsAsString[0] + " " + name + " " + argsAsString[1] + ")";
+		else
+			return name + "(" + util::joinHumanReadable(argsAsString) + ")";
 	}
 private:
 	/// Manual constructors, should only be used by SolverInterface and this class itself.
diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 6f424b505..346fbdd1d 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -135,6 +135,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
 				Constraint c{move(data), _expr.name == "=", {}};
 				if (!tryAddDirectBounds(c))
 					state().fixedConstraints.emplace_back(move(c));
+				cout << "Added as fixed constraint" << endl;
 			}
 			else
 			{
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index 62e9a1bb2..1fe2e9d30 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -67,25 +67,31 @@ void ReasoningBasedSimplifier::operator()(If& _if)
 	if (!SideEffectsCollector{m_dialect, *_if.condition}.movable())
 		return;
 
+	cout << "Checking if condition  can be false" << endl;
 	smtutil::Expression condition = encodeExpression(*_if.condition);
 	m_solver->push();
 	m_solver->addAssertion(condition == constantValue(0));
+	cout << "  running check" << endl;
 	CheckResult result = m_solver->check({}).first;
 	m_solver->pop();
 	if (result == CheckResult::UNSATISFIABLE)
 	{
+		cout << " unsat => cannot be false!" << endl;
 		Literal trueCondition = m_dialect.trueLiteral();
 		trueCondition.debugData = debugDataOf(*_if.condition);
 		_if.condition = make_unique<yul::Expression>(move(trueCondition));
 	}
 	else
 	{
+		cout << "Checking if condition  can be true" << endl;
 		m_solver->push();
 		m_solver->addAssertion(condition != constantValue(0));
+		cout << "  running check" << endl;
 		CheckResult result2 = m_solver->check({}).first;
 		m_solver->pop();
 		if (result2 == CheckResult::UNSATISFIABLE)
 		{
+			cout << " unsat => cannot be true!" << endl;
 			Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType);
 			falseCondition.debugData = debugDataOf(*_if.condition);
 			_if.condition = make_unique<yul::Expression>(move(falseCondition));
@@ -96,6 +102,7 @@ void ReasoningBasedSimplifier::operator()(If& _if)
 	}
 
 	m_solver->push();
+	cout << "Setting condition true inside body" << endl;
 	m_solver->addAssertion(condition != constantValue(0));
 
 	ASTModifier::operator()(_if.body);