diff --git a/btor/include/boolector_solver.h b/btor/include/boolector_solver.h
index 672625321..ade43a650 100644
--- a/btor/include/boolector_solver.h
+++ b/btor/include/boolector_solver.h
@@ -75,7 +75,7 @@ class BoolectorSolver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(SortKind sk, const SortVec & sorts) const override;
-
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;
diff --git a/btor/include/boolector_sort.h b/btor/include/boolector_sort.h
index 4387191a5..1919c48ef 100644
--- a/btor/include/boolector_sort.h
+++ b/btor/include/boolector_sort.h
@@ -40,6 +40,8 @@ class BoolectorSortBase : public AbsSort
   SortVec get_domain_sorts() const override;
   Sort get_codomain_sort() const override;
   std::string get_uninterpreted_name() const override;
+  size_t get_arity() const override;
+  SortVec get_uninterpreted_param_sorts() const override;
   Datatype get_datatype() const override;
   bool compare(const Sort s) const override;
   SortKind get_sort_kind() const override { return sk; };
diff --git a/btor/src/boolector_solver.cpp b/btor/src/boolector_solver.cpp
index ac313d7b2..0323d5f40 100644
--- a/btor/src/boolector_solver.cpp
+++ b/btor/src/boolector_solver.cpp
@@ -645,6 +645,14 @@ Sort BoolectorSolver::make_sort(SortKind sk, const SortVec & sorts) const
   }
 }
 
+Sort BoolectorSolver::make_sort(const Sort & sort_con,
+                                const SortVec & sorts) const
+
+{
+  throw IncorrectUsageException(
+      "Boolector does not support uninterpreted sort construction");
+}
+
 Term BoolectorSolver::make_symbol(const std::string name, const Sort & sort)
 {
   // check that name is available
diff --git a/btor/src/boolector_sort.cpp b/btor/src/boolector_sort.cpp
index 6173eed72..ae88636a5 100644
--- a/btor/src/boolector_sort.cpp
+++ b/btor/src/boolector_sort.cpp
@@ -75,12 +75,23 @@ std::string BoolectorSortBase::get_uninterpreted_name() const
       "Boolector doesn't support uninterpreted sorts.");
 }
 
+size_t BoolectorSortBase::get_arity() const
+{
+  throw NotImplementedException(
+      "Boolector does not support uninterpreted sorts");
+}
 
-Datatype BoolectorSortBase::get_datatype() const {
+SortVec BoolectorSortBase::get_uninterpreted_param_sorts() const
+{
+  throw NotImplementedException(
+      "Boolector does not support uninterpreted sorts.");
+}
+
+Datatype BoolectorSortBase::get_datatype() const
+{
   throw NotImplementedException("get_datatype");
 };
 
-
 bool BoolectorSortBase::compare(const Sort s) const
 {
   std::shared_ptr<BoolectorSortBase> bs =
diff --git a/cvc4/include/cvc4_solver.h b/cvc4/include/cvc4_solver.h
index df89c56f0..5e137778c 100644
--- a/cvc4/include/cvc4_solver.h
+++ b/cvc4/include/cvc4_solver.h
@@ -74,6 +74,7 @@ class CVC4Solver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;
diff --git a/cvc4/include/cvc4_sort.h b/cvc4/include/cvc4_sort.h
index 4d874054b..b13a7a5ed 100644
--- a/cvc4/include/cvc4_sort.h
+++ b/cvc4/include/cvc4_sort.h
@@ -42,6 +42,8 @@ namespace smt
     SortVec get_domain_sorts() const override;
     Sort get_codomain_sort() const override;
     std::string get_uninterpreted_name() const override;
+    size_t get_arity() const override;
+    SortVec get_uninterpreted_param_sorts() const override;
     Datatype get_datatype() const override;
     bool compare(const Sort) const override;
     SortKind get_sort_kind() const override;
diff --git a/cvc4/src/cvc4_solver.cpp b/cvc4/src/cvc4_solver.cpp
index 7f379648f..8bedc3062 100644
--- a/cvc4/src/cvc4_solver.cpp
+++ b/cvc4/src/cvc4_solver.cpp
@@ -592,6 +592,24 @@ Sort CVC4Solver::make_sort(SortKind sk, const SortVec & sorts) const
   }
 }
 
