diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 7b0c97383..11d0da6a9 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -248,7 +248,7 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 	}
 
 	set<size_t> previousConditionalConstraints;
-	auto theorySolver = [&](map<size_t, bool> const& _booleanAssignment) -> optional<Clause>
+	auto theorySolver = [&](size_t /*_decisionLevel*/, map<size_t, bool> const& _booleanAssignment) -> optional<Clause>
 	{
 		SolvingState lpStateToCheck = lpState;
 		set<size_t> conditionalConstraints;
@@ -281,8 +281,9 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 		else
 			return nullopt;
 	};
+	auto backtrackNotify = [](size_t /*_decisionLevel*/) {};
 
-	auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver}.solve();
+	auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver, backtrackNotify}.solve();
 	if (!optionalModel)
 	{
 		cout << "==============> CDCL final result: unsatisfiable." << endl;
diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index 58326a88e..25c730b52 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -32,9 +32,11 @@ using namespace solidity::util;
 CDCL::CDCL(
 	vector<string> _variables,
 	vector<Clause> const& _clauses,
-	std::function<std::optional<Clause>(std::map<size_t, bool> const&)> _theorySolver
+	std::function<std::optional<Clause>(size_t, std::map<size_t, bool> const&)> _theorySolver,
+	std::function<void(size_t)> _backtrackNotify
 ):
 	m_theorySolver(_theorySolver),
+	m_backtrackNotify(_backtrackNotify),
 	m_variables(move(_variables)),
 	order(VarOrderLt(activity))
 {
@@ -69,7 +71,7 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
 		optional<Clause> conflictClause = propagate();
 		if (!conflictClause && m_theorySolver)
 		{
-			conflictClause = m_theorySolver(m_assignments);
+			conflictClause = m_theorySolver(currentDecisionLevel(), m_assignments);
 //			if (conflictClause)
 //				cout << "Theory gave us conflict: " << toString(*conflictClause) << endl;
 		}
@@ -323,6 +325,8 @@ void CDCL::cancelUntil(size_t _backtrackLevel)
 	}
 	m_decisionPoints.resize(_backtrackLevel);
 	m_assignmentQueuePointer = m_assignmentTrail.size();
+	if (m_backtrackNotify)
+		m_backtrackNotify(currentDecisionLevel());
 	solAssert(currentDecisionLevel() == _backtrackLevel);
 }
 
diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h
index 0c1ac1ccf..da8837eb6 100644
--- a/libsolutil/CDCL.h
+++ b/libsolutil/CDCL.h
@@ -59,7 +59,8 @@ public:
 	CDCL(
 		std::vector<std::string> _variables,
 		std::vector<Clause> const& _clauses,
-		std::function<std::optional<Clause>(std::map<size_t, bool> const&)> _theoryPropagator = {}
+		std::function<std::optional<Clause>(size_t, std::map<size_t, bool> const&)> _theorySolver = {},
+		std::function<void(size_t)> _backtrackNotify = {}
 	);
 
 	std::optional<Model> solve();
@@ -102,7 +103,8 @@ private:
 
 	/// Callback that receives an assignment and uses the theory to either returns nullopt ("satisfiable")
 	/// or a conflict clause, i.e. a clauses that is false in the theory with the given assignments.
-	std::function<std::optional<Clause>(std::map<size_t, bool>)> m_theorySolver;
+	std::function<std::optional<Clause>(size_t, std::map<size_t, bool>)> m_theorySolver;
+	std::function<void(size_t)> m_backtrackNotify;
 
 	std::vector<std::string> m_variables;
 	/// includes the learnt clauses