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

Try to parse values only for satisfiable answer

Browse Source
This commit is contained in:
Martin Blicha 2023-06-26 13:23:57 +02:00
parent efb0d4253c
commit da2f4cb100
1 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsmtutil/SMTLib2Interface.cpp
View File

@ -168,7 +168,8 @@ std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::ve
solverCommands.emplace_back("cvc4");
CheckResult lastResult = CheckResult::ERROR;
std::vector<std::string> finalValues;
std::vector<string> finalValues;
smtAssert(m_smtCallback);
for (auto const& s: solverCommands)
{
auto callBackResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ' ' + s, query);
@ -181,7 +182,8 @@ std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::ve
if (!solverAnswered(lastResult))
{
lastResult = result;
finalValues = parseValues(response);
if (result == CheckResult::SATISFIABLE)
finalValues = parseValues(response);
}
else if (lastResult != result)
{