2 files changed, 17 insertions, 14 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 95f4b1a67..081990a45 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -101,7 +101,7 @@ namespace CVC4 {
       struct myExpr : public CVC4::api::Term {
         myExpr() : CVC4::api::Term() {}
         myExpr(void*) : CVC4::api::Term() {}
-        myExpr(const Expr& e) : CVC4::api::Term(e) {}
+        myExpr(const Expr& e) : CVC4::api::Term(d_solver, e) {}
         myExpr(const myExpr& e) : CVC4::api::Term(e) {}
       };/* struct myExpr */
     }/* CVC4::parser::smt2 namespace */
@@ -286,7 +286,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     { PARSER_STATE->popScope();
       // Do NOT call mkSort, since that creates a new sort!
       // This name is not its own distinct sort, it's an alias.
-      PARSER_STATE->defineParameterizedType(name, sorts, t.getType());
+      PARSER_STATE->defineParameterizedType(name, sorts, t);
       cmd->reset(new DefineTypeCommand(
           name, api::sortVectorToTypes(sorts), t.getType()));
     }
@@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
 
     PARSER_STATE->getUnresolvedSorts().clear();
 
-    ret = datatypeTypes[0];
+    ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]);
   };
 
 // SyGuS grammar term.
@@ -893,7 +893,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
                               << "expression " << atomTerm << std::endl;
         std::stringstream ss;
         ss << atomTerm;
-        sgt.d_op.d_expr = atomTerm.getExpr();
+        sgt.d_op.d_expr = atomTerm;
         sgt.d_name = ss.str();
         sgt.d_gterm_type = SygusGTerm::gterm_op;
       }
@@ -1791,8 +1791,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
           Expr ef = f.getExpr();
           if (Datatype::datatypeOf(ef).isParametric())
           {
-            type = Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
-                       .getSpecializedConstructorType(expr.getSort().getType());
+            type = api::Sort(
+                PARSER_STATE->getSolver(),
+                Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
+                    .getSpecializedConstructorType(expr.getSort().getType()));
           }
           argTypes = type.getConstructorDomainSorts();
         }
@@ -1914,10 +1916,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
       sorts.emplace_back(arg.getSort());
       terms.emplace_back(arg);
     }
-    expr = SOLVER->mkTuple(sorts, terms).getExpr();
+    expr = SOLVER->mkTuple(sorts, terms);
   }
   | /* an atomic term (a term with no subterms) */
-    termAtomic[atomTerm] { expr = atomTerm.getExpr(); }
+    termAtomic[atomTerm] { expr = atomTerm; }
   ;
 
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9ca2194f4..608e47a6b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1377,7 +1377,7 @@ void Smt2::mkSygusDatatype(api::DatatypeDecl& dt,
         if( std::find( types.begin(), types.end(), t )==types.end() ){
           types.push_back( t );
           //identity element
-          api::Sort bt = dt.getDatatype().getSygusType();
+          api::Sort bt = api::Sort(d_solver, dt.getDatatype().getSygusType());
           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
 
           std::stringstream ss;
@@ -1481,7 +1481,7 @@ api::Term Smt2::purifySygusGTerm(api::Term term,
     api::Term ret = d_solver->mkVar(term.getSort());
     Trace("parser-sygus2-debug")
         << "...unresolved non-terminal, intro " << ret << std::endl;
-    args.push_back(ret.getExpr());
+    args.push_back(api::Term(d_solver, ret.getExpr()));
     cargs.push_back(itn->second);
     return ret;
   }
@@ -1571,8 +1571,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
   Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort();
   Trace("parser-qid") << std::endl;
   // otherwise, we process the type ascription
-  p.d_expr =
-      applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr();
+  p.d_expr = applyTypeAscription(p.d_expr, type);
 }
 
 api::Term Smt2::parseOpToExpr(ParseOp& p)
@@ -1776,8 +1775,10 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       parseError(ss.str());
     }
     const Datatype& dt = ((DatatypeType)t.getType()).getDatatype();
-    api::Term ret = d_solver->mkTerm(
-        api::APPLY_SELECTOR, api::Term(dt[0][n].getSelector()), args[0]);
+    api::Term ret =
+        d_solver->mkTerm(api::APPLY_SELECTOR,
+                         api::Term(d_solver, dt[0][n].getSelector()),
+                         args[0]);
     Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
     return ret;
   }