4 files changed, 9 insertions, 7 deletions
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 87739789b..4e74eefb5 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -62,8 +62,9 @@ Command* Smt2Input::parseCommand() {
   return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
 }
 
-Expr Smt2Input::parseExpr() {
-  return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
+api::Term Smt2Input::parseExpr()
+{
+  return api::Term(d_pSmt2Parser->parseExpr(d_pSmt2Parser));
 }
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index e8b736a16..9d4ed2857 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -76,7 +76,7 @@ class Smt2Input : public AntlrInput {
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() override;
+  api::Term parseExpr() override;
 
 };/* class Smt2Input */
 
diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp
index ff1a409ae..f0bed978e 100644
--- a/src/parser/smt2/sygus_input.cpp
+++ b/src/parser/smt2/sygus_input.cpp
@@ -63,8 +63,9 @@ Command* SygusInput::parseCommand() {
   return d_pSmt2Parser->parseSygus(d_pSmt2Parser);
 }
 
-Expr SygusInput::parseExpr() {
-  return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
+api::Term SygusInput::parseExpr()
+{
+  return api::Term(d_pSmt2Parser->parseExpr(d_pSmt2Parser));
 }
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h
index a0e3e81ef..39b161655 100644
--- a/src/parser/smt2/sygus_input.h
+++ b/src/parser/smt2/sygus_input.h
@@ -72,11 +72,11 @@ class SygusInput : public AntlrInput {
 
   /**
    * Parse an expression from the input. Returns a null
-   * <code>Expr</code> if there is no expression there to parse.
+   * <code>api::Term</code> if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() override;
+  api::Term parseExpr() override;
 
 };/* class SygusInput */