From 6e4205e445261525bdc814dbc2bfea94057fb895 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 17 Sep 2020 13:43:18 +0200 Subject: [PATCH] Do not run reasoning test if no SMT Solver is available. --- test/libyul/YulOptimizerTest.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/test/libyul/YulOptimizerTest.cpp b/test/libyul/YulOptimizerTest.cpp index cdcfd4fc2..fc5177fe4 100644 --- a/test/libyul/YulOptimizerTest.cpp +++ b/test/libyul/YulOptimizerTest.cpp @@ -103,7 +103,10 @@ YulOptimizerTest::YulOptimizerTest(string const& _filename): BOOST_THROW_EXCEPTION(runtime_error("Filename path has to contain a directory: \"" + _filename + "\".")); m_optimizerStep = std::prev(std::prev(path.end()))->string(); - if (m_optimizerStep == "reasoningBasedSimplifier" && solidity::test::CommonOptions::get().disableSMT) + if (m_optimizerStep == "reasoningBasedSimplifier" && ( + solidity::test::CommonOptions::get().disableSMT || + ReasoningBasedSimplifier::invalidInCurrentEnvironment() + )) m_shouldRun = false; m_source = m_reader.source();