diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp
index bd74cf2c9..8c3900745 100644
--- a/libsmtutil/SMTLib2Interface.cpp
+++ b/libsmtutil/SMTLib2Interface.cpp
@@ -219,6 +219,8 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	{
 	case Kind::Int:
 		return "Int";
+	case Kind::Real:
+		return "Real";
 	case Kind::Bool:
 		return "Bool";
 	case Kind::BitVector:
@@ -278,8 +280,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
 		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
 		{
 			auto const& e = _expressionsToEvaluate.at(i);
-			smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
-			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n";
+			smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool || e.sort->kind == Kind::Real, "Invalid sort for expression to evaluate.");
+			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + toSmtLibSort(*e.sort) + ")\n";
 			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
 		}
 		command += "(check-sat)\n";
diff --git a/libsmtutil/Sorts.cpp b/libsmtutil/Sorts.cpp
index 543c7ba0f..4077f86ea 100644
--- a/libsmtutil/Sorts.cpp
+++ b/libsmtutil/Sorts.cpp
@@ -25,6 +25,7 @@ namespace solidity::smtutil
 {
 
 shared_ptr<Sort> const SortProvider::boolSort{make_shared<Sort>(Kind::Bool)};
+shared_ptr<Sort> const SortProvider::realSort{make_shared<Sort>(Kind::Real)};
 shared_ptr<IntSort> const SortProvider::uintSort{make_shared<IntSort>(false)};
 shared_ptr<IntSort> const SortProvider::sintSort{make_shared<IntSort>(true)};
 
diff --git a/libsmtutil/Sorts.h b/libsmtutil/Sorts.h
index 107dc1f2c..fd794dad3 100644
--- a/libsmtutil/Sorts.h
+++ b/libsmtutil/Sorts.h
@@ -31,6 +31,7 @@ namespace solidity::smtutil
 enum class Kind
 {
 	Int,
+	Real,
 	Bool,
 	BitVector,
 	Function,
@@ -206,6 +207,7 @@ struct SortProvider
 	static std::shared_ptr<IntSort> const sintSort;
 	static std::shared_ptr<IntSort> intSort(bool _signed = false);
 	static std::shared_ptr<BitVectorSort> const bitVectorSort;
+	static std::shared_ptr<Sort> const realSort;
 };
 
 }
diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index b1f805cb2..dad12da7f 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -92,10 +92,9 @@ void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _s
 {
 	// Internal variables are '$<number>', or '$c<number>' so escape `$` to `$$`.
 	string name = (_name.empty() || _name.at(0) != '$') ? _name : "$$" + _name;
-	// TODO This will not be an integer variable in our model.
-	// Introduce a new kind?
-	solAssert(_sort && (_sort->kind == Kind::Int || _sort->kind == Kind::Bool), "");
+	solAssert(_sort && (_sort->kind == Kind::Int || _sort->kind == Kind::Real || _sort->kind == Kind::Bool), "");
 	solAssert(!state().variables.count(name), "");
+	// TODO store the actual kind (integer, real, bool)
 	declareVariable(name, _sort->kind == Kind::Bool);
 }
 
@@ -206,10 +205,10 @@ string BooleanLPSolver::toString() const
 		if (!bounds.lower && !bounds.upper)
 			continue;
 		if (bounds.lower)
-			result += ::toString(*bounds.lower) + " <= ";
+			result += bounds.lower->toString() + " <= ";
 		result += variableName(index);
 		if (bounds.upper)
-			result += " <= " + ::toString(*bounds.upper);
+			result += " <= " + bounds.upper->toString();
 		result += "\n";
 	}
 	result += "-- Clauses:\n";
@@ -251,7 +250,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
 				addBooleanEquality(newBoolean, _expr.arguments.at(1), _letBindings);
 			}
 		}
-		else if (_expr.arguments.at(0).sort->kind == Kind::Int)
+		else if (_expr.arguments.at(0).sort->kind == Kind::Int || _expr.arguments.at(0).sort->kind == Kind::Real)
 		{
 			// Try to see if both sides are linear.
 			optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings);
@@ -260,7 +259,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
 			{
 				LinearExpression data = *left - *right;
 				data[0] *= -1;
-				Constraint c{move(data), _expr.name == "="};
+				Constraint c{move(data), Constraint::EQUAL};
 				if (!tryAddDirectBounds(c))
 					state().fixedConstraints.emplace_back(move(c));
 				cerr << "Added as fixed constraint" << endl;
@@ -293,24 +292,20 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
 	}
 	else if (_expr.name == "=>")
 		addAssertion(!_expr.arguments.at(0) || _expr.arguments.at(1), move(_letBindings));
