cerc-io/solidity
11
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 #8678 from ethereum/smt_remove_redundant_constraints

Browse Source 
[SMTChecker] Remove redundant CHC constraints
This commit is contained in:
chriseth
2020-04-20 15:44:59 +02:00
committed by GitHub
parent 55483445e9 bca43586c6
commit 41ef13129b
6 changed files with 15 additions and 22 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+3 -1
View File
@@ -107,6 +107,9 @@ void SMTEncoder::endVisit(ContractDefinition const& _contract)
solAssert(m_currentContract == &_contract, "");
m_currentContract = nullptr;
if (m_callStack.empty())
m_context.popSolver();
}
void SMTEncoder::endVisit(VariableDeclaration const& _varDecl)
@@ -662,7 +665,6 @@ void SMTEncoder::initFunction(FunctionDefinition const& _function)
{
solAssert(m_callStack.empty(), "");
solAssert(m_currentContract, "");
m_context.reset();
m_context.pushSolver();
m_pathConditions.clear();
pushCallStack({&_function, nullptr});