diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-14 19:41:53 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-16 18:54:33 -0400 |
commit | bd9b95170b21ad066e87a59db78fac8ab7f24629 (patch) | |
tree | aad3fae7d7bbbadb88e808d70b6809f9a0fe8413 /src/smt/smt_options_template.cpp | |
parent | 5aa5b7588230a4e61abb3a7bda132120618a3efa (diff) |
Fix (extraneous) command dumping.
Diffstat (limited to 'src/smt/smt_options_template.cpp')
-rw-r--r-- | src/smt/smt_options_template.cpp | 27 |
1 files 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); } |