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 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)