From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 14 Sep 2013 23:41:53 +0000 (-0400)
Subject: Fix (extraneous) command dumping.
X-Git-Tag: cvc5-1.0.0~7287^2~12
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd9b95170b21ad066e87a59db78fac8ab7f24629;p=cvc5.git

Fix (extraneous) command dumping.
---

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