+Sort CVC4Solver::make_sort(const Sort & sort_con, const SortVec & sorts) const
+{
+  ::CVC4::api::Sort csort_con =
+      std::static_pointer_cast<CVC4Sort>(sort_con)->sort;
+
+  size_t arity = sorts.size();
+  std::vector<::CVC4::api::Sort> csorts;
+  csorts.reserve(sorts.size());
+  ::CVC4::api::Sort csort;
+  for (uint32_t i = 0; i < arity; i++)
+  {
+    csort = std::static_pointer_cast<CVC4Sort>(sorts[i])->sort;
+    csorts.push_back(csort);
+  }
+
+  return std::make_shared<CVC4Sort>(csort_con.instantiate(csorts));
+}
+
 Term CVC4Solver::make_symbol(const std::string name, const Sort & sort)
 {
   // check that name is available
diff --git a/cvc4/src/cvc4_sort.cpp b/cvc4/src/cvc4_sort.cpp
index d32a03823..bad505cd5 100644
--- a/cvc4/src/cvc4_sort.cpp
+++ b/cvc4/src/cvc4_sort.cpp
@@ -67,9 +67,38 @@ Sort CVC4Sort::get_codomain_sort() const
 
 std::string CVC4Sort::get_uninterpreted_name() const { return sort.toString(); }
 
+size_t CVC4Sort::get_arity() const
+{
+  try
+  {
+    if (sort.isUninterpretedSort())
+    {
+      return 0;
+    }
+    else
+    {
+      return sort.getSortConstructorArity();
+    }
+  }
+  catch (::CVC4::api::CVC4ApiException & e)
+  {
+    throw InternalSolverException(e.what());
+  }
+}
+
+SortVec CVC4Sort::get_uninterpreted_param_sorts() const
+{
+  SortVec param_sorts;
+  for (auto cs : sort.getUninterpretedSortParamSorts())
+  {
+    param_sorts.push_back(std::make_shared<CVC4Sort>(cs));
+  }
+  return param_sorts;
+}
+
 bool CVC4Sort::compare(const Sort s) const
 {
-  std::shared_ptr<CVC4Sort> cs = std::static_pointer_cast<CVC4Sort> (s);
+  std::shared_ptr<CVC4Sort> cs = std::static_pointer_cast<CVC4Sort>(s);
   return sort == cs->sort;
 }
 
@@ -77,14 +106,14 @@ Datatype CVC4Sort::get_datatype() const
 {
   try
   {
-    return std::make_shared<CVC4Datatype> (sort.getDatatype());
-  } catch (::CVC4::api::CVC4ApiException & e)
+    return std::make_shared<CVC4Datatype>(sort.getDatatype());
+  }
+  catch (::CVC4::api::CVC4ApiException & e)
   {
     throw InternalSolverException(e.what());
   }
 };
 
