diff --git a/test/tools/ossfuzz/CDCLSolverCustomMutatorInterface.cpp b/test/tools/ossfuzz/CDCLSolverCustomMutatorInterface.cpp
new file mode 100644
index 000000000..376cf4fe9
--- /dev/null
+++ b/test/tools/ossfuzz/CDCLSolverCustomMutatorInterface.cpp
@@ -0,0 +1,68 @@
+/*
+	This file is part of solidity.
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <test/tools/ossfuzz/CDCLSolverCustomMutatorInterface.h>
+#include <test/tools/ossfuzz/cdclsolver/ConstraintGenerator.h>
+
+#include <liblangutil/Exceptions.h>
+
+using namespace std;
+using namespace solidity::test::fuzzer::cdclsolver;
+
+// Prototype as we can't use the FuzzerInterface.h header.
+extern "C" size_t LLVMFuzzerMutate(uint8_t* _data, size_t _size, size_t _maxSize);
+extern "C" size_t LLVMFuzzerCustomMutator(uint8_t* _data, size_t size, size_t _maxSize, unsigned int seed);
+
+namespace
+{
+/// Define LP Solver's custom mutator by implementing libFuzzer's
+/// custom mutator external interface.
+extern "C" size_t LLVMFuzzerCustomMutator(
+	uint8_t* _data,
+	size_t _size,
+	size_t _maxSize,
+	unsigned int _seed
+)
+{
+	solAssert(_data, "libFuzzerInterface: libFuzzer supplied bad buffer");
+	if (_maxSize <= _size || _size == 0)
+		return LLVMFuzzerMutate(_data, _size, _maxSize);
+	return CDCLSolverCustomMutatorInterface{_data, _size, _maxSize, _seed}.generate();
+}
+}
+
+CDCLSolverCustomMutatorInterface::CDCLSolverCustomMutatorInterface(
+	uint8_t* _data,
+	size_t _size,
+	size_t _maxSize,
+	unsigned int _seed
+):
+	data(_data),
+	size(_size),
+	maxMutantSize(_maxSize),
+	generator(make_shared<ConstraintGenerator>(_seed))
+{}
+
+size_t CDCLSolverCustomMutatorInterface::generate()
+{
+	string testCase = generator->generate();
+	solAssert(
+		!testCase.empty() && data,
+		"LP constraints custom mutator: Invalid mutant or memory pointer"
+	);
+	size_t mutantSize = min(testCase.size(), maxMutantSize - 1);
+	mempcpy(data, testCase.data(), mutantSize);
+	return mutantSize;
+}
diff --git a/test/tools/ossfuzz/CDCLSolverCustomMutatorInterface.h b/test/tools/ossfuzz/CDCLSolverCustomMutatorInterface.h
new file mode 100644
index 000000000..95e3c9500
--- /dev/null
+++ b/test/tools/ossfuzz/CDCLSolverCustomMutatorInterface.h
@@ -0,0 +1,43 @@
+/*
+	This file is part of solidity.
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+/**
+ * Implements libFuzzer's custom mutator interface for CDCL Solver fuzzer.
+ */
+
+#pragma once
+
+#include <test/tools/ossfuzz/cdclsolver/ConstraintGenerator.h>
+
+#include <memory>
+
+namespace solidity::test::fuzzer::cdclsolver
+{
+struct CDCLSolverCustomMutatorInterface
+{
+	CDCLSolverCustomMutatorInterface(uint8_t* _data, size_t _size, size_t _maxSize, unsigned _seed);
+	/// Generates LP Solver constraints, copies it into buffer
+	/// provided by libFuzzer and @returns size of the test program.
+	size_t generate();
+
+	/// Raw pointer to libFuzzer provided input
+	uint8_t* data;
+	/// Size of libFuzzer provided input
+	size_t size;
+	/// Maximum length of mutant specified by libFuzzer
+	size_t maxMutantSize;
+	/// Constraint generator handle
+	std::shared_ptr<ConstraintGenerator> generator;
+};
+}
diff --git a/test/tools/ossfuzz/CDCLSolverFuzzer.cpp b/test/tools/ossfuzz/CDCLSolverFuzzer.cpp
new file mode 100644
index 000000000..8b1b9871e
--- /dev/null
+++ b/test/tools/ossfuzz/CDCLSolverFuzzer.cpp
@@ -0,0 +1,123 @@
+/*
+	This file is part of solidity.
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <test/tools/ossfuzz/cdclsolver/FuzzerSolverInterface.h>
+
+#include <algorithm>
+#include <cstddef>
+#include <iostream>
+#include <optional>
+#include <sstream>
+#include <stdint.h>
+#include <string>
+#include <vector>
+
+using namespace solidity::test::fuzzer::cdclsolver;
+using namespace std;
+
+using Constraint = pair<bool, vector<int>>;
+using Constraints = vector<Constraint>;
+
+// Prototype as we can't use the FuzzerInterface.h header.
+extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size);
+
+namespace
+{
+#ifdef DEBUG
+void printConstraints(Constraints _constraints)
+{
+	for (auto& i: _constraints)
+	{
+		cout << (i.first ? "=" : "<=");
+		for (auto& j: i.second)
+			cout << "," << j;
+		cout << endl;
+	}
+}
+#endif
+
+bool validInput(string const& _input)
+{
+	return all_of(
+		_input.begin(),
+		_input.end(),
+		[](unsigned char _c) { return isdigit(_c) || (_c == ',') || (_c == '-') || (_c == '\n'); }
+	);
+}
+
+optional<Constraints> parseConstraints(istringstream& _input)
+{
+	Constraints constraints;
+	for (string line; getline(_input, line); )
+	{
+		istringstream lineStream;
+		lineStream.str(line);
+		Constraint constraint;
+		bool first = true;
+		for (string field; getline(lineStream, field, ','); )
+		{
+			int val = 0;
+			try
+			{
+				val = stoi(field);
+			}
+			// Fuzzer can sometimes supply invalid input to stoi that needs to be
+			// rejected.
+			catch (invalid_argument const&)
+			{
+				return nullopt;
+			}
+			if (first)
+			{
+				constraint.first = static_cast<bool>(val);
+				first = false;
+			}
+			else
+				constraint.second.emplace_back(val);
+		}
+		constraints.emplace_back(constraint);
+	}
+	// Zero input constraints is an invalid input
+	if (constraints.size() < 1)
+		return nullopt;
+	// Incomplete constraints are invalid
+	for (auto c: constraints)
+		if (c.second.empty())
+			return nullopt;
+	return constraints;
+}
+}
+
+extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size)
+{
+	istringstream input;
+	input.str(string(reinterpret_cast<char const*>(_data), _size));
+	if (validInput(input.str()))
+	{
+		// Parse CSV input
+		auto constraints = parseConstraints(input);
+		if (constraints.has_value())
+		{
+			FuzzerSolverInterface solverWithModels(/*supportModels=*/true);
+			if (!solverWithModels.differentialCheck(constraints.value()))
+			{
+				cout << solverWithModels.m_lpResult << endl;
+				cout << solverWithModels.m_z3Result << endl;
+				solAssert(false, "LP result did not match with z3 result.");
+			}
+		}
+	}
+	return 0;
+}
diff --git a/test/tools/ossfuzz/CMakeLists.txt b/test/tools/ossfuzz/CMakeLists.txt
index 265533397..c4c87ec20 100644
--- a/test/tools/ossfuzz/CMakeLists.txt
+++ b/test/tools/ossfuzz/CMakeLists.txt
@@ -9,6 +9,7 @@ add_dependencies(ossfuzz
 )
 
 if (OSSFUZZ)
