3 files changed, 66 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 603e82c3e..810715885 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1172,7 +1172,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
     return stats;
   } else if(key == "error-behavior") {
     // immediate-exit | continued-execution
-    return SExpr::Keyword("immediate-exit");
+    return SExpr::Keyword("continued-execution");
   } else if(key == "name") {
     return Configuration::getName();
   } else if(key == "version") {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 9f00fad6b..1da8d26da 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -239,6 +239,11 @@ class CVC4_PUBLIC SmtEngine {
   std::string d_filename;
 
   /**
+   * Verbosity of various commands.
+   */
+  std::map<std::string, Integer> d_commandVerbosity;
+
+  /**
    * A private utility class to SmtEngine.
    */
   smt::SmtEnginePrivate* d_private;
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index 638cf2f83..228c18adb 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -44,11 +44,29 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
     Dump("benchmark") << SetOptionCommand(key, value);
   }
 
+  if(key == "command-verbosity") {
+    if(!value.isAtom()) {
+      const vector<SExpr>& cs = value.getChildren();
+      if(cs.size() == 2 &&
+         (cs[0].isKeyword() || cs[0].isString()) &&
+         cs[1].isInteger()) {
+        string c = cs[0].getValue();
+        const Integer& v = cs[1].getIntegerValue();
+        if(v < 0 || v > 2) {
+          throw OptionException("command-verbosity must be 0, 1, or 2");
+        }
+        d_commandVerbosity[c] = v;
+        return;
+      }
+    }
+    throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
+  }
+
   string optionarg = value.getValue();
 
   ${smt_setoption_handlers}
 
-#line 52 "${template}"
+#line 70 "${template}"
 
   throw UnrecognizedOptionException(key);
 }
@@ -63,9 +81,49 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
     Dump("benchmark") << GetOptionCommand(key);
   }
 
+  if(key == "command-verbosity") {
+    vector<SExpr> result;
+    SExpr defaultVerbosity;
+    for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
+        i != d_commandVerbosity.end();
+        ++i) {
+      vector<SExpr> v;
+      v.push_back((*i).first);
+      v.push_back((*i).second);
+      if((*i).first == "*") {
+        // put the default at the end of the SExpr
+        defaultVerbosity = v;
+      } else {
+        result.push_back(v);
+      }
+    }
+    // put the default at the end of the SExpr
+    if(!defaultVerbosity.isAtom()) {
+      result.push_back(defaultVerbosity);
+    } else {
+      // ensure the default is always listed
+      vector<SExpr> v;
+      v.push_back("*");
+      v.push_back(Integer(2));
+      result.push_back(v);
+    }
+    return result;
+  } else if(key.length() >= 18 &&
+            key.compare(0, 18, "command-verbosity:") == 0) {
+    map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18);
+    if(i != d_commandVerbosity.end()) {
+      return (*i).second;
+    }
+    i = d_commandVerbosity.find("*");
+    if(i != d_commandVerbosity.end()) {
+      return (*i).second;
+    }
+    return Integer(2);
+  }
+
   ${smt_getoption_handlers}
 
-#line 69 "${template}"
+#line 127 "${template}"
 
   throw UnrecognizedOptionException(key);
 }