Reasoning is always valid.

This commit is contained in:
chriseth 2022-03-21 10:50:01 +01:00
parent c34019f136
commit 9ec7cf88ec

View File

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