From 36dd801660bad8fe1d967c887363f15dbe1bcc63 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 09:27:55 -0400
Subject: [PATCH] A couple of fixes to the get-option command for compliance
 with SMT-LIB.

Thanks to David Cok for reporting this issue.
---
 src/expr/command.cpp  |  6 ++----
 src/options/mkoptions | 31 +++++++++++++++++++++++++++++--
 2 files changed, 31 insertions(+), 6 deletions(-)

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 3a88a6cba..593f84ced 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1228,11 +1228,9 @@ std::string GetOptionCommand::getFlag() const throw() {
 
 void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    vector<SExpr> v;
-    v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
-    v.push_back(smtEngine->getOption(d_flag));
+    SExpr res = smtEngine->getOption(d_flag);
     stringstream ss;
-    ss << SExpr(v);
+    ss << res;
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
   } catch(UnrecognizedOptionException&) {
diff --git a/src/options/mkoptions b/src/options/mkoptions
index fa6c4c260..2e152ee07 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -666,13 +666,40 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 
   if [ -n "$smtname" ]; then
     if [ "$internal" != - ]; then
-      smt_getoption_handlers="${smt_getoption_handlers}
+      case "$type" in
+      bool) smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    return SExprKeyword(options::$internal() ? \"true\" : \"false\");
+  }";;
+      int|unsigned|int*_t|uint*_t|CVC4::Integer) smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    return SExpr(Integer(options::$internal()));
+  }";;
+      float|double) smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    stringstream ss; ss << std::fixed << options::$internal();
+    return SExpr(Rational::fromDecimal(ss.str()));
+  }";;
+      CVC4::Rational) smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    return SExpr(options::$internal());
+  }";;
+      *) smt_getoption_handlers="${smt_getoption_handlers}
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
     stringstream ss; ss << options::$internal();
     return SExpr(ss.str());
-  }"
+  }";;
+      esac
     fi
 
     if [ "$type" = bool ]; then
-- 
2.30.2