-	else if (_expr.name == "<=")
+	else if (_expr.name == "<=" || _expr.name == "<")
 	{
 		optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings);
 		optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1), _letBindings);
 		solAssert(left && right);
 		LinearExpression data = *left - *right;
 		data[0] *= -1;
-		Constraint c{move(data), _expr.name == "="};
+		// TODO if the type is integer, transform x < y into x <= y - 1
+		Constraint c{move(data), _expr.name == "<=" ? Constraint::LESS_OR_EQUAL : Constraint::LESS_THAN};
 		if (!tryAddDirectBounds(c))
 			state().fixedConstraints.emplace_back(move(c));
 	}
 	else if (_expr.name == ">=")
 		addAssertion(_expr.arguments.at(1) <= _expr.arguments.at(0), move(_letBindings));
-	else if (_expr.name == "<")
-	{
-		cerr << "ERROR cannot properly encode '<'" << endl;
-		addAssertion(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1, move(_letBindings));
-	}
 	else if (_expr.name == ">")
 		addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings));
 	else
@@ -325,7 +320,8 @@ Expression BooleanLPSolver::declareInternalVariable(bool _boolean)
 {
 	string name = "$" + to_string(state().variables.size() + 1);
 	declareVariable(name, _boolean);
-	return smtutil::Expression(name, {}, _boolean ? SortProvider::boolSort : SortProvider::uintSort);
+	// TODO also support integer
+	return smtutil::Expression(name, {}, _boolean ? SortProvider::boolSort : SortProvider::realSort);
 }
 
 void BooleanLPSolver::declareVariable(string const& _name, bool _boolean)
@@ -369,27 +365,25 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
 	}
 	else if (_expr.name == "not")
 		return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0), move(_letBindings)));
-	else if (_expr.name == "<=" || _expr.name == "=")
+	else if (_expr.name == "<=" || _expr.name == "<" || _expr.name == "=")
 	{
 		optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings);
 		optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1), _letBindings);
 		if (!left || !right)
 			return {};
 
+		// TODO if the type is int, use x < y -> x <= y - 1
 		LinearExpression data = *left - *right;
 		data[0] *= -1;
 
-		return Literal{true, addConditionalConstraint(Constraint{move(data), _expr.name == "="})};
+		Constraint::Kind kind =
+			_expr.name == "<=" ? Constraint::LESS_OR_EQUAL :
+			_expr.name == "<" ? Constraint::LESS_THAN :
+			Constraint::EQUAL;
+		return Literal{true, addConditionalConstraint(Constraint{move(data), kind})};
 	}
 	else if (_expr.name == ">=")
 		return parseLiteral(_expr.arguments.at(1) <= _expr.arguments.at(0), move(_letBindings));
-	else if (_expr.name == "<")
-	{
-		cerr << "ERROR cannot properly encode '<'" << endl;
-		// TODO this is not the theory of reals!
-
-		return parseLiteral(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1, move(_letBindings));
-	}
 	else if (_expr.name == ">")
 		return parseLiteral(_expr.arguments.at(1) < _expr.arguments.at(0), move(_letBindings));
 
