support (set-info) on status, source, category, difficulty, smt-lib-version, and notes; reduces extraneous "unsupported" output

1 files changed, 7 insertions, 2 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5bf5ebd69..fc2c8550e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -162,10 +162,15 @@ SmtEngine::~SmtEngine() {
 
 void SmtEngine::setInfo(const string& key, const SExpr& value)
   throw(BadOptionException) {
-  if(key == ":status") {
+  if(key == ":status" ||
+     key == ":source" ||
+     key == ":category" ||
+     key == ":difficulty" ||
+     key == ":smt-lib-version" ||
+     key == ":notes") {
+    // ignore these
     return;
   }
-  // FIXME implement me
   throw BadOptionException();
 }