-
 SortKind CVC4Sort::get_sort_kind() const
 {
   if (sort.isBoolean())
@@ -115,6 +144,10 @@ SortKind CVC4Sort::get_sort_kind() const
   {
     return UNINTERPRETED;
   }
+  else if (sort.isSortConstructor())
+  {
+    return UNINTERPRETED_CONS;
+  }
   else if (sort.isDatatype())
   {
     return DATATYPE;
diff --git a/include/logging_solver.h b/include/logging_solver.h
index 52c12ea47..afa70afe4 100644
--- a/include/logging_solver.h
+++ b/include/logging_solver.h
@@ -42,6 +42,7 @@ class LoggingSolver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(const SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;
diff --git a/include/logging_sort.h b/include/logging_sort.h
index 2831799c9..f4c64e325 100644
--- a/include/logging_sort.h
+++ b/include/logging_sort.h
@@ -26,6 +26,10 @@ namespace smt {
 // Sort s is the underlying sort
 // all other sorts are LoggingSorts
 Sort make_uninterpreted_logging_sort(Sort s, std::string name, uint64_t arity);
+Sort make_uninterpreted_logging_sort(Sort s,
+                                     std::string name,
+                                     uint64_t arity,
+                                     const SortVec & sorts);
 Sort make_logging_sort(SortKind sk, Sort s);
 Sort make_logging_sort(SortKind sk, Sort s, uint64_t width);
 Sort make_logging_sort(SortKind sk, Sort s, Sort sort1);
@@ -86,6 +90,18 @@ class LoggingSort : public AbsSort
         "get_uninterpreted_name not implemented by generic LoggingSort");
   }
 
+  size_t get_arity() const override
+  {
+    throw NotImplementedException(
+        "get_arity not implemented by generic LoggingSort");
+  }
+
+  SortVec get_uninterpreted_param_sorts() const override
+  {
+    throw NotImplementedException(
+        "get_uninterpreted_param_sorts not implemented by generic LoggingSort");
+  }
+
   Datatype get_datatype() const override
   {
     throw NotImplementedException(
@@ -150,15 +166,22 @@ class UninterpretedLoggingSort : public LoggingSort
 {
  public:
   UninterpretedLoggingSort(Sort s, std::string n, uint64_t a);
+  UninterpretedLoggingSort(Sort s,
+                           std::string n,
+                           uint64_t a,
+                           const SortVec & sorts);
   ~UninterpretedLoggingSort();
 
   typedef LoggingSort super;
 
   std::string get_uninterpreted_name() const override;
+  size_t get_arity() const override;
+  SortVec get_uninterpreted_param_sorts() const override;
 
  protected:
   std::string name;
   uint64_t arity;
+  SortVec param_sorts;
 };
 
 }  // namespace smt
diff --git a/include/printing_solver.h b/include/printing_solver.h
index 6cc586e34..0e5cbbf33 100644
--- a/include/printing_solver.h
+++ b/include/printing_solver.h
@@ -81,6 +81,7 @@ class PrintingSolver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(const SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
   DatatypeDecl make_datatype_decl(const std::string & s) override;
   DatatypeConstructorDecl make_datatype_constructor_decl(
diff --git a/include/solver.h b/include/solver.h
index ae0f3fdd0..166d20dae 100644
--- a/include/solver.h
+++ b/include/solver.h
@@ -174,6 +174,15 @@ class AbsSmtSolver
    */
   virtual Sort make_sort(const SortKind sk, const SortVec & sorts) const = 0;
 
+  /* Create an uninterpreted sort
+   * @param sort_con a sort with SortKind UNINTERPRETED_CONS (must have
+   * nonzero arity)
+   * @param sorts a vector of sorts of size matching sort_con->get_arity()
+   * @return a Sort object
+   */
+  virtual Sort make_sort(const Sort & sort_con,
+                         const SortVec & sorts) const = 0;
+
   /* Create a datatype sort
    * @param d the Datatype Declaration
    * @return a Sort object
diff --git a/include/sort.h b/include/sort.h
index 77dc7e79e..a2ae376fa 100644
--- a/include/sort.h
+++ b/include/sort.h
@@ -40,6 +40,9 @@ enum SortKind
   REAL,
   FUNCTION,
   UNINTERPRETED,
+  // an uninterpreted sort constructor (has non-zero arity and takes subsort
+  // arguments)
+  UNINTERPRETED_CONS,
   DATATYPE,
 
   /** IMPORTANT: This must stay at the bottom.
@@ -71,6 +74,8 @@ class AbsSort
   virtual std::vector<Sort> get_domain_sorts() const = 0;
   virtual Sort get_codomain_sort() const = 0;
   virtual std::string get_uninterpreted_name() const = 0;
+  virtual size_t get_arity() const = 0;
+  virtual std::vector<Sort> get_uninterpreted_param_sorts() const = 0;
   virtual Datatype get_datatype() const = 0;
   virtual bool compare(const Sort sort) const = 0;
   virtual SortKind get_sort_kind() const = 0;
@@ -103,7 +108,6 @@ template <>
 struct hash<smt::Sort>
 {
   size_t operator()(const smt::Sort & s) const { return s->hash(); }
-  };
-
+};
 }
 
diff --git a/include/term_translator.h b/include/term_translator.h
index c86ceaa9b..d6ff54c92 100644
--- a/include/term_translator.h
+++ b/include/term_translator.h
@@ -63,7 +63,7 @@ class TermTranslator
    *  @param the sort transfer
    *  @return a sort belonging to this solver
    */
-  Sort transfer_sort(const Sort & sort) const;
+  Sort transfer_sort(const Sort & sort);
 
   /** Transfers a term from the other solver to this solver
    *  @param term the term to transfer to the member variable solver
@@ -93,7 +93,7 @@ class TermTranslator
    *  called in this function)
    *  @return a term with the given value
    */
-  Term value_from_smt2(const std::string val, const Sort sort) const;
+  Term value_from_smt2(const std::string val, const Sort sort);
 
   /** identifies relevant casts to perform an operation
    *  assumes the operation is currently not well-sorted
@@ -135,6 +135,10 @@ class TermTranslator
   // it can still call non-const methods of the solver
   SmtSolver solver;  ///< solver to translate terms to
   UnorderedTermMap cache;
+  // map from uninterpreted sort names to the sort in the destination solver
+  // necessary because it needs to be the same exact uninterpreted sort
+  // cannot recreate it with the same name and get the same object back
+  std::unordered_map<std::string, Sort> uninterpreted_sorts;
 };
 }  // namespace smt
 
diff --git a/msat/include/msat_solver.h b/msat/include/msat_solver.h
index cb1c2d45b..0b6f44d87 100644
--- a/msat/include/msat_solver.h
+++ b/msat/include/msat_solver.h
@@ -87,6 +87,7 @@ class MsatSolver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
 
   Sort make_sort(const DatatypeDecl & d) const override;
 
diff --git a/msat/include/msat_sort.h b/msat/include/msat_sort.h
index 79b5661bb..d882d91cb 100644
--- a/msat/include/msat_sort.h
+++ b/msat/include/msat_sort.h
@@ -37,6 +37,8 @@ class MsatSort : public AbsSort
   SortVec get_domain_sorts() const override;
   Sort get_codomain_sort() const override;
   std::string get_uninterpreted_name() const override;
+  size_t get_arity() const override;
+  SortVec get_uninterpreted_param_sorts() const override;
   Datatype get_datatype() const override;
   bool compare(const Sort) const override;
   SortKind get_sort_kind() const override;
diff --git a/msat/src/msat_solver.cpp b/msat/src/msat_solver.cpp
index 95319c46f..202494a1e 100644
--- a/msat/src/msat_solver.cpp
+++ b/msat/src/msat_solver.cpp
@@ -484,6 +484,11 @@ Sort MsatSolver::make_sort(SortKind sk, const SortVec & sorts) const
   }
 }
 
+Sort MsatSolver::make_sort(const Sort & sort_con, const SortVec & sorts) const
+{
+  throw NotImplementedException(
+      "MathSAT does not support uninterpreted sort constructors");
+}
 
 Sort MsatSolver::make_sort(const DatatypeDecl & d) const {
   throw NotImplementedException("MsatSolver::make_sort");
diff --git a/msat/src/msat_sort.cpp b/msat/src/msat_sort.cpp
index 2b815722d..0206c46e0 100644
--- a/msat/src/msat_sort.cpp
+++ b/msat/src/msat_sort.cpp
@@ -116,11 +116,23 @@ string MsatSort::get_uninterpreted_name() const
   return res;
 }
 
-Datatype MsatSort::get_datatype() const {
+size_t MsatSort::get_arity() const
+{
+  // MathSAT does not support uninterpreted sorts with non-zero arity
+  return 0;
+}
+
+SortVec MsatSort::get_uninterpreted_param_sorts() const
+{
+  throw NotImplementedException(
+      "MathSAT does not support uninterpreted sort constructors");
+}
+
+Datatype MsatSort::get_datatype() const
+{
   throw NotImplementedException("get_datatype");
 };
 
-
 bool MsatSort::compare(const Sort s) const
 {
   std::shared_ptr<MsatSort> msort = std::static_pointer_cast<MsatSort>(s);
diff --git a/src/logging_solver.cpp b/src/logging_solver.cpp
index 424d55892..0f9aa6194 100644
--- a/src/logging_solver.cpp
+++ b/src/logging_solver.cpp
@@ -112,6 +112,24 @@ Sort LoggingSolver::make_sort(SortKind sk, const SortVec & sorts) const
   return make_logging_sort(sk, sort, sorts);
 }
 
+Sort LoggingSolver::make_sort(const Sort & sort_con,
+                              const SortVec & sorts) const
+{
+  Sort sub_sort_con = static_pointer_cast<LoggingSort>(sort_con)->wrapped_sort;
+
+  // convert to sorts stored by LoggingSorts
+  SortVec sub_sorts;
+  for (auto s : sorts)
+  {
+    sub_sorts.push_back(static_pointer_cast<LoggingSort>(s)->wrapped_sort);
+  }
+
+  Sort ressort = wrapped_solver->make_sort(sub_sort_con, sub_sorts);
+  return make_uninterpreted_logging_sort(ressort,
+                                         sort_con->get_uninterpreted_name(),
+                                         0,  // has zero arity after applied
+                                         sorts);
+}
 
 Sort LoggingSolver::make_sort(const DatatypeDecl & d) const {
   throw NotImplementedException("LoggingSolver::make_sort");
diff --git a/src/logging_sort.cpp b/src/logging_sort.cpp
index b4264101c..b6d77ffc6 100644
--- a/src/logging_sort.cpp
+++ b/src/logging_sort.cpp
@@ -27,6 +27,20 @@ Sort make_uninterpreted_logging_sort(Sort s, string name, uint64_t arity)
   return std::make_shared<UninterpretedLoggingSort>(s, name, arity);
 }
 
+Sort make_uninterpreted_logging_sort(Sort s,
+                                     string name,
+                                     uint64_t arity,
+                                     const SortVec & sorts)
+{
+  if (sorts.size() != arity)
+  {
+    throw IncorrectUsageException(
+        "Number of uninterpreted param sorts must match sort constructor "
+        "arity");
+  }
+  return std::make_shared<UninterpretedLoggingSort>(s, name, arity, sorts);
+}
+
 Sort make_logging_sort(SortKind sk, Sort s)
 {
   if (sk != BOOL && sk != INT && sk != REAL)
@@ -228,7 +242,17 @@ Sort FunctionLoggingSort::get_codomain_sort() const { return codomain_sort; }
 // UninterpretedLoggingSort
 
 UninterpretedLoggingSort::UninterpretedLoggingSort(Sort s, string n, uint64_t a)
-    : super(UNINTERPRETED, s), name(n), arity(a)
+    // non-zero arity means it's a sort constructor
+    // otherwise it's just an uninterpreted sort
+    : super(a ? UNINTERPRETED_CONS : UNINTERPRETED, s), name(n), arity(a)
+{
+}
+
+UninterpretedLoggingSort::UninterpretedLoggingSort(Sort s,
+                                                   string n,
+                                                   uint64_t a,
+                                                   const SortVec & sorts)
+    : super(UNINTERPRETED, s), name(n), arity(a), param_sorts(sorts)
 {
 }
 
@@ -239,4 +263,11 @@ std::string UninterpretedLoggingSort::get_uninterpreted_name() const
   return name;
 }
 
+size_t UninterpretedLoggingSort::get_arity() const { return arity; }
+
+SortVec UninterpretedLoggingSort::get_uninterpreted_param_sorts() const
+{
+  return param_sorts;
+}
+
 }  // namespace smt
diff --git a/src/printing_solver.cpp b/src/printing_solver.cpp
index cbba50f21..3f4246f0f 100644
--- a/src/printing_solver.cpp
+++ b/src/printing_solver.cpp
@@ -91,6 +91,11 @@ Sort PrintingSolver::make_sort(SortKind sk, const SortVec & sorts) const
   return wrapped_solver->make_sort(sk, sorts);
 }
 
+Sort PrintingSolver::make_sort(const Sort & sort_con,
+                               const SortVec & sorts) const
+{
+  return wrapped_solver->make_sort(sort_con, sorts);
+}
 
 Sort PrintingSolver::make_sort(const DatatypeDecl & d) const {
   throw NotImplementedException("PrintingSolver::make_sort");
diff --git a/src/sort.cpp b/src/sort.cpp
index 1d744d377..089432fb6 100644
--- a/src/sort.cpp
+++ b/src/sort.cpp
@@ -31,7 +31,8 @@ const std::unordered_map<SortKind, std::string> sortkind2str(
       { REAL, "REAL" },
       { FUNCTION, "FUNCTION" },
       { UNINTERPRETED, "UNINTERPRETED" },
-      { DATATYPE, "DATATYPE"} });
+      { UNINTERPRETED_CONS, "UNINTERPRETED_CONS" },
+      { DATATYPE, "DATATYPE" } });
 
 std::string to_string(SortKind sk)
 {
diff --git a/src/term_translator.cpp b/src/term_translator.cpp
index 2ffea605a..27fd91bcc 100644
--- a/src/term_translator.cpp
+++ b/src/term_translator.cpp
@@ -55,7 +55,7 @@ const unordered_map<PrimOp, PrimOp> bv_to_bool_ops({ { BVAnd, And },
                                                      { BVNot, Not },
                                                      { BVComp, Equal } });
 
-Sort TermTranslator::transfer_sort(const Sort & sort) const
+Sort TermTranslator::transfer_sort(const Sort & sort)
 {
   SortKind sk = sort->get_sort_kind();
   if ((sk == INT) || (sk == REAL) || (sk == BOOL))
@@ -86,6 +86,23 @@ Sort TermTranslator::transfer_sort(const Sort & sort) const
     sorts.push_back(transfer_sort(sort->get_codomain_sort()));
     return solver->make_sort(sk, sorts);
   }
+  else if (sk == UNINTERPRETED)
+  {
+    assert(sort->get_arity() == 0);
+    string name = sort->get_uninterpreted_name();
+    auto it = uninterpreted_sorts.find(name);
+    if (it != uninterpreted_sorts.end())
+    {
+      // cache hit
+      return it->second;
+    }
+    else
+    {
+      Sort sort_con = solver->make_sort(name, 0);
+      uninterpreted_sorts[name] = sort_con;
+      return sort_con;
+    }
+  }
   else
   {
     throw SmtException("Failed to transfer sort: " + sort->to_string());
@@ -266,7 +283,7 @@ Term TermTranslator::transfer_term(const Term & term, const SortKind sk)
 }
 
 Term TermTranslator::value_from_smt2(const std::string val,
-                                     const Sort orig_sort) const
+                                     const Sort orig_sort)
 {
   SortKind sk = orig_sort->get_sort_kind();
   Sort sort = transfer_sort(orig_sort);
@@ -464,7 +481,7 @@ Term TermTranslator::cast_op(Op op, const TermVec & terms) const
     casted_children.reserve(terms.size());
     casted_children.push_back(terms[0]);
     SortVec domain_sorts = funsort->get_domain_sorts();
-    assert(terms.size() + 1 == domain_sorts.size());
+    assert(terms.size() == domain_sorts.size() + 1);
     for (size_t i = 1; i < terms.size(); ++i)
     {
       casted_children.push_back(cast_term(terms[i], domain_sorts[i - 1]));
diff --git a/tests/test-term-translation.cpp b/tests/test-term-translation.cpp
index 04730205e..2ff20d4ed 100644
--- a/tests/test-term-translation.cpp
+++ b/tests/test-term-translation.cpp
@@ -274,6 +274,43 @@ TEST_P(TranslationTests, Extract)
   ASSERT_TRUE(r.is_unsat());
 }
 
+TEST_P(TranslationTests, UninterpretedSort)
+{
+  Sort uninterp_sort;
+  try
+  {
+    uninterp_sort = s1->make_sort("uninterp-sort", 0);
+    // need to fail if either solver doesn't support uninterpreted sorts
+    Sort dummy_sort = s2->make_sort("dummy", 0);
+  }
+  catch (SmtException & e)
+  {
+    // if this solver doesn't support uninterpreted sorts, that's fine
+    // just stop the test
+    return;
+  }
+
+  ASSERT_TRUE(uninterp_sort);
+  Sort ufsort = s1->make_sort(FUNCTION, { uninterp_sort, boolsort });
+  Term v = s1->make_symbol("v", uninterp_sort);
+  Term f = s1->make_symbol("f", ufsort);
+  Term fv = s1->make_term(Apply, f, v);
+
+  TermTranslator to_s2(s2);
+  TermTranslator to_s1(s1);
+
+  Term fv_2 = to_s2.transfer_term(fv);
+  EXPECT_EQ(fv_2->get_op(), Apply);
+
+  // populate cache with symbols for back translation
+  UnorderedTermMap & cache = to_s1.get_cache();
+  cache[to_s2.transfer_term(v)] = v;
+  cache[to_s2.transfer_term(f)] = f;
+
+  Term fv_1 = to_s1.transfer_term(fv_2);
+  EXPECT_EQ(fv, fv_1);
+}
+
 TEST_P(BoolArrayTranslationTests, Arrays)
 {
   Term f = s1->make_term(false);
diff --git a/tests/unit/unit-sort.cpp b/tests/unit/unit-sort.cpp
index 9d215a15f..136550cee 100644
--- a/tests/unit/unit-sort.cpp
+++ b/tests/unit/unit-sort.cpp
@@ -93,6 +93,56 @@ TEST_P(UnitSortTests, SortParams)
   // not every solver supports querying function types for domain/codomain yet
 }
 
+TEST_P(UnitSortTests, UninterpretedSort)
+{
+  Sort uninterp_sort;
+  try
+  {
+    uninterp_sort = s->make_sort("declared-sort", 0);
+  }
+  catch (SmtException & e)
+  {
+    // if not supported, that's fine.
+    std::cout << "got exception when declaring sort: " << e.what() << std::endl;
+    return;
+  }
+
+  ASSERT_TRUE(uninterp_sort);
+  EXPECT_EQ(uninterp_sort->get_sort_kind(), UNINTERPRETED);
+  EXPECT_EQ(uninterp_sort->get_arity(), 0);
+
+  // Now try non-zero arity (not supported by very many solvers)
+  Sort sort_cons;
+  try
+  {
+    sort_cons = s->make_sort("sort-con", 4);
+  }
+  catch (SmtException & e)
+  {
+    // if not supported, that's fine.
+    std::cout << "got exception when declaring nonzero arity sort: " << e.what()
+              << std::endl;
+    return;
+  }
+
+  ASSERT_TRUE(sort_cons);
+  // Expecting an uninterpreted constructor sort
+  EXPECT_EQ(sort_cons->get_sort_kind(), UNINTERPRETED_CONS);
+  EXPECT_EQ(sort_cons->get_arity(), 4);
+
+  // now try applying the sort constructor
+  Sort applied_sort_cons =
+      s->make_sort(sort_cons, { bvsort, bvsort, bvsort, boolsort });
+  EXPECT_EQ(applied_sort_cons->get_arity(), 0);
+  std::cout << "before param_sorts with " << s->get_solver_enum() << std::endl;
+  SortVec param_sorts = applied_sort_cons->get_uninterpreted_param_sorts();
+  EXPECT_EQ(param_sorts.size(), 4);
+  EXPECT_EQ(param_sorts[0], bvsort);
+  EXPECT_EQ(param_sorts[1], bvsort);
+  EXPECT_EQ(param_sorts[2], bvsort);
+  EXPECT_EQ(param_sorts[3], boolsort);
+}
+
 TEST_P(UnitSortArithTests, SameSortDiffObj)
 {
   Sort intsort_2 = s->make_sort(INT);
diff --git a/yices2/include/yices2_solver.h b/yices2/include/yices2_solver.h
index de9d7ffc5..b33edc92b 100644
--- a/yices2/include/yices2_solver.h
+++ b/yices2/include/yices2_solver.h
@@ -81,7 +81,7 @@ class Yices2Solver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(SortKind sk, const SortVec & sorts) const override;
-
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;
diff --git a/yices2/include/yices2_sort.h b/yices2/include/yices2_sort.h
index 8282e6e9d..5b9815f6e 100644
--- a/yices2/include/yices2_sort.h
+++ b/yices2/include/yices2_sort.h
@@ -44,6 +44,8 @@ class Yices2Sort : public AbsSort
   SortVec get_domain_sorts() const override;
   Sort get_codomain_sort() const override;
   std::string get_uninterpreted_name() const override;
+  size_t get_arity() const override;
+  SortVec get_uninterpreted_param_sorts() const override;
   Datatype get_datatype() const override;
   bool compare(const Sort s) const override;
   SortKind get_sort_kind() const override;
diff --git a/yices2/src/yices2_solver.cpp b/yices2/src/yices2_solver.cpp
index 2edd821de..bf8bdec7d 100644
--- a/yices2/src/yices2_solver.cpp
+++ b/yices2/src/yices2_solver.cpp
@@ -630,6 +630,12 @@ Sort Yices2Solver::make_sort(SortKind sk, const SortVec & sorts) const
   return std::make_shared<Yices2Sort> (y_sort, true);
 }
 
+Sort Yices2Solver::make_sort(const Sort & sort_con, const SortVec & sorts) const
+{
+  throw NotImplementedException(
+      "Yices2 does not support uninterpreted sort constructors");
+}
+
 Term Yices2Solver::make_symbol(const std::string name, const Sort & sort)
 {
   shared_ptr<Yices2Sort> ysort = static_pointer_cast<Yices2Sort>(sort);
diff --git a/yices2/src/yices2_sort.cpp b/yices2/src/yices2_sort.cpp
index ee8db1715..79e3e29e3 100644
--- a/yices2/src/yices2_sort.cpp
+++ b/yices2/src/yices2_sort.cpp
@@ -113,12 +113,23 @@ string Yices2Sort::get_uninterpreted_name() const
       "get_uninterpreted_name not implemented for Yices2Sort");
 }
 
+size_t Yices2Sort::get_arity() const
+{
+  // yices2 does not support uninterpreted sorts with non-zero arity
+  return 0;
+}
+
+SortVec Yices2Sort::get_uninterpreted_param_sorts() const
+{
+  throw NotImplementedException(
+      "Yices2 does not support uninterpreted sort constructors");
+}
 
-Datatype Yices2Sort::get_datatype() const {
+Datatype Yices2Sort::get_datatype() const
+{
   throw NotImplementedException("get_datatype");
 };
 
-
 bool Yices2Sort::compare(const Sort s) const
 {
   shared_ptr<Yices2Sort> ys = std::static_pointer_cast<Yices2Sort>(s);
@@ -156,6 +167,10 @@ SortKind Yices2Sort::get_sort_kind() const
       return FUNCTION;
     }
   }
+  else if (yices_type_is_uninterpreted(type))
+  {
+    return UNINTERPRETED;
+  }
   else
   {
     std::string msg("Unknown Yices2 type: ");