@@ -401,12 +395,12 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
 	if (isConditionalConstraint(_lit.variable))
 	{
 		Constraint const& c = conditionalConstraint(_lit.variable);
-		if (c.equality)
+		if (c.kind == Constraint::EQUAL)
 		{
 			// X = b
 
-			cerr << "ERROR cannot properly encode '<'" << endl;
 
+			/* This is the integer case
 			// X <= b - 1
 			Constraint le = c;
 			le.equality = false;
@@ -421,24 +415,42 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
 			ge.data[0] -= 1;
 			Literal geL{true, addConditionalConstraint(ge)};
 
+			*/
+
+			// X < b
+			Constraint lt = c;
+			lt.kind = Constraint::LESS_THAN;
+			Literal ltL{true, addConditionalConstraint(lt)};
+
+			// X > b <=> -X < -b
+			Constraint gt = c;
+			gt.kind = Constraint::LESS_THAN;
+			gt.data *= -1;
+			Literal gtL{true, addConditionalConstraint(gt)};
 
 			Literal equalBoolean = *parseLiteral(declareInternalVariable(true), {});
 			// a = or(x, y) <=> (-a \/ x \/ y) /\ (a \/ -x) /\ (a \/ -y)
-			state().clauses.emplace_back(Clause{vector<Literal>{negate(equalBoolean), leL, geL}});
-			state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(leL)}});
-			state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(geL)}});
+			state().clauses.emplace_back(Clause{vector<Literal>{negate(equalBoolean), ltL, gtL}});
+			state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(ltL)}});
+			state().clauses.emplace_back(Clause{vector<Literal>{equalBoolean, negate(gtL)}});
 			return equalBoolean;
 		}
 		else
 		{
-			cerr << "ERROR cannot properly encode '<'" << endl;
-			// X > b
+			/* This is the integer case
 			// -x < -b
 			// -x <= -b - 1
 
 			Constraint negated = c;
 			negated.data *= -1;
 			negated.data[0] -= 1;
+			*/
+
+			// !(X <= b) <=> X > b <=> -X < -b
+			// !(X < b) <=> X >= b <=> -X <= -b
+			Constraint negated = c;
+			negated.data *= -1;
+			negated.kind = c.kind == Constraint::LESS_THAN ? Constraint::LESS_OR_EQUAL : Constraint::LESS_THAN;
 			return Literal{true, addConditionalConstraint(negated)};
 		}
 	}
@@ -547,10 +559,11 @@ bool BooleanLPSolver::tryAddDirectBounds(Constraint const& _constraint)
 	//cerr << "adding direct bound." << endl;
 	if (ranges::distance(nonzero) == 0)
 	{
-		// 0 <= b or 0 = b
+		// 0 < b or 0 <= b or 0 = b
 		if (
-			_constraint.data.front() < 0 ||
-			(_constraint.equality && _constraint.data.front() != 0)
+			(_constraint.kind == Constraint::LESS_THAN && _constraint.data.front() <= 0) ||
+			(_constraint.kind == Constraint::LESS_OR_EQUAL && _constraint.data.front() < 0) ||
+			(_constraint.kind == Constraint::EQUAL && _constraint.data.front() != 0)
 		)
 		{
 //			cerr << "SETTING INF" << endl;
@@ -560,27 +573,29 @@ bool BooleanLPSolver::tryAddDirectBounds(Constraint const& _constraint)
 	else
 	{
 		auto&& [varIndex, factor] = nonzero.front();
-		// a * x <= b
-		rational bound = _constraint.data[0] / factor;
-		if (factor > 0 || _constraint.equality)
+		// a * x <= b or a * x < b or a * x = b
+
+		RationalWithDelta bound = _constraint.data[0];
+		if (_constraint.kind == Constraint::LESS_THAN)
+			bound -= RationalWithDelta::delta();
+		bound /= factor;
+		if (factor > 0 || _constraint.kind == Constraint::EQUAL)
 			addUpperBound(varIndex, bound);
-		if (factor < 0 || _constraint.equality)
+		if (factor < 0 || _constraint.kind == Constraint::EQUAL)
 			addLowerBound(varIndex, bound);
 	}
 	return true;
 }
 
-void BooleanLPSolver::addUpperBound(size_t _index, rational _value)
+void BooleanLPSolver::addUpperBound(size_t _index, RationalWithDelta _value)
 {
 	//cerr << "adding " << variableName(_index) << " <= " << toString(_value) << endl;
 	if (!state().bounds[_index].upper || _value < *state().bounds[_index].upper)
 		state().bounds[_index].upper = move(_value);
 }
 
-void BooleanLPSolver::addLowerBound(size_t _index, rational _value)
+void BooleanLPSolver::addLowerBound(size_t _index, RationalWithDelta _value)
 {
-	// Lower bound must be at least zero.
-	_value = max(_value, rational{});
 	//cerr << "adding " << variableName(_index) << " >= " << toString(_value) << endl;
 	if (!state().bounds[_index].lower || _value > *state().bounds[_index].lower)
 		state().bounds[_index].lower = move(_value);
@@ -712,7 +727,11 @@ string BooleanLPSolver::toString(Constraint const& _constraint) const
 	// TODO reasons?
 	return
 		joinHumanReadable(line, " + ") +
-		(_constraint.equality ? "  = " : " <= ") +
+		(
+			_constraint.kind == Constraint::EQUAL ? "  = " :
+			_constraint.kind == Constraint::LESS_OR_EQUAL ? " <= " :
+			" <  "
+		) +
 		::toString(_constraint.data.front());
 }
 
diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h
index d690207bd..186b3bd98 100644
--- a/libsolutil/BooleanLP.h
+++ b/libsolutil/BooleanLP.h
@@ -42,8 +42,8 @@ struct State
 
 	struct Bounds
 	{
-		std::optional<rational> lower;
-		std::optional<rational> upper;
+		std::optional<RationalWithDelta> lower;
+		std::optional<RationalWithDelta> upper;
 	};
 
 	// Unconditional bounds on variables
@@ -115,8 +115,8 @@ private:
 	std::optional<LinearExpression> parseFactor(smtutil::Expression const& _expression, std::map<std::string, size_t> _letBindings) const;
 
 	bool tryAddDirectBounds(Constraint const& _constraint);
-	void addUpperBound(size_t _index, rational _value);
-	void addLowerBound(size_t _index, rational _value);
+	void addUpperBound(size_t _index, RationalWithDelta _value);
+	void addLowerBound(size_t _index, RationalWithDelta _value);
 
 	size_t addConditionalConstraint(Constraint _constraint);
 
diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp
index 26e916b09..4058163d8 100644
--- a/libsolutil/LP.cpp
+++ b/libsolutil/LP.cpp
@@ -86,11 +86,10 @@ string reasonToString(ReasonSet const& _reasons, size_t _minSize)
 
 }
 
