From a13b5332c271b903fe711e700b0040964243361c Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 21 Mar 2022 18:26:25 +0100
Subject: [PATCH] Fixing minor last things

---
 libsolutil/CDCL.cpp      | 8 ++++++--
 libsolutil/CDCL.h        | 1 +
 tools/satsolver-main.cpp | 2 +-
 3 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index 9084c5494..633f3758a 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -76,6 +76,10 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
 		if (conflictClause)
 		{
 			conflicts++;
+			m_sumConflicts++;
+			if (m_sumConflicts % 1000 == 999) {
+				cout << "c confl: " << m_sumConflicts << std::endl;
+			}
 			if (currentDecisionLevel() == 0)
 			{
 //				cout << "Unsatisfiable" << endl;
@@ -96,8 +100,8 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
 		{
 			if (auto variable = nextDecisionVariable())
 			{
-				cout << "Level " << currentDecisionLevel() << " - ";
-				cout << ((m_assignments.size() * 100) / m_variables.size()) << "% of variables assigned." << endl;
+// 				cout << "c Level " << currentDecisionLevel() << " - ";
+// 				cout << ((m_assignments.size() * 100) / m_variables.size()) << "% of variables assigned." << endl;
 				m_decisionPoints.emplace_back(m_assignmentTrail.size());
 //				cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl;
 
diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h
index 289bd51bc..65cae269e 100644
--- a/libsolutil/CDCL.h
+++ b/libsolutil/CDCL.h
@@ -122,6 +122,7 @@ 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;
+	uint64_t m_sumConflicts = 0;
 
 	// Var activity
 	Heap<VarOrderLt> order;
diff --git a/tools/satsolver-main.cpp b/tools/satsolver-main.cpp
index ad7c98de9..b53dab4c1 100644
--- a/tools/satsolver-main.cpp
+++ b/tools/satsolver-main.cpp
@@ -177,7 +177,7 @@ int main(int argc, char** argv)
 				last_line_break = ss.str().size();
 				ss << "v";
 			}
-			ss << " " << (m.second ? "" : "-") << m.first;
+			ss << " " << (m.second ? "" : "-") << m.first+1;
 		}
 		cout << ss.str() << " 0" << endl;
 		cout << "s SATISFIABLE" << endl;