From a7a6475f6fc1ca2eff0f0ed325a8dfab5d7bfbc5 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 21 Mar 2022 18:04:01 +0100
Subject: [PATCH] Fixing remaining issues

---
 libsolutil/CDCL.cpp      |  4 +++-
 tools/satsolver-main.cpp | 16 ++++++++--------
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index a4021b7a1..9084c5494 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -309,7 +309,9 @@ void CDCL::cancelUntil(size_t _backtrackLevel)
 		m_reason.erase(l);
 		// TODO maybe could do without.
 		m_levelForVariable.erase(l.variable);
-		order.insert((int)l.variable);
+		if (!order.inHeap((int)l.variable)) {
+			order.insert((int)l.variable);
+		}
 	}
 	m_decisionPoints.resize(_backtrackLevel);
 	m_assignmentQueuePointer = m_assignmentTrail.size();
diff --git a/tools/satsolver-main.cpp b/tools/satsolver-main.cpp
index 8e09b0eec..ad7c98de9 100644
--- a/tools/satsolver-main.cpp
+++ b/tools/satsolver-main.cpp
@@ -98,6 +98,8 @@ std::pair<vector<vector<Literal>>, size_t> readCNFFile(const string& fname)
 	{
 		if (line.empty())
 			continue;
+		if (line[0] == 'c')
+			continue;
 		if (line[0] == 'p') {
 			assert(line.substr(0,6) == string("p cnf "));
 			line = line.substr(6);
@@ -166,18 +168,16 @@ int main(int argc, char** argv)
 
 	if (model) {
 		const size_t line_break_after = 80;
+		size_t last_line_break = 0;
 		stringstream ss;
 		ss << "v";
-		for (size_t i = 0; i < model->size(); i++) {
-			if (ss.str().size() > line_break_after) {
-				cout << ss.str() << endl;
-				ss.clear();
+		for(auto const& m: *model) {
+			if (ss.str().size()-last_line_break > line_break_after) {
+				ss << endl;
+				last_line_break = ss.str().size();
 				ss << "v";
 			}
-// 			if (model->at(i) != TriState::t_unset()) {
-// 				ss << " " << (model->at(i) == TriState::t_true() ? "" : "-") << i+1;
-// 			}
-
+			ss << " " << (m.second ? "" : "-") << m.first;
 		}
 		cout << ss.str() << " 0" << endl;
 		cout << "s SATISFIABLE" << endl;