From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 29 May 2013 17:02:52 +0000 (-0400)
Subject: Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.
X-Git-Tag: cvc5-1.0.0~7287^2~33^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6dc2c46fced4d8121d6d7bdd739d977f32d0462;p=cvc5.git

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

diff --git a/NEWS b/NEWS
index eb991f74c..0532716a9 100644
--- 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 36336a959..423bf3234 100644
--- 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());
   }