-
 bool Constraint::operator<(Constraint const& _other) const
 {
-	if (equality != _other.equality)
-		return equality < _other.equality;
+	if (kind != _other.kind)
+		return kind < _other.kind;
 
 	for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i)
 		if (rational diff = data.get(i) - _other.data.get(i))
@@ -105,7 +104,7 @@ bool Constraint::operator<(Constraint const& _other) const
 
 bool Constraint::operator==(Constraint const& _other) const
 {
-	if (equality != _other.equality)
+	if (kind != _other.kind)
 		return false;
 
 	for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i)
@@ -119,6 +118,17 @@ bool Constraint::operator==(Constraint const& _other) const
 	return true;
 }
 
+string RationalWithDelta::toString() const
+{
+	string result = ::toString(m_main);
+	if (m_delta)
+		result +=
+			(m_delta > 0 ? "+" : "-") +
+			(abs(m_delta) == 1 ? "" : ::toString(abs(m_delta))) +
+			"d";
+	return result;
+}
+
 bool SolvingState::Compare::operator()(SolvingState const& _a, SolvingState const& _b) const
 {
 	if (!considerVariableNames || _a.variableNames == _b.variableNames)
@@ -160,7 +170,11 @@ string SolvingState::toString() const
 			}
 		result +=
 			joinHumanReadable(line, " + ") +
-			(constraint.equality ? "  = " : " <= ") +
+			(
+				constraint.kind == Constraint::EQUAL ? "  = " :
+				constraint.kind == Constraint::LESS_OR_EQUAL ? " <= " :
+				" <  "
+			) +
 			::toString(constraint.data.front()) +
 			"\n";
 	}
@@ -172,10 +186,10 @@ string SolvingState::toString() const
 		if (bounds.lower)
 			result +=
 				reasonToString(bounds.lowerReasons, reasonLength) +
-				::toString(*bounds.lower) + " <= ";
+				bounds.lower->toString() + " <= ";
 		result += variableNames.at(index);
 		if (bounds.upper)
-			result += " <= "s + ::toString(*bounds.upper) + " " + reasonToString(bounds.upperReasons, 0);
+			result += " <= "s + bounds.upper->toString() + " " + reasonToString(bounds.upperReasons, 0);
 		result += "\n";
 	}
 	return result;
@@ -215,7 +229,7 @@ void LPSolver::setVariableName(size_t _variable, string _name)
 	p.variables[p.varMapping.at(_variable)].name = move(_name);
 }
 
-void LPSolver::addLowerBound(size_t _variable, rational _bound)
+void LPSolver::addLowerBound(size_t _variable, RationalWithDelta _bound)
 {
 	SubProblem& p = unsealForVariable(_variable);
 	size_t innerIndex = p.varMapping.at(_variable);
@@ -227,7 +241,7 @@ void LPSolver::addLowerBound(size_t _variable, rational _bound)
 	}
 }
 
