diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index db1abd6f1..bf7cb9638 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -241,6 +241,11 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, LetBindings _letBind
 	solAssert(_expr.sort->kind == Kind::Bool);
 	if (_expr.arguments.empty())
 	{
+		if (_expr.name == "true")
+			return;
+		else if (_expr.name == "false")
+			solAssert(false, "Adding false as top-level assertion.");
+
 		size_t varIndex = 0;
 		if (_letBindings->count(_expr.name))
 		{
@@ -430,8 +435,16 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
 		}
 		else if (_expr.name == "true" || _expr.name == "false")
 		{
-			// TODO handle this better
-			solAssert(false, "True/false literals not implemented");
+			// TODO handle this better, we can introduce some shortcuts if we propagate this up.
+			// Also we should maybe not create a new variable each time.
+
+			if (!state().trueConstant)
+			{
+				Expression var = declareInternalVariable(true);
+				addAssertion(var, make_shared<map<string, LetBinding>>());
+				state().trueConstant = parseLiteral(var, make_shared<map<string, LetBinding>>())->variable;
+			}
+			return Literal{_expr.name == "true", *state().trueConstant};
 		}
 		else
 			varIndex = state().variables.at(_expr.name);
diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h
index 0b6163bd2..11bbe6cbd 100644
--- a/libsolutil/BooleanLP.h
+++ b/libsolutil/BooleanLP.h
@@ -39,6 +39,8 @@ struct State
 	// Potential constraints, referenced through clauses
 	std::map<size_t, Constraint> conditionalConstraints;
 	std::vector<Clause> clauses;
+	/// The variable index of a bool variable that is always true.
+	std::optional<size_t> trueConstant;
 
 	struct Bounds
 	{