Skip to content

Commit

Permalink
Adjust BMC cex generation for models that cannot be parsed
Browse files Browse the repository at this point in the history
  • Loading branch information
Leo Alt committed Jul 15, 2021
1 parent cfe085e commit 3225180
Showing 1 changed file with 13 additions and 9 deletions.
22 changes: 13 additions & 9 deletions libsolidity/formal/BMC.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -932,16 +932,20 @@ void BMC::checkCondition(
solAssert(!_callStack.empty(), "");
std::ostringstream message;
message << "BMC: " << _description << " happens here.";

std::ostringstream modelMessage;
modelMessage << "Counterexample:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);

for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
// Sometimes models have complex smtlib2 expressions that SMTLib2Interface fails to parse.
if (values.size() == expressionNames.size())
{
modelMessage << "Counterexample:\n";
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);

for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
}

m_errorReporter.warning(
_errorHappens,
Expand Down

0 comments on commit 3225180

Please sign in to comment.