-void LPSolver::addUpperBound(size_t _variable, rational _bound)
+void LPSolver::addUpperBound(size_t _variable, RationalWithDelta _bound)
 {
 	SubProblem& p = unsealForVariable(_variable);
 	size_t innerIndex = p.varMapping.at(_variable);
@@ -274,7 +288,10 @@ map<string, rational> LPSolver::model() const
 	for (auto const& problem: m_subProblems)
 		if (problem)
 			for (auto&& [outerIndex, innerIndex]: problem->varMapping)
-				result[problem->variables[innerIndex].name] = problem->variables[innerIndex].value;
+				// TODO assign proper value to "delta"
+				result[problem->variables[innerIndex].name] =
+					problem->variables[innerIndex].value.m_main +
+					problem->variables[innerIndex].value.m_delta / rational(100000);
 	return result;
 }
 
@@ -376,10 +393,13 @@ void LPSolver::addConstraintToSubProblem(
 		// TODO we could avoid some of the steps by introducing an "addUpperBound"
 		// function on the subproblem.
 		rational factor = _constraint.data[latestVariableIndex];
-		rational bound = _constraint.data.front() / factor;
-		if (factor > 0 || _constraint.equality)
+		RationalWithDelta bound = _constraint.data.front();
+		if (_constraint.kind == Constraint::LESS_THAN)
+			bound -= RationalWithDelta::delta();
+		bound /= factor;
+		if (factor > 0 || _constraint.kind == Constraint::EQUAL)
 			addUpperBound(latestVariableIndex, bound);
-		if (factor < 0 || _constraint.equality)
+		if (factor < 0 || _constraint.kind == Constraint::EQUAL)
 			addLowerBound(latestVariableIndex, bound);
 		return;
 	}
