From e6dc2c46fced4d8121d6d7bdd739d977f32d0462 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 29 May 2013 13:02:52 -0400
Subject: [PATCH] Per SMT-LIB spec, allow (set-info..) command to succeed
 implicitly with unknown key.

---
 NEWS                 | 2 +-
 src/expr/command.cpp | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

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());
   }
-- 
2.30.2