Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.

diff --git a/NEWS b/NEWS
index eb991f74ca5aecfa62711077f4a8fc80b1263abb..0532716a9730008de075257a638de03148735d9c 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -6,7 +6,7 @@ Changes since 1.2
 * We no longer permit model or proof generation if there's been an
   intervening push/pop.
 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
-  resolved
+  resolved.
 
 Changes since 1.1
 =================

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 36336a95963479bbf24e6f2e2a4b06e4da141e26..423bf3234f86fc93ca431548acc32783c8c44e13 100644 (file)
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1118,7 +1118,8 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
     smtEngine->setInfo(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
   } catch(UnrecognizedOptionException&) {
-    d_commandStatus = new CommandUnsupported();
+    // As per SMT-LIB spec, silently accept unknown set-info keys
+    d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }