diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index 0548c1d89..14fe67961 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -38,7 +38,7 @@ CDCL::CDCL(
 	m_theorySolver(_theorySolver),
 	m_backtrackNotify(_backtrackNotify),
 	m_variables(move(_variables)),
-	order(VarOrderLt(activity))
+	m_order(VarOrderLt(m_activity))
 {
 	for (Clause const& clause: _clauses)
 		addClause(clause);
@@ -278,17 +278,17 @@ std::pair<Clause, size_t> CDCL::analyze(Clause _conflictClause)
 
 void CDCL::addClause(Clause _clause)
 {
-	uint64_t max_var = (uint32_t)activity.size();
+	uint64_t max_var = (uint32_t)m_activity.size();
 	uint64_t new_max_var = 0;
 	for(auto const& l: _clause) {
 		new_max_var = std::max<uint64_t>(l.variable+1, max_var);
 	}
 	int64_t to_add = (int64_t)new_max_var - (int64_t)max_var;
 	if (to_add > 0) {
-		activity.insert(activity.end(), (uint64_t)to_add, 0.0);
+		m_activity.insert(m_activity.end(), (uint64_t)to_add, 0.0);
 	}
 	for(auto const& l: _clause) {
-		if (!order.inHeap((int)l.variable)) order.insert((int)l.variable);
+		if (!m_order.inHeap((int)l.variable)) m_order.insert((int)l.variable);
 	}
 
 	m_clauses.push_back(make_unique<Clause>(move(_clause)));
@@ -331,8 +331,8 @@ void CDCL::cancelUntil(size_t _backtrackLevel)
 		m_reason.erase(l);
 		// TODO maybe could do without.
 		m_levelForVariable.erase(l.variable);
-		if (!order.inHeap((int)l.variable)) {
-			order.insert((int)l.variable);
+		if (!m_order.inHeap((int)l.variable)) {
+			m_order.insert((int)l.variable);
 		}
 	}
 	m_decisionPoints.resize(_backtrackLevel);
@@ -344,8 +344,8 @@ void CDCL::cancelUntil(size_t _backtrackLevel)
 optional<size_t> CDCL::nextDecisionVariable()
 {
 	while(true) {
-		if (order.empty()) return nullopt;
-		size_t i = (size_t)order.removeMin();
+		if (m_order.empty()) return nullopt;
+		size_t i = (size_t)m_order.removeMin();
 		if (!m_assignments.count(i)) return i;
 	}
 	return nullopt;
diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h
index 6cecd1dce..04d970a1f 100644
--- a/libsolutil/CDCL.h
+++ b/libsolutil/CDCL.h
@@ -129,30 +129,30 @@ private:
 #endif
 
 	// Var activity
-	Heap<VarOrderLt> order;
-	std::vector<double> activity;
-	double var_inc_vsids = 1;
-	double var_decay = 0.95;
+	Heap<VarOrderLt> m_order;
+	std::vector<double> m_activity;
+	double m_var_inc_vsids = 1;
+	double m_var_decay = 0.95;
 	void vsids_decay_var_act()
 	{
-		var_inc_vsids *= (1.0 / var_decay);
+		m_var_inc_vsids *= (1.0 / m_var_decay);
 	}
-	void vsids_bump_var_act(uint32_t var)
+	void vsids_bump_var_act(const uint32_t var)
 	{
-		assert(activity.size() > var);
-		activity[var] += var_inc_vsids;
+		assert(m_activity.size() > var);
+		m_activity[var] += m_var_inc_vsids;
 
 		bool rescaled = false;
-		if (activity[var] > 1e100) {
+		if (m_activity[var] > 1e100) {
 			// Rescale
-			for (auto& a: activity) a *= 1e-100;
+			for (auto& a: m_activity) a *= 1e-100;
 			rescaled = true;
-			var_inc_vsids *= 1e-100;
+			m_var_inc_vsids *= 1e-100;
 		}
 
 		// Update order_heap with respect to new activity:
-		if (order.inHeap((int)var)) order.decrease((int)var);
-		if (rescaled) assert(order.heap_property());
+		if (m_order.inHeap((int)var)) m_order.decrease((int)var);
+		if (rescaled) assert(m_order.heap_property());
 	}
 
 	// TODO group those into a class