From bd9b95170b21ad066e87a59db78fac8ab7f24629 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 14 Sep 2013 19:41:53 -0400
Subject: [PATCH] Fix (extraneous) command dumping.

---
 src/smt/smt_options_template.cpp | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index 228c18adb..4edd91a8d 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -77,6 +77,20 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
   NodeManagerScope nms(d_nodeManager);
 
   Trace("smt") << "SMT getOption(" << key << ")" << endl;
+
+  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);
+  }
+
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetOptionCommand(key);
   }
@@ -108,22 +122,11 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
       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 127 "${template}"
+#line 130 "${template}"
 
   throw UnrecognizedOptionException(key);
 }
-- 
2.30.2