5 files changed, 36 insertions, 25 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b29647311..435597bc7 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6219,8 +6219,7 @@ std::string Solver::getOption(const std::string& option) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  Node res = d_smtEngine->getOption(option);
-  return res.toString();
+  return d_smtEngine->getOption(option);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5f85445ff..55bf68b9f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1926,7 +1926,7 @@ void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
 
 bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
 
-Node SmtEngine::getOption(const std::string& key) const
+std::string SmtEngine::getOption(const std::string& key) const
 {
   NodeManagerScope nms(getNodeManager());
   NodeManager* nm = d_env->getNodeManager();
@@ -1939,14 +1939,14 @@ Node SmtEngine::getOption(const std::string& key) const
         d_commandVerbosity.find(key.c_str() + 18);
     if (i != d_commandVerbosity.end())
     {
-      return nm->mkConst(Rational(i->second));
+      return i->second.toString();
     }
     i = d_commandVerbosity.find("*");
     if (i != d_commandVerbosity.end())
     {
-      return nm->mkConst(Rational(i->second));
+      return i->second.toString();
     }
-    return nm->mkConst(Rational(2));
+    return "2";
   }
 
   if (Dump.isOn("benchmark"))
@@ -1984,30 +1984,24 @@ Node SmtEngine::getOption(const std::string& key) const
                                     nm->mkConst(Rational(2)));
     }
     result.push_back(defaultVerbosity);
-    return nm->mkNode(Kind::SEXPR, result);
+    return nm->mkNode(Kind::SEXPR, result).toString();
   }
 
-  // parse atom string
   std::string atom = getOptions().getOption(key);
 
-  if (atom == "true")
+  if (atom != "true" && atom != "false")
   {
-    return nm->mkConst<bool>(true);
-  }
-  else if (atom == "false")
-  {
-    return nm->mkConst<bool>(false);
-  }
-  try
-  {
-    Integer z(atom);
-    return nm->mkConst(Rational(z));
-  }
-  catch (std::invalid_argument&)
-  {
-    // Fall through to the next case
+    try
+    {
+      Integer z(atom);
+    }
+    catch (std::invalid_argument&)
+    {
+      atom = "\"" + atom + "\"";
+    }
   }
-  return nm->mkConst(String(atom));
+
+  return atom;
 }
 
 Options& SmtEngine::getOptions() { return d_env->d_options; }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 63ba5f831..51eed32b2 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -317,7 +317,7 @@ class CVC4_EXPORT SmtEngine
    * Get an aspect of the current SMT execution environment.
    * @throw OptionException
    */
-  Node getOption(const std::string& key) const;
+  std::string getOption(const std::string& key) const;
 
   /**
    * Define function func in the current context to be:
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c40174eda..e84281a0d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -710,6 +710,7 @@ set(regress_0_tests
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/opt-abd-no-use.smt2
+  regress0/options/ast-and-sexpr.smt2
   regress0/options/invalid_dump.smt2
   regress0/options/set-and-get-options.smt2
   regress0/parallel-let.smt2
diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2
new file mode 100644
index 000000000..2a464571c
--- /dev/null
+++ b/test/regress/regress0/options/ast-and-sexpr.smt2
@@ -0,0 +1,17 @@
+; EXPECT: (SEXPR (SEXPR check-sat (CONST_RATIONAL 2)) (SEXPR * (CONST_RATIONAL 1)))
+; EXPECT: (:status unknown)
+
+; This regression tests uses of s-expressions when the output-language is AST
+
+(set-option :output-language ast)
+
+; Set the verbosity of all commands to 1
+(set-option :command-verbosity (* 1))
+; Set the verbosity of (check-sat) command to 2
+(set-option :command-verbosity (check-sat 2))
+; Get the verbosity of all commands
+(get-option :command-verbosity)
+; There is no SMT option to get the verbosity of a specific command
+
+(set-info :source (0 1 True False x ""))
+(get-info :status)