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

[SMTChecker] Fix ICE in CHC internal calls

Browse Source
This commit is contained in:
Leonardo Alt
2020-04-07 01:09:03 +02:00
parent 398c515982
commit e3ec22124e
4 changed files with 50 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/CHC.cpp
+5 -1
View File
@@ -961,7 +961,11 @@ smt::Expression CHC::predicate(FunctionCall const& _funCall)
for (auto const& var: function->returnParameters())
args.push_back(m_context.variable(*var)->currentValue());
return (*m_summaries.at(contract).at(function))(args);
if (contract->isLibrary())
return (*m_summaries.at(contract).at(function))(args);
solAssert(m_currentContract, "");
return (*m_summaries.at(m_currentContract).at(function))(args);
}
void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)