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 #14377 from ethereum/fix-smtlib

Browse Source 
SMTChecker: Fix generation of smtlib scripts
This commit is contained in:
Leo 2023-06-30 16:58:26 +02:00 committed by GitHub
commit 2f451a186b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/BMC.cpp
View File

@ -81,13 +81,13 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
SMTEncoder::resetSourceAnalysis(); SMTEncoder::resetSourceAnalysis();
state().prepareForSourceUnit(_source, false);
m_solvedTargets = std::move(_solvedTargets); m_solvedTargets = std::move(_solvedTargets);
m_context.setSolver(m_interface.get()); m_context.setSolver(m_interface.get());
m_context.reset(); m_context.reset();
m_context.setAssertionAccumulation(true); m_context.setAssertionAccumulation(true);
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall); m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
createFreeConstants(sourceDependencies(_source)); createFreeConstants(sourceDependencies(_source));
state().prepareForSourceUnit(_source, false);
m_unprovedAmt = 0; m_unprovedAmt = 0;
_source.accept(*this); _source.accept(*this);