From ea5acaba821790dd240db779f2340fbe5fce0b8e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 7 Aug 2012 14:53:06 +0000 Subject: [PATCH] Fix SmtEngine::setInfo() handling for certain keys. This fixes the "unsupported" message we see in QF_SAT nightly regressions. --- src/smt/smt_engine.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index de5971306..c11354657 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -613,7 +613,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { - if(key == ":status") { + if(key == "status") { std::string s = value.getValue(); BenchmarkStatus status = (s == "sat") ? SMT_SATISFIABLE : @@ -625,10 +625,10 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") - if(key.length() > 6) { - string prefix = key.substr(0, 6); - if(prefix == ":cvc4-" || prefix == ":cvc4_") { - string cvc4key = key.substr(6); + if(key.length() > 5) { + string prefix = key.substr(0, 5); + if(prefix == "cvc4-" || prefix == "cvc4_") { + string cvc4key = key.substr(5); if(cvc4key == "logic") { if(! value.isAtom()) { throw OptionException("argument to (set-info :cvc4-logic ..) must be a string"); -- 2.30.2