aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
-rw-r--r--libsolidity/formal/SMTChecker.cpp7
1 files changed, 1 insertions, 6 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index e1fd2bfd..092ecdb2 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -44,12 +44,7 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
void SMTChecker::analyze(SourceUnit const& _source)
{
- bool pragmaFound = false;
- for (auto const& node: _source.nodes())
- if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get()))
- if (pragma->literals()[0] == "checkAssertions")
- pragmaFound = true;
- if (pragmaFound)
+ if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
{
m_interface->reset();
m_currentSequenceCounter.clear();