From e655f53813d7f44c823c9796ffb875c4c061da65 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Mon, 30 May 2022 11:08:16 +0200
Subject: [PATCH] Fix toString.

---
 libsolutil/BooleanLP.cpp | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index f7c84f29d..853abb8b5 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -172,6 +172,9 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 			Clause conflictClause;
 			for (size_t constraintIndex: reasonSet)
 				conflictClause.emplace_back(Literal{false, constraintIndex});
+#ifdef DEBUG
+		cerr << "||||| conflict claus: " << toString(conflictClause) << endl;
+#endif
 			return conflictClause;
 		}
 		else
@@ -755,14 +758,17 @@ string BooleanLPSolver::toString(Clause const& _clause) const
 {
 	vector<string> literals;
 	for (Literal const& l: _clause)
+	{
+		string lit = l.positive ? "" : "!";
 		if (isBooleanVariable(l.variable))
-			literals.emplace_back((l.positive ? "" : "!") + variableName(l.variable));
+			lit += variableName(l.variable);
 		else
 		{
 			solAssert(isConditionalConstraint(l.variable));
-			solAssert(l.positive);
-			literals.emplace_back(toString(conditionalConstraint(l.variable)));
+			lit += toString(conditionalConstraint(l.variable));
 		}
+		literals.emplace_back(move(lit));
+	}
 	return joinHumanReadable(literals, "  \\/  ") + "\n";
 }