@@ -389,15 +409,17 @@ void LPSolver::addConstraintToSubProblem(
 	// Name is only needed for printing
 	//problem.variables[slackIndex].name = "_s" + to_string(m_slackVariableCounter++);
 	problem.basicVariables[slackIndex] = problem.factors.size();
-	if (_constraint.equality)
+	if (_constraint.kind == Constraint::EQUAL)
 		problem.variables[slackIndex].bounds.lower = _constraint.data[0];
 	problem.variables[slackIndex].bounds.upper = _constraint.data[0];
+	if (_constraint.kind == Constraint::LESS_THAN)
+		*problem.variables[slackIndex].bounds.upper -= RationalWithDelta::delta();
 	// TODO it is a basic var, so we don't add it, unless we use this for basic vars.
 	//problem.variablesPotentiallyOutOfBounds.insert(slackIndex);
 
 	// Compress the constraint, i.e. turn outer variable indices into
 	// inner variable indices.
-	rational valueForSlack;
+	RationalWithDelta valueForSlack;
 	LinearExpression compressedConstraint;
 	LinearExpression basicVarNullifier;
 	compressedConstraint.resize(problem.variables.size());
@@ -504,15 +526,15 @@ string LPSolver::SubProblem::toString() const
 	for (auto&& [i, v]: variables | ranges::views::enumerate)
 	{
 		if (v.bounds.lower)
-			resultString += ::toString(*v.bounds.lower) + " <= ";
+			resultString += v.bounds.lower->toString() + " <= ";
 		else
 			resultString += "       ";
 		resultString += v.name;
 		if (v.bounds.upper)
-			resultString += " <= " + ::toString(*v.bounds.upper);
+			resultString += " <= " + v.bounds.upper->toString();
 		else
 			resultString += "       ";
-		resultString += "   := " + ::toString(v.value) + "\n";
+		resultString += "   := " + v.value.toString() + "\n";
 	}
 	for (auto&& [rowIndex, row]: factors | ranges::views::enumerate)
 	{
@@ -574,9 +596,9 @@ bool LPSolver::SubProblem::correctNonbasic()
 	return true;
 }
 
-void LPSolver::SubProblem::update(size_t _varIndex, rational const& _value)
+void LPSolver::SubProblem::update(size_t _varIndex, RationalWithDelta const& _value)
 {
-	rational delta = _value - variables[_varIndex].value;
+	RationalWithDelta delta = _value - variables[_varIndex].value;
 	variables[_varIndex].value = _value;
 	for (size_t j = 0; j < variables.size(); j++)
 		if (basicVariables.count(j) && factors[basicVariables.at(j)][_varIndex])
@@ -658,18 +680,18 @@ void LPSolver::SubProblem::pivot(size_t _old, size_t _new)
 
 void LPSolver::SubProblem::pivotAndUpdate(
 	size_t _oldBasicVar,
-	rational const& _newValue,
+	RationalWithDelta const& _newValue,
 	size_t _newBasicVar
 )
 {
-	rational theta = (_newValue - variables[_oldBasicVar].value) / factors[basicVariables[_oldBasicVar]][_newBasicVar];
+	RationalWithDelta theta = (_newValue - variables[_oldBasicVar].value) / factors[basicVariables[_oldBasicVar]][_newBasicVar];
 
 	variables[_oldBasicVar].value = _newValue;
 	variables[_newBasicVar].value += theta;
 
 	for (auto const& [i, row]: basicVariables)
 		if (i != _oldBasicVar && factors[row][_newBasicVar])
-			variables[i].value += factors[row][_newBasicVar] * theta;
+			variables[i].value += theta * factors[row][_newBasicVar];
 
 	pivot(_oldBasicVar, _newBasicVar);
 }
diff --git a/libsolutil/LP.h b/libsolutil/LP.h
index b497d0048..2c4d4fa4f 100644
--- a/libsolutil/LP.h
+++ b/libsolutil/LP.h
@@ -34,14 +34,16 @@ using ReasonSet = std::set<size_t>;
 
 /**
  * Constraint of the form
- *  - data[1] * x_1 + data[2] * x_2 + ... <= data[0]  (equality == false)
- *  - data[1] * x_1 + data[2] * x_2 + ...  = data[0]  (equality == true)
+ *  - data[1] * x_1 + data[2] * x_2 + ... <= data[0]  (LESS_OR_EQUAL)
+ *  - data[1] * x_1 + data[2] * x_2 + ...  < data[0]  (LESS_THAN)
+ *  - data[1] * x_1 + data[2] * x_2 + ...  = data[0]  (EQUAL)
  * The set and order of variables is implied.
  */
 struct Constraint
 {
 	LinearExpression data;
-	bool equality = false;
+	enum Kind { EQUAL, LESS_THAN, LESS_OR_EQUAL };
+	Kind kind = LESS_OR_EQUAL;
 
 	bool operator<(Constraint const& _other) const;
 	bool operator==(Constraint const& _other) const;
@@ -52,10 +54,9 @@ struct Constraint
  * x > 0 is transformed into x >= 1*delta, where delta is assumed to be "small". Its value
  * is never explicitly computed / set, it is just a symbolic parameter.
  */
-class RationalWithDelta
+struct RationalWithDelta
 {
-public:
-	RationalWithDelta(rational _x): m_main(move(_x)) {}
+	RationalWithDelta(rational _x = {}): m_main(move(_x)) {}
 	static RationalWithDelta delta()
 	{
 		RationalWithDelta x(0);
@@ -69,30 +70,69 @@ public:
 		m_delta += _other.m_delta;
 		return *this;
 	}
+	RationalWithDelta& operator-=(RationalWithDelta const& _other)
+	{
+		m_main -= _other.m_main;
+		m_delta -= _other.m_delta;
+		return *this;
+	}
+	RationalWithDelta operator-(RationalWithDelta const& _other) const
+	{
+		RationalWithDelta ret = *this;
+		ret -= _other;
+		return ret;
+	}
 	RationalWithDelta& operator*=(rational const& _factor)
 	{
 		m_main *= _factor;
 		m_delta *= _factor;
 		return *this;
 	}
-	bool operator<=(RationalWithDelta const& _other)
+	RationalWithDelta operator*(rational const& _factor) const
+	{
+		RationalWithDelta ret = *this;
+		ret *= _factor;
+		return ret;
+	}
+	RationalWithDelta& operator/=(rational const& _factor)
+	{
+		m_main /= _factor;
+		m_delta /= _factor;
+		return *this;
+	}
+	RationalWithDelta operator/(rational const& _factor) const
+	{
+		RationalWithDelta ret = *this;
+		ret /= _factor;
+		return ret;
+	}
+	bool operator<=(RationalWithDelta const& _other) const
 	{
 		return std::tie(m_main, m_delta) <= std::tie(_other.m_main, _other.m_delta);
 	}
-	bool operator<(RationalWithDelta const& _other)
+	bool operator>=(RationalWithDelta const& _other) const
+	{
+		return std::tie(m_main, m_delta) >= std::tie(_other.m_main, _other.m_delta);
+	}
+	bool operator<(RationalWithDelta const& _other) const
 	{
 		return std::tie(m_main, m_delta) < std::tie(_other.m_main, _other.m_delta);
 	}
-	bool operator==(RationalWithDelta const& _other)
+	bool operator>(RationalWithDelta const& _other) const
+	{
+		return std::tie(m_main, m_delta) > std::tie(_other.m_main, _other.m_delta);
+	}
+	bool operator==(RationalWithDelta const& _other) const
 	{
 		return std::tie(m_main, m_delta) == std::tie(_other.m_main, _other.m_delta);
 	}
-	bool operator!=(RationalWithDelta const& _other)
+	bool operator!=(RationalWithDelta const& _other) const
 	{
 		return std::tie(m_main, m_delta) != std::tie(_other.m_main, _other.m_delta);
 	}
 
-private:
+	std::string toString() const;
+
 	rational m_main;
 	rational m_delta;
 };
@@ -107,8 +147,8 @@ struct SolvingState
 	std::vector<std::string> variableNames;
 	struct Bounds
 	{
-		std::optional<rational> lower;
-		std::optional<rational> upper;
+		std::optional<RationalWithDelta> lower;
+		std::optional<RationalWithDelta> upper;
 		bool operator<(Bounds const& _other) const { return make_pair(lower, upper) < make_pair(_other.lower, _other.upper); }
 		bool operator==(Bounds const& _other) const { return make_pair(lower, upper) == make_pair(_other.lower, _other.upper); }
 
@@ -158,6 +198,18 @@ inline void hashCombineVector(std::size_t& _seed, std::vector<T> const& _v)
 		hashCombine(_seed, x);
 }
 
+template<>
+struct std::hash<solidity::util::RationalWithDelta>
+{
+	std::size_t operator()(solidity::util::RationalWithDelta const& _x) const noexcept
+	{
+		std::size_t result = 0;
+		hashCombine(result, _x.m_main);
+		hashCombine(result, _x.m_delta);
+		return result;
+	}
+};
+
 template<>
 struct std::hash<solidity::util::SolvingState::Bounds>
 {
@@ -189,7 +241,7 @@ struct std::hash<solidity::util::Constraint>
 	std::size_t operator()(solidity::util::Constraint const& _constraint) const noexcept
 	{
 		std::size_t result = 0;
-		hashCombine(result, _constraint.equality);
+		hashCombine(result, _constraint.kind);
 		hashCombine(result, _constraint.data);
 		return result;
 	}
@@ -243,8 +295,8 @@ class LPSolver
 public:
 	void addConstraint(Constraint const& _constraint, std::optional<size_t> _reason = std::nullopt);
 	void setVariableName(size_t _variable, std::string _name);
-	void addLowerBound(size_t _variable, rational _bound);
-	void addUpperBound(size_t _variable, rational _bound);
+	void addLowerBound(size_t _variable, RationalWithDelta _bound);
+	void addUpperBound(size_t _variable, RationalWithDelta _bound);
 
 	std::pair<LPResult, ReasonSet>check();
 
@@ -254,13 +306,13 @@ public:
 private:
 	struct Bounds
 	{
-		std::optional<rational> lower;
-		std::optional<rational> upper;
+		std::optional<RationalWithDelta> lower;
+		std::optional<RationalWithDelta> upper;
 	};
 	struct Variable
 	{
 		std::string name = {};
-		rational value = 0;
+		RationalWithDelta value = {};
 		Bounds bounds = {};
 	};
 	struct SubProblem
@@ -282,13 +334,13 @@ private:
 	private:
 		bool correctNonbasic();
 		/// Set value of non-basic variable.
-		void update(size_t _varIndex, rational const& _value);
+		void update(size_t _varIndex, RationalWithDelta const& _value);
 		/// @returns the index of the first basic variable violating its bounds.
 		std::optional<size_t> firstConflictingBasicVariable() const;
 		std::optional<size_t> firstReplacementVar(size_t _basicVarToReplace, bool _increasing) const;
 
 		void pivot(size_t _old, size_t _new);
-		void pivotAndUpdate(size_t _oldBasicVar, rational const& _newValue, size_t _newBasicVar);
+		void pivotAndUpdate(size_t _oldBasicVar, RationalWithDelta const& _newValue, size_t _newBasicVar);
 	};
 
 
diff --git a/test/libsolutil/BooleanLP.cpp b/test/libsolutil/BooleanLP.cpp
index 927212ef4..3346eb6b6 100644
--- a/test/libsolutil/BooleanLP.cpp
+++ b/test/libsolutil/BooleanLP.cpp
@@ -196,6 +196,9 @@ BOOST_AUTO_TEST_CASE(splittable)
 	Expression w = variable("w");
 	solver.addAssertion(x < y);
 	solver.addAssertion(x < y - 2);
+	solver.addAssertion(x >= 0);
+	solver.addAssertion(y >= 0);
+	solver.addAssertion(w >= 0);
 	solver.addAssertion(z + w == 28);
 
 	solver.push();
diff --git a/test/libsolutil/LP.cpp b/test/libsolutil/LP.cpp
index efc9956b9..ebc399d29 100644
--- a/test/libsolutil/LP.cpp
+++ b/test/libsolutil/LP.cpp
@@ -55,12 +55,25 @@ public:
 	{
 		_lhs -= _rhs;
 		_lhs[0] = -_lhs[0];
-		m_solver.addConstraint({move(_lhs), false}, move(_reason));
+		m_solver.addConstraint({move(_lhs), Constraint::LESS_OR_EQUAL}, move(_reason));
 	}
 
 	void addLEConstraint(LinearExpression _lhs, rational _rhs)
 	{
-		addLEConstraint(move(_lhs), constant(_rhs));
+		addLEConstraint(move(_lhs), LinearExpression::constant(move(_rhs)));
+	}
+
+	/// Adds the constraint "_lhs < _rhs".
+	void addLTConstraint(LinearExpression _lhs, LinearExpression _rhs, optional<size_t> _reason = {})
+	{
+		_lhs -= _rhs;
+		_lhs[0] = -_lhs[0];
+		m_solver.addConstraint({move(_lhs), Constraint::LESS_THAN}, move(_reason));
+	}
+
+	void addLTConstraint(LinearExpression _lhs, rational _rhs)
+	{
+		addLTConstraint(move(_lhs), LinearExpression::constant(move(_rhs)));
 	}
 
 	/// Adds the constraint "_lhs = _rhs".
@@ -68,7 +81,7 @@ public:
 	{
 		_lhs -= _rhs;
 		_lhs[0] = -_lhs[0];
-		m_solver.addConstraint({move(_lhs), true}, move(_reason));
+		m_solver.addConstraint({move(_lhs), Constraint::EQUAL}, move(_reason));
 	}
 
 	void addLowerBound(string _variable, rational _value)
@@ -425,6 +438,17 @@ BOOST_AUTO_TEST_CASE(reasons_joined)
 	infeasible({0, 2, 3});
 }
 
+BOOST_AUTO_TEST_CASE(less_than)
+{
+	auto x = variable("x");
+	addLTConstraint(2 * x, 10);
+	feasible({{"x", 0}});
+	addLowerBound("x", 4);
+	feasible({{"x", 4}});
+	addLowerBound("x", 5);
+	infeasible();
+}
+
 
 BOOST_AUTO_TEST_CASE(fuzzer2)
 {
diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp
index 158739370..9cb0e8de2 100644
--- a/tools/solsmt.cpp
+++ b/tools/solsmt.cpp
@@ -143,7 +143,7 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<stri
 	return std::visit(GenericVisitor{
 		[&](string_view const& _atom) {
 			if (isDigit(_atom.front()) || _atom.front() == '.')
-				return Expression(parseRational(_atom));
+				return Expression(parseRational(_atom).str(), {}, SortProvider::realSort);
 			else
 				return Expression(string(_atom), {}, _variableSorts.at(string(_atom)));
 		},
@@ -179,7 +179,7 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<stri
 				sort =
 					contains(boolOperators, op) ?
 					SortProvider::boolSort :
-					SortProvider::intSort(); // TODO should be real at some point
+					arguments.back().sort;
 			}
 			return Expression(string(op), move(arguments), move(sort));
 		}
@@ -245,8 +245,7 @@ int main(int argc, char** argv)
 			solAssert(get<vector<SMTLib2Expression>>(items[2].data).empty());
 			string_view type = get<string_view>(items[3].data);
 			solAssert(type == "Real" || type == "Bool");
-			// TODO should be real, but we call it int...
-			SortPointer sort = type == "Real" ? SortProvider::intSort() : SortProvider::boolSort;
+			SortPointer sort = type == "Real" ? SortProvider::realSort : SortProvider::boolSort;
 			variableSorts[variableName] = sort;
 			solver.declareVariable(variableName, move(sort));
 		}