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

[SMTChecker] Fix counterexample state reporting

Browse Source
This commit is contained in:
Leonardo Alt 2020-10-13 22:18:43 +01:00
parent 8675c3ee41
commit 440e5b3935
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolidity/formal/Predicate.cpp
View File

@ -189,7 +189,7 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, this, txData, postBlockchainState, postStateVars).
/// The signature of an implicit constructor summary predicate is: summary(error, this, txData, preBlockSchainState, postBlockchainState, postStateVars).
/// Here we are interested in postStateVars.
auto stateVars = stateVariables();
@ -204,7 +204,7 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
}
else if (programContract())
{
stateFirst = _args.begin() + 4;
stateFirst = _args.begin() + 5;
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else