From c93f0434cd2dc8542d9adf9dc7d9256fd54d65de Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Fri, 11 Aug 2017 18:54:56 +0200
Subject: Use experimental feature pragma for SMT checker.

---
 libsolidity/ast/ExperimentalFeatures.h | 3 +++
 libsolidity/formal/SMTChecker.cpp      | 7 +------
 2 files changed, 4 insertions(+), 6 deletions(-)

(limited to 'libsolidity')

diff --git a/libsolidity/ast/ExperimentalFeatures.h b/libsolidity/ast/ExperimentalFeatures.h
index 0c03ea4a..2c089671 100644
--- a/libsolidity/ast/ExperimentalFeatures.h
+++ b/libsolidity/ast/ExperimentalFeatures.h
@@ -29,6 +29,7 @@ namespace solidity
 
 enum class ExperimentalFeature
 {
+	SMTChecker,
 	ABIEncoderV2, // new ABI encoder that makes use of JULIA
 	Test,
 	TestOnlyAnalysis
@@ -36,11 +37,13 @@ enum class ExperimentalFeature
 
 static const std::map<ExperimentalFeature, bool> ExperimentalFeatureOnlyAnalysis =
 {
+	{ ExperimentalFeature::SMTChecker, true },
 	{ ExperimentalFeature::TestOnlyAnalysis, true },
 };
 
 static const std::map<std::string, ExperimentalFeature> ExperimentalFeatureNames =
 {
+	{ "SMTChecker", ExperimentalFeature::SMTChecker },
 	{ "ABIEncoderV2", ExperimentalFeature::ABIEncoderV2 },
 	{ "__test", ExperimentalFeature::Test },
 	{ "__testOnlyAnalysis", ExperimentalFeature::TestOnlyAnalysis },
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();
-- 
cgit