diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index 888949e36..be1412441 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -168,7 +168,8 @@ 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) { auto callBackResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ' ' + s, query); @@ -181,7 +182,8 @@ std::pair> SMTLib2Interface::check(std::ve if (!solverAnswered(lastResult)) { lastResult = result; - finalValues = parseValues(response); + if (result == CheckResult::SATISFIABLE) + finalValues = parseValues(response); } else if (lastResult != result) {