+    add_subdirectory(cdclsolver)
     add_custom_target(ossfuzz_proto)
     add_dependencies(ossfuzz_proto
             sol_proto_ossfuzz
@@ -23,6 +24,13 @@ if (OSSFUZZ)
 endif()
 
 if (OSSFUZZ)
+    add_executable(cdclsolver_ossfuzz
+      CDCLSolverFuzzer.cpp
+      CDCLSolverCustomMutatorInterface.cpp
+    )
+    target_link_libraries(cdclsolver_ossfuzz PRIVATE solutil cdclsolvergen z3)
+    set_target_properties(cdclsolver_ossfuzz PROPERTIES LINK_FLAGS ${LIB_FUZZING_ENGINE})
+
     add_executable(solc_ossfuzz
             solc_ossfuzz.cpp
             ../fuzzer_common.cpp
diff --git a/test/tools/ossfuzz/cdclsolver/CMakeLists.txt b/test/tools/ossfuzz/cdclsolver/CMakeLists.txt
new file mode 100644
index 000000000..ac474a22e
--- /dev/null
+++ b/test/tools/ossfuzz/cdclsolver/CMakeLists.txt
@@ -0,0 +1,9 @@
+set(sources
+		ConstraintGenerator.cpp
+		ConstraintGenerator.h
+		FuzzerSolverInterface.cpp
+		FuzzerSolverInterface.h
+)
+add_library(cdclsolvergen)
+target_sources(cdclsolvergen PUBLIC	${sources})
+target_link_libraries(cdclsolvergen PUBLIC solutil)
diff --git a/test/tools/ossfuzz/cdclsolver/ConstraintGenerator.cpp b/test/tools/ossfuzz/cdclsolver/ConstraintGenerator.cpp
new file mode 100644
index 000000000..20980b957
--- /dev/null
+++ b/test/tools/ossfuzz/cdclsolver/ConstraintGenerator.cpp
@@ -0,0 +1,42 @@
+/*
+	This file is part of solidity.
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <test/tools/ossfuzz/cdclsolver/ConstraintGenerator.h>
+
+using namespace std;
+using namespace solidity::test::fuzzer::cdclsolver;
+
+ConstraintGenerator::ConstraintGenerator(unsigned int _seed)
+{
+	prng = make_shared<RandomEngine>(_seed);
+}
+
+string ConstraintGenerator::generate()
+{
+	string constraint;
+	for (int i = 0; i < numConstraints(); i++)
+	{
+		// First entry is always constraint type. If it is equal to "1", it is an equality constraint
+		// otherwise an less-than-equal constraint.
+		constraint += to_string(zeroOrOne());
+		for (int j = 0; j < numFactors(); j++)
+			if (bernoulliDist(s_piecewiseConstantProb))
+				constraint += ",0";
+			else
+				constraint += "," + to_string(randomInteger());
+		constraint += "\n";
+	}
+	return constraint;
+}
diff --git a/test/tools/ossfuzz/cdclsolver/ConstraintGenerator.h b/test/tools/ossfuzz/cdclsolver/ConstraintGenerator.h
new file mode 100644
index 000000000..bc8c260ed
--- /dev/null
+++ b/test/tools/ossfuzz/cdclsolver/ConstraintGenerator.h
@@ -0,0 +1,95 @@
+/*
+	This file is part of solidity.
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+/*
+ * Generates constraints for the CDCL solver.
+ */
+
+#pragma once
+
+#include <limits>
+#include <memory>
+#include <random>
+#include <string>
+
+namespace solidity::test::fuzzer::cdclsolver
+{
+
+using RandomEngine = std::mt19937;
+using Distribution = std::uniform_int_distribution<int>;
+using Bernoulli = std::bernoulli_distribution;
+
+struct ConstraintGenerator
+{
+	explicit ConstraintGenerator(unsigned int _seed);
+
+	/// @returns generated constraint.
+	std::string generate();
+
+	/// @returns random number of factors.
+	int numFactors()
+	{
+		return Distribution(s_minNumFactors, s_maxNumFactors)(*prng);
+	}
+
+	/// @returns random number of constraints.
+	int numConstraints()
+	{
+		return Distribution(s_minConstraints, s_maxConstraints)(*prng);
+	}
+
+	/// @returns an integer chosen uniformly at random.
+	int randomInteger()
+	{
+		return Distribution(s_minFactor, s_maxFactor)(*prng);
+	}
+
+	/// @returns an integer in the range [-1, 1] chosen uniformly at random.
+	int randomMinusOneToOne()
+	{
+		return Distribution(-1, 1)(*prng);
+	}
+
+	/// @returns zero or one with a probability of occurance of 0.5 each.
+	int zeroOrOne()
+	{
+		return Distribution(0, 1)(*prng);
+	}
+
+	/// @returns true with a probability @param _p, false otherwise.
+	bool bernoulliDist(double _truthProbability)
+	{
+		return Bernoulli(_truthProbability)(*prng);
+	}
+
+
+	std::shared_ptr<RandomEngine> prng;
+
+	/// Smallest number of factors in linear constraint of the form
+	/// a*x1 + b*x2 <= c
+	static constexpr int s_minNumFactors = 2;
+	/// Largest number of factors in linear constraint
+	static constexpr int s_maxNumFactors = 100;
+	/// Smallest number of linear constraints
+	static constexpr int s_minConstraints = 1;
+	/// Largest number of linear constraints
+	static constexpr int s_maxConstraints = 100;
+	/// Smallest value of a factor in linear constraint
+	static constexpr int s_minFactor = -100;
+	/// Largest value of a factor in linear constraint
+	static constexpr int s_maxFactor = 100;
+	/// Probability that a factor in the range of [-1, 1] is chosen
+	static constexpr double s_piecewiseConstantProb = 0.75;
+};
+}
diff --git a/test/tools/ossfuzz/cdclsolver/FuzzerSolverInterface.cpp b/test/tools/ossfuzz/cdclsolver/FuzzerSolverInterface.cpp
new file mode 100644
index 000000000..44baf127b
--- /dev/null
+++ b/test/tools/ossfuzz/cdclsolver/FuzzerSolverInterface.cpp
@@ -0,0 +1,165 @@
+/*
+	This file is part of solidity.
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <test/tools/ossfuzz/cdclsolver/FuzzerSolverInterface.h>
+
+#include <range/v3/view/enumerate.hpp>
+
+#include <set>
+
+using namespace solidity::test::fuzzer::cdclsolver;
+using namespace solidity::util;
+using namespace std;
+using namespace z3;
+
+FuzzerSolverInterface::FuzzerSolverInterface(bool _supportModels):
+	m_lpSolver(_supportModels),
+	m_z3Solver(m_z3Ctx)
+{
+	m_lpSolvingState.variableNames.emplace_back("");
+	params z3Params(m_z3Ctx);
+	z3Params.set(":timeout", static_cast<unsigned>(10)); // in milliseconds
+	m_z3Solver.set(z3Params);
+}
+
+LinearExpression FuzzerSolverInterface::linearExpression(vector<int> _factors)
+{
+	LinearExpression lexp;
+	lexp.resize(_factors.size());
+	for (auto&& [index, value]: _factors | ranges::views::enumerate)
+		lexp[index] = rational{value};
+	return lexp;
+}
+
+void FuzzerSolverInterface::addLPConstraint(pair<bool, vector<int>> _constraint)
+{
+	m_lpSolvingState.constraints.push_back(
+		{linearExpression(move(_constraint.second)), _constraint.first, {}}
+	);
+}
+
+void FuzzerSolverInterface::addLPVariable(string _varName)
+{
+	if (
+		find(
+			m_lpSolvingState.variableNames.begin(),
+			m_lpSolvingState.variableNames.end(),
+			_varName
+		) == m_lpSolvingState.variableNames.end()
+	)
+		m_lpSolvingState.variableNames.emplace_back(_varName);
+}
+
+void FuzzerSolverInterface::addZ3Constraint(pair<bool, vector<int>> _constraint)
+{
+	bool isEquality = _constraint.first;
+	expr reduce = m_z3Ctx.real_val(0);
+	for (auto&& [index, value]: _constraint.second | ranges::views::enumerate)
+	{
+		if (index != 0 && value != 0)
+		{
+			string varName = "x" + to_string(index - 1);
+			// Add variable name to LP solving state to aid debugging
+			addLPVariable(varName);
+			expr var = m_z3Ctx.real_const(varName.c_str());
+			expr factor = m_z3Ctx.int_val(value);
+			reduce = reduce + var * factor;
+			m_z3Solver.add(var >= 0);
+		}
+	}
+	if (isEquality)
+		m_z3Solver.add(reduce == _constraint.second[0]);
+	else
+		m_z3Solver.add(reduce <= _constraint.second[0]);
+}
+
+void FuzzerSolverInterface::addLPConstraints(vector<pair<bool, vector<int>>> _constraints)
+{
+	for (auto c: _constraints)
+		addLPConstraint(c);
+}
+
+void FuzzerSolverInterface::addZ3Constraints(vector<pair<bool, vector<int>>> _constraints)
+{
+	for (auto c: _constraints)
+		addZ3Constraint(c);
+}
+
+Solution FuzzerSolverInterface::checkLP()
+{
+	return m_lpSolver.check(m_lpSolvingState);
+}
+
+check_result FuzzerSolverInterface::checkZ3()
+{
+	return m_z3Solver.check();
+}
+
+string FuzzerSolverInterface::checkLPResult()
+{
+	m_lpResult = lpResult(checkLP().first);
+	return m_lpResult;
+}
+
+string FuzzerSolverInterface::checkZ3Result()
+{
+	m_z3Result = z3Result(checkZ3());
+	return m_z3Result;
+}
+
+bool FuzzerSolverInterface::differentialCheck(vector<pair<bool, vector<int>>> _constraints)
+{
+	addZ3Constraints(_constraints);
+	string z3Result = checkZ3Result();
+	// There is no point in continuing if z3 (the quicker solver) returns
+	// unknown.
+	if (z3Result == "unknown")
+		return true;
+	addLPConstraints(_constraints);
+	string lpResult = checkLPResult();
+	bool checkFailed = ((z3Result == "infeasible") && (lpResult == "feasible")) ||
+		((z3Result == "feasible") && (lpResult == "infeasible"));
+	return !checkFailed;
+}
+
+string FuzzerSolverInterface::lpResult(LPResult _result)
+{
+	switch (_result)
+	{
+	case LPResult::Unknown:
+		return "unknown";
+	case LPResult::Unbounded:
+		return "unbounded";
+	case LPResult::Feasible:
+		return "feasible";
+	case LPResult::Infeasible:
+		return "infeasible";
+	}
+}
+
+string FuzzerSolverInterface::z3Result(check_result _result)
+{
+	switch (_result)
+	{
+	case check_result::unsat:
+		return "infeasible";
+	case check_result::sat:
+		return "feasible";
+	case check_result::unknown:
+		return "unknown";
+	default:
+		solAssert(false, "Invalid Z3 result");
+	}
+}
diff --git a/test/tools/ossfuzz/cdclsolver/FuzzerSolverInterface.h b/test/tools/ossfuzz/cdclsolver/FuzzerSolverInterface.h
new file mode 100644
index 000000000..5b26c8095
--- /dev/null
+++ b/test/tools/ossfuzz/cdclsolver/FuzzerSolverInterface.h
@@ -0,0 +1,88 @@
+/*
+	This file is part of solidity.
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+/**
+ * Implements the Fuzzer-Solver interface.
+ */
+
+#pragma once
+
+#include <libsolutil/LP.h>
+#include <libsolutil/LinearExpression.h>
+
+#include <z3++.h>
+
+#include <string>
+
+namespace solidity::test::fuzzer::cdclsolver
+{
+
+using Model = std::map<std::string, solidity::util::rational>;
+using ReasonSet = std::set<size_t>;
+using Solution = std::pair<solidity::util::LPResult, std::variant<Model, ReasonSet>>;
+
+class FuzzerSolverInterface
+{
+public:
+	FuzzerSolverInterface(bool _supportModels);
+
+	/// Adds @param _constraint to LP solver.
+	void addLPConstraint(std::pair<bool, std::vector<int>> _constraint);
+
+	/// Adds @param _constraint to Z3 solver.
+	void addZ3Constraint(std::pair<bool, std::vector<int>> _constraint);
+
+	/// Adds @param _constraints to LP solver.
+	void addLPConstraints(std::vector<std::pair<bool, std::vector<int>>> _constraints);
+
+	/// Adds @param _constraints to Z3 solver.
+	void addZ3Constraints(std::vector<std::pair<bool, std::vector<int>>> _constraints);
+
+	/// @returns linear expression created from @param _factors.
+	solidity::util::LinearExpression linearExpression(std::vector<int> _factors);
+
+	/// Queries LP solver and @returns solution.
+	Solution checkLP();
+
+	/// Queries Z3 solver and @returns solution.
+	z3::check_result checkZ3();
+
+	/// Queries LP solver and @returns sat result as string.
+	std::string checkLPResult();
+
+	/// Queries Z3 solver and @returns sat result as string.
+	std::string checkZ3Result();
+
+	/// @returns true if both the LP and the Z3 solver return an identical result on
+	/// @param _constraints, false otherwise.
+	bool differentialCheck(std::vector<std::pair<bool, std::vector<int>>> _constraints);
+private:
+	/// @returns LP result as string.
+	std::string lpResult(solidity::util::LPResult _result);
+
+	/// @returns Z3 result as string.
+	std::string z3Result(z3::check_result _result);
+
+	/// Adds variable name to LP solver solving state.
+	void addLPVariable(std::string _varName);
+
+	solidity::util::LPSolver m_lpSolver;
+	solidity::util::SolvingState m_lpSolvingState;
+	z3::context m_z3Ctx;
+	z3::solver m_z3Solver;
+public:
+	std::string m_lpResult;
+	std::string m_z3Result;
+};
+}