cerc-io/solidity
10
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

Fix SMTLib2Interface

Browse Source
This commit is contained in:
Martin Blicha 2023-06-26 16:38:59 +02:00
parent f4b849972c
commit c6f274892e
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsmtutil/SMTLib2Interface.cpp
View File

@ -118,11 +118,11 @@ namespace { // Helpers for querying solvers using SMT callback
auto resultFromSolverResponse (std::string const& response) { auto resultFromSolverResponse (std::string const& response) {
CheckResult result; CheckResult result;
// TODO proper parsing // TODO proper parsing
if (boost::starts_with(response, "sat\n")) if (boost::starts_with(response, "sat"))
result = CheckResult::SATISFIABLE; result = CheckResult::SATISFIABLE;
else if (boost::starts_with(response, "unsat\n")) else if (boost::starts_with(response, "unsat"))
result = CheckResult::UNSATISFIABLE; result = CheckResult::UNSATISFIABLE;
else if (boost::starts_with(response, "unknown\n")) else if (boost::starts_with(response, "unknown"))
result = CheckResult::UNKNOWN; result = CheckResult::UNKNOWN;
else else
result = CheckResult::ERROR; result = CheckResult::ERROR;

2
libsmtutil/SMTLib2Interface.h
View File

@ -44,7 +44,7 @@ public:
explicit SMTLib2Interface( explicit SMTLib2Interface(
std::map<util::h256, std::string> _queryResponses = {}, std::map<util::h256, std::string> _queryResponses = {},
frontend::ReadCallback::Callback _smtCallback = {}, frontend::ReadCallback::Callback _smtCallback = {},
SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(), SMTSolverChoice _enabledSolvers = SMTSolverChoice::None(),
std::optional<unsigned> _queryTimeout = {} std::optional<unsigned> _queryTimeout = {}
); );