From 9ec7cf88ec0ba50085b2e64deb22c1f1d7dac3d9 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Mon, 21 Mar 2022 10:50:01 +0100
Subject: [PATCH] Reasoning is always valid.

---
 libyul/optimiser/ReasoningBasedSimplifier.cpp | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index cfe367c67..2bedd8733 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -50,11 +50,7 @@ void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast)
 
 std::optional<string> ReasoningBasedSimplifier::invalidInCurrentEnvironment()
 {
-	// SMTLib2 interface is always available, but we would like to have synchronous answers.
-	if (smtutil::SMTPortfolio{}.solvers() <= 1)
-		return string{"No SMT solvers available."};
-	else
-		return nullopt;
+	return nullopt;
 }
 
 void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl)