From 479bb9c3de078369bb9100a76a1c8495ed188d3c Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Sat, 15 Jul 2023 14:56:18 +0200 Subject: [PATCH] Fix missing std --- libsmtutil/CHCSmtLib2Interface.cpp | 2 +- libsmtutil/SMTLib2Interface.cpp | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index b3b23a7f9..3f0d3f881 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -197,7 +197,7 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input) { if (m_enabledSolvers.z3 and boost::starts_with(result.responseOrErrorMessage, "unsat")) { solverBinary += " fp.xform.slice=false fp.xform.inline_linear=false fp.xform.inline_eager=false"; - string extendedQuery = "(set-option :produce-proofs true)" + _input + "\n(get-proof)"; + std::string extendedQuery = "(set-option :produce-proofs true)" + _input + "\n(get-proof)"; auto secondResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, extendedQuery); if (secondResult.success) return secondResult.responseOrErrorMessage; diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index e4264557d..5746dbe4e 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -39,7 +39,7 @@ using namespace solidity::frontend; using namespace solidity::smtutil; SMTLib2Interface::SMTLib2Interface( - [[maybe_unused]] std::map _queryResponses, + [[maybe_unused]] std::map _queryResponses, ReadCallback::Callback _smtCallback, SMTSolverChoice _enabledSolvers, std::optional _queryTimeout @@ -136,23 +136,23 @@ namespace { // Helpers for querying solvers using SMT callback std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end) { - std::vector values; + std::vector values; while (_start < _end) { - auto valStart = find(_start, _end, ' '); + auto valStart = std::find(_start, _end, ' '); if (valStart < _end) ++valStart; - auto valEnd = find(valStart, _end, ')'); + auto valEnd = std::find(valStart, _end, ')'); values.emplace_back(valStart, valEnd); - _start = find(valEnd, _end, '('); + _start = std::find(valEnd, _end, '('); } return values; } - std::vector parseValues(string const& solverAnswer) + std::vector parseValues(std::string const& solverAnswer) { - return parseValues(find(solverAnswer.cbegin(), solverAnswer.cend(), '\n'), solverAnswer.cend()); + return parseValues(std::find(solverAnswer.cbegin(), solverAnswer.cend(), '\n'), solverAnswer.cend()); } } @@ -168,7 +168,7 @@ std::pair> SMTLib2Interface::check(std::ve solverCommands.emplace_back("cvc4"); CheckResult lastResult = CheckResult::ERROR; - std::vector finalValues; + std::vector finalValues; smtAssert(m_smtCallback); for (auto const& s: solverCommands) {