From e2b86d605ddde8acb278d541f055fe09961fd151 Mon Sep 17 00:00:00 2001
From: Bhargava Shastry <bhargava.shastry@ethereum.org>
Date: Wed, 16 Feb 2022 14:13:00 +0100
Subject: [PATCH] Add fuzzer test.

---
 test/libsolutil/LP.cpp | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/test/libsolutil/LP.cpp b/test/libsolutil/LP.cpp
index b766e9bc7..867a8beea 100644
--- a/test/libsolutil/LP.cpp
+++ b/test/libsolutil/LP.cpp
@@ -51,6 +51,11 @@ public:
 		return LinearExpression::factorForVariable(variableIndex(_name), 1);
 	}
 
+	LinearExpression variable(string const& _name, rational _value)
+	{
+		return LinearExpression::factorForVariable(variableIndex(_name), _value);
+	}
+
 	/// Adds the constraint "_lhs <= _rhs".
 	void addLEConstraint(LinearExpression _lhs, LinearExpression _rhs, set<size_t> _reason = {})
 	{
@@ -110,6 +115,14 @@ public:
 		BOOST_CHECK_MESSAGE(suppliedReason == _reason, "Reasons are different");
 	}
 
+	void sat()
+	{
+		auto [result, model] = m_solver.check(m_solvingState);
+		for (auto const& [var, value]: model)
+			cout << var << " = " << value << endl;
+		BOOST_REQUIRE(result == LPResult::Feasible);
+	}
+
 protected:
 	size_t variableIndex(string const& _name)
 	{
@@ -131,6 +144,15 @@ protected:
 
 BOOST_FIXTURE_TEST_SUITE(LP, LPTestFramework, *boost::unit_test::label("nooptions"))
 
+BOOST_AUTO_TEST_CASE(fuzzer)
+{
+	auto x = variable("x", -6);
+	auto y = variable("y", -6);
+	// expected result: -6x -6y = 8 is unsat since x >= 0 and y >= 0 are implied
+	addEQConstraint(x + y, constant(8));
+	sat();
+}
+
 BOOST_AUTO_TEST_CASE(basic)
 {
 	auto x = variable("x");