cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #6897 from ethereum/smt_check_pragma_earlier

Browse Source 
[SMTChecker] Exit early if no pragma
This commit is contained in:
Leonardo 2019-06-05 10:26:25 +02:00 committed by GitHub
commit 3a3316393e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libsolidity/formal/SMTChecker.cpp
View File

@ -52,9 +52,12 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _
void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner) void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
{ {
if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
return;
m_scanner = _scanner; m_scanner = _scanner;
if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
_source.accept(*this); _source.accept(*this);
solAssert(m_interface.solvers() > 0, ""); solAssert(m_interface.solvers() > 0, "");
// If this check is true, Z3 and CVC4 are not available // If this check is true, Z3 and CVC4 are not available