diff --git a/.gitignore b/.gitignore
index 4eb89f3ea..b01e63ad1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -42,3 +42,5 @@ deps/CVC4/
 deps/
 
 local/
+.cache/
+.vscode/
diff --git a/contrib/setup-z3.sh b/contrib/setup-z3.sh
index a04c25a3a..842615ddb 100755
--- a/contrib/setup-z3.sh
+++ b/contrib/setup-z3.sh
@@ -1,13 +1,21 @@
 #!/bin/bash
 set -e
 
-Z3_VERSION=6cc52e04c3ea7e2534644a285d231bdaaafd8714
+Z3_VERSION=z3-4.12.6
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 DEPS=$DIR/../deps
 
 mkdir -p $DEPS
 
+if [ "$(uname)" == "Darwin" ]; then
+    NUM_CORES=$(sysctl -n hw.logicalcpu)
+elif [ "$(expr substr $(uname -s) 1 5)" == "Linux" ]; then
+    NUM_CORES=$(nproc)
+else
+    NUM_CORES=1
+fi
+
 if [ ! -d "$DEPS/z3" ]; then
     cd $DEPS
     git clone https://github.com/Z3Prover/z3.git
@@ -18,10 +26,19 @@ if [ ! -d "$DEPS/z3" ]; then
     # a pthread related issue
     # compiling with --single-threaded helps, but isn't a real solution
     # see https://github.com/Z3Prover/z3/issues/4554
-    ./configure --staticlib --single-threaded
-    cd build
-    make -j$(nproc)
+    cmake -S . -B build -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_LIBZ3_SHARED=Off -DZ3_BUILD_LIBZ3_MSVC_STATIC=On
+    cmake --build build -j$NUM_CORES
     cd $DIR
 else
     echo "$DEPS/z3 already exists. If you want to rebuild, please remove it manually."
 fi
+
+if [ -f $DEPS/z3/build/libz3.a ]; then
+    echo "It appears z3 was setup successfully into $DEPS/z3."
+    echo "You may now install it with make ./configure.sh --z3 && cd build && make"
+else
+    echo "Building z3 failed."
+    echo "You might be missing some dependencies."
+    echo "Please see their github page for installation instructions: https://github.com/z3/z3"
+    exit 1
+fi
diff --git a/src/solver_enums.cpp b/src/solver_enums.cpp
index 84b774d6a..3f5e357d6 100644
--- a/src/solver_enums.cpp
+++ b/src/solver_enums.cpp
@@ -108,6 +108,7 @@ const unordered_map<SolverEnum, unordered_set<SolverAttribute>>
             ARRAY_FUN_BOOLS,
             CONSTARR,
             UNSAT_CORE,
+            THEORY_DATATYPE,
             QUANTIFIERS,
             UNINTERP_SORT,
             TIMELIMIT } },
diff --git a/tests/z3/z3_test.cpp b/tests/z3/z3_test.cpp
index 7bbb6f465..7ce947e91 100644
--- a/tests/z3/z3_test.cpp
+++ b/tests/z3/z3_test.cpp
@@ -32,6 +32,18 @@ int main()
       FUNCTION, SortVec{ boolsort1, intsort1, realsort1, boolsort1 });
   cout << functionsort << endl;
 
+  DatatypeDecl listSpec = s->make_datatype_decl("list");
+  DatatypeConstructorDecl nildecl = s->make_datatype_constructor_decl("nil");
+  DatatypeConstructorDecl consdecl = s->make_datatype_constructor_decl("cons");
+  s->add_selector(consdecl, "head", s->make_sort(INT));
+  s->add_selector_self(consdecl, "tail");
+  s->add_constructor(listSpec, nildecl);
+  s->add_constructor(listSpec, consdecl);
+  Sort listsort = s->make_sort(listSpec);
+  z3::sort sort = std::static_pointer_cast<Z3Sort>(listsort)->get_z3_type();
+  cout << sort << endl
+       << sort.constructors() << endl
+       << sort.recognizers() << endl;
   cout << "* * * end sort testing * * *" << endl
        << "* * * basic term testing * * *" << endl;
 
diff --git a/z3/CMakeLists.txt b/z3/CMakeLists.txt
index 89492d74a..2d2159f07 100644
--- a/z3/CMakeLists.txt
+++ b/z3/CMakeLists.txt
@@ -4,6 +4,7 @@ add_library(smt-switch-z3 "${SMT_SWITCH_LIB_TYPE}"
   "${CMAKE_CURRENT_SOURCE_DIR}/src/z3_solver.cpp"
   "${CMAKE_CURRENT_SOURCE_DIR}/src/z3_sort.cpp"
   "${CMAKE_CURRENT_SOURCE_DIR}/src/z3_term.cpp"
+  "${CMAKE_CURRENT_SOURCE_DIR}/src/z3_datatype.cpp"
   )
 
 target_include_directories (smt-switch-z3 PUBLIC "${PROJECT_SOURCE_DIR}/include")
diff --git a/z3/include/z3_datatype.h b/z3/include/z3_datatype.h
new file mode 100644
index 000000000..ea0741e22
--- /dev/null
+++ b/z3/include/z3_datatype.h
@@ -0,0 +1,62 @@
+#pragma once
+#include "z3++.h"
+#include "datatype.h"
+#include "exceptions.h"
+
+namespace smt {
+
+class Z3DatatypeDecl : public AbsDatatypeDecl
+{
+ public:
+  Z3DatatypeDecl(std::string name) : name(name){};
+
+ protected:
+  friend class Z3Solver;
+  std::string name;
+  std::vector<DatatypeConstructorDecl> consvec {};
+};
+
+class Z3DatatypeConstructorDecl : public AbsDatatypeConstructorDecl
+{
+ public:
+  Z3DatatypeConstructorDecl(z3::context & c, std::string name)
+      : c(c), constructorname(name){};
+  bool compare(const DatatypeConstructorDecl &) const override;
+
+ protected:
+  friend class Z3Solver;
+
+  z3::context & c;
+  std::string constructorname, datatypename;
+  std::vector<z3::symbol> fieldnames {};
+  std::vector<z3::sort> sorts {};
+};
+
+class Z3Datatype : public AbsDatatype
+{
+ public:
+  Z3Datatype(z3::context & c, z3::sort s) : c(c), datatype(s) {}
+  std::string get_name() const override { return datatype.name().str(); }
+  int get_num_constructors() const override
+  {
+    return Z3_get_datatype_sort_num_constructors(c, datatype);
+  }
+  int get_num_selectors(std::string name) const override
+  {
+    for (size_t i = 0; i < get_num_constructors(); i++)
+    {
+      z3::func_decl cons{ c, Z3_get_datatype_sort_constructor(c, datatype, i) };
+      if (cons.name().str() == name) return cons.arity();
+    }
+    throw InternalSolverException(datatype.name().str() + "." + name
+                                  + " not found");
+  }
+
+ private:
+  z3::context & c;
+
+  z3::sort datatype;
+  friend class Z3Solver;
+};
+
+}  // namespace smt
diff --git a/z3/include/z3_solver.h b/z3/include/z3_solver.h
index 5f8fdf25e..7784679c4 100644
--- a/z3/include/z3_solver.h
+++ b/z3/include/z3_solver.h
@@ -26,6 +26,7 @@
 #include "result.h"
 #include "smt.h"
 #include "sort.h"
+#include "z3_datatype.h"
 #include "z3_sort.h"
 #include "z3_term.h"
 
@@ -75,6 +76,8 @@ class Z3Solver : public AbsSmtSolver
   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;
+  SortVec make_datatype_sorts(
+      const std::vector<DatatypeDecl> & decls) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;
   DatatypeConstructorDecl make_datatype_constructor_decl(
@@ -153,5 +156,6 @@ class Z3Solver : public AbsSmtSolver
       throw NotImplementedException("Unimplemented result type from Z3");
     }
   }
+  void add_constructor(z3::sort, z3::constructors*, const DatatypeConstructorDecl&) const;
 };
 }  // namespace smt
diff --git a/z3/src/z3_datatype.cpp b/z3/src/z3_datatype.cpp
new file mode 100644
index 000000000..c12bb5ace
--- /dev/null
+++ b/z3/src/z3_datatype.cpp
@@ -0,0 +1,23 @@
+#include "z3_datatype.h"
+
+namespace z3 {
+const bool operator==(const z3::sort & lhs, const z3::sort & rhs)
+{
+  return z3::eq(lhs, rhs);
+}
+const bool operator==(const z3::symbol & lhs, const z3::symbol & rhs)
+{
+  return lhs.str() == rhs.str();
+}
+}  // namespace z3
+
+namespace smt {
+bool Z3DatatypeConstructorDecl::compare(
+    const DatatypeConstructorDecl & other) const
+{
+  auto cast = std::static_pointer_cast<Z3DatatypeConstructorDecl>(other);
+  return std::tie(constructorname, fieldnames, sorts)
+         == std::tie(cast->constructorname, cast->fieldnames, cast->sorts);
+}
+
+}  // namespace smt
diff --git a/z3/src/z3_solver.cpp b/z3/src/z3_solver.cpp
index 695b68ddd..066c555b1 100644
--- a/z3/src/z3_solver.cpp
+++ b/z3/src/z3_solver.cpp
@@ -3,14 +3,24 @@
 #include <inttypes.h>
 #include <z3++.h>
 
-#include "solver_utils.h"
-
+#include <exception>
 #include <iostream>
+#include <iterator>
+#include <memory>
+
+#include "exceptions.h"
+#include "ops.h"
+#include "smt_defs.h"
+#include "solver_utils.h"
 
 // TEMP for conversions, e.g. creating bit-vectors from base 2 or base 16
 // TODO look deeper into Z3 API to see if there's dedicated support
 //      Note: there is one for base 2 but not an obvious one for base 16
 #include "gmpxx.h"
+#include "sort.h"
+#include "z3_datatype.h"
+#include "z3_sort.h"
+#include "z3_term.h"
 
 using namespace std;
 
@@ -143,7 +153,7 @@ void Z3Solver::set_opt(const std::string option, const std::string value)
   }
   else if (option == "time-limit")
   {
-    unsigned milliseconds = stoi(value)*1000;
+    unsigned milliseconds = stoi(value) * 1000;
     slv.set("timeout", milliseconds);
   }
   else if (option == "produce-unsat-assumptions")
@@ -218,52 +228,194 @@ Term Z3Solver::make_term(bool b) const
 
   return std::make_shared<Z3Term>(z_term, ctx);
 }
+void Z3Solver::add_constructor(z3::sort dtsort,
+                               z3::constructors * cs,
+                               const DatatypeConstructorDecl & cons) const
+{
+  auto z3cons = std::static_pointer_cast<Z3DatatypeConstructorDecl>(cons);
+  auto & cname = z3cons->constructorname;
+  auto recognizer = "is-"s + cname;
+  for (auto & sort : z3cons->sorts)
+  {
+    if (static_cast<Z3_sort>(sort) == nullptr)
+    {
+      sort = dtsort;  // assignment?
+    }
+  }
+  cs->add(ctx.str_symbol(cname.c_str()),
+          ctx.str_symbol(recognizer.c_str()),
+          z3cons->fieldnames.size(),
+          z3cons->fieldnames.data(),
+          z3cons->sorts.data());
+}
 
 Sort Z3Solver::make_sort(const DatatypeDecl & d) const
 {
-  throw NotImplementedException("Z3Solver::make_sort");
-};
+  try
+  {
+    std::shared_ptr<Z3DatatypeDecl> cd =
+        std::static_pointer_cast<Z3DatatypeDecl>(d);
+    auto dtsort = ctx.datatype_sort(ctx.str_symbol(cd->name.c_str()));
+    z3::constructors cs{ ctx };
+    for (auto cons : cd->consvec)
+    {
+      add_constructor(dtsort, &cs, cons);
+    }
+    auto sort = ctx.datatype(ctx.str_symbol(cd->name.data()), cs);
+    return std::make_shared<Z3Sort>(sort, ctx);
+  }
+  catch (z3::exception & e)
+  {
+    throw InternalSolverException(e.what());
+  }
+}
+
+SortVec Z3Solver::make_datatype_sorts(
+    const std::vector<DatatypeDecl> & decls) const
+{
+  std::vector<z3::symbol> syms;
+  std::vector<std::unique_ptr<z3::constructors>> consvec;
+  std::vector<z3::constructor_list> clvec{};
+  std::vector<z3::constructor_list *> clpvec{};  // constructor_list pointer vec
+  for (auto & absdecl : decls)
+  {
+    std::shared_ptr<Z3DatatypeDecl> decl =
+        std::static_pointer_cast<Z3DatatypeDecl>(absdecl);
+    auto dt_symbol = ctx.str_symbol(decl->name.c_str());
+    auto dt_sort = ctx.datatype_sort(dt_symbol);
+    syms.push_back(dt_symbol);
+    auto cs = std::make_unique<z3::constructors>(ctx);
+    for (auto cons : decl->consvec) add_constructor(dt_sort, cs.get(), cons);
+    clvec.emplace_back(*cs);
+    clpvec.push_back(&clvec.back());
+    consvec.push_back(std::move(cs));
+  }
+  auto raw_sorts = ctx.datatypes(decls.size(), syms.data(), clpvec.data());
+  SortVec sorts{};
+  for (auto s : raw_sorts) sorts.push_back(std::make_shared<Z3Sort>(s, ctx));
+  return sorts;
+}
+
 DatatypeDecl Z3Solver::make_datatype_decl(const std::string & s)
 {
-  throw NotImplementedException("Z3Solver::make_datatype_decl");
+  try
+  {
+    return std::make_shared<Z3DatatypeDecl>(s);
+  }
+  catch (z3::exception & e)
+  {
+    throw InternalSolverException(e.what());
+  }
 }
+
 DatatypeConstructorDecl Z3Solver::make_datatype_constructor_decl(
     const std::string s)
 {
-  throw NotImplementedException("Z3Solver::make_datatype_constructor_decl");
-};
+  try
+  {
+    return std::make_shared<Z3DatatypeConstructorDecl>(ctx, s);
+  }
+  catch (z3::exception & e)
+  {
+    throw InternalSolverException(e.what());
+  }
+}
+
 void Z3Solver::add_constructor(DatatypeDecl & dt,
-                               const DatatypeConstructorDecl & con) const
+                               const DatatypeConstructorDecl & cons) const
 {
-  throw NotImplementedException("Z3Solver::add_constructor");
-};
+  try
+  {
+    auto z3dt = std::static_pointer_cast<Z3DatatypeDecl>(dt);
+    z3dt->consvec.push_back(cons);
+  }
+  catch (z3::exception & e)
+  {
+    throw InternalSolverException(e.what());
+  }
+}
+
 void Z3Solver::add_selector(DatatypeConstructorDecl & dt,
                             const std::string & name,
                             const Sort & s) const
 {
-  throw NotImplementedException("Z3Solver::add_selector");
-};
+  try
+  {
+    auto cdt = std::static_pointer_cast<Z3DatatypeConstructorDecl>(dt);
+    cdt->fieldnames.push_back(ctx.str_symbol(name.c_str()));
+    cdt->sorts.push_back(std::static_pointer_cast<Z3Sort>(s)->get_z3_type());
+  }
+  catch (z3::exception & e)
+  {
+    throw InternalSolverException(e.what());
+  }
+}
+
 void Z3Solver::add_selector_self(DatatypeConstructorDecl & dt,
                                  const std::string & name) const
 {
-  throw NotImplementedException("Z3Solver::add_selector_self");
-};
+  try
+  {
+    auto cdt = std::static_pointer_cast<Z3DatatypeConstructorDecl>(dt);
+    cdt->fieldnames.push_back(ctx.str_symbol(name.c_str()));
+    cdt->sorts.emplace_back(ctx);  // push back an empty sort because we don't
+                                   // know the datatype name yet
+  }
+  catch (z3::exception & e)
+  {
+    throw InternalSolverException(e.what());
+  }
+}
 
 Term Z3Solver::get_constructor(const Sort & s, std::string name) const
 {
-  throw NotImplementedException("Z3Solver::get_constructor");
-};
+  try
+  {
+    auto z3sort = std::static_pointer_cast<Z3Sort>(s);
+    auto dt = std::static_pointer_cast<Z3Datatype>(z3sort->get_datatype());
+    for (auto cons_raw : dt->datatype.constructors())
+    {
+      z3::func_decl cons{ ctx, cons_raw };
+      if (cons.name().str() == name) return std::make_shared<Z3Term>(cons, ctx);
+    }
+    throw InternalSolverException("Constructor" + name + " not found");
+  }
+  catch (z3::exception & e)
+  {
+    throw InternalSolverException(e.what());
+  }
+}
+
 Term Z3Solver::get_tester(const Sort & s, std::string name) const
 {
-  throw NotImplementedException("Z3Solver::get_testeer");
-};
+  auto z3sort = std::static_pointer_cast<Z3Sort>(s);
+  auto dt = std::static_pointer_cast<Z3Datatype>(z3sort->get_datatype());
+  for (size_t i = 0; i < dt->get_num_constructors(); i++)
+  {
+    z3::func_decl cons{
+      ctx, Z3_get_datatype_sort_constructor(ctx, dt->datatype, i)
+    };
+    if (cons.name().str() == name)
+      return std::make_shared<Z3Term>(
+          z3::func_decl{
+              ctx, Z3_get_datatype_sort_recognizer(ctx, dt->datatype, i) },
+          ctx);
+  }
+  throw InternalSolverException("tester " + name + " not found");
+}
 
 Term Z3Solver::get_selector(const Sort & s,
                             std::string con,
                             std::string name) const
 {
-  throw NotImplementedException("Z3Solver::get_selector");
-};
+  auto cons = get_constructor(s, con);
+  auto func = std::static_pointer_cast<Z3Term>(cons)->get_z3_func_decl();
+  for (auto field : func.accessors())
+  {
+    if (field.name().str() == name) return std::make_shared<Z3Term>(field, ctx);
+  }
+  throw InternalSolverException("Selector " + name + " not found");
+}
 
 Term Z3Solver::make_term(int64_t i, const Sort & sort) const
 {
@@ -733,11 +885,14 @@ Term Z3Solver::make_term(Op op, const Term & t) const
 
   if (zterm->is_function)
   {
-    throw IncorrectUsageException(
-        "Cannot make a unary operator term with a function.");
+    if (op.prim_op != Apply_Constructor)
+    {
+      throw IncorrectUsageException(
+          "Cannot make a unary operator term with a function.");
+    }
+    res = Z3_mk_app(ctx, zterm->get_z3_func_decl(), 0, 0);
   }
-
-  if (op.prim_op == Extract)
+  else if (op.prim_op == Extract)
   {
     if (op.idx0 < 0 || op.idx1 < 0)
     {
@@ -837,6 +992,8 @@ Term Z3Solver::make_term(Op op, const Term & t0, const Term & t1) const
     {
       return make_term(op, TermVec{ t0, t1 });
     }
+    if (op == Apply_Constructor || op == Apply_Tester || op == Apply_Selector)
+      return make_term(Apply, t0, t1);
     throw IncorrectUsageException(
         "Cannot make a binary op term with a function.");
   }
@@ -903,6 +1060,7 @@ Term Z3Solver::make_term(Op op,
     {
       return make_term(op, TermVec{ t0, t1, t2 });
     }
+    if (op == Apply_Constructor) return make_term(Apply, t0, t1, t2);
     throw IncorrectUsageException(
         "Cannot make a ternary op term with a function.");
   }
diff --git a/z3/src/z3_sort.cpp b/z3/src/z3_sort.cpp
index b374535df..20f67c2fe 100644
--- a/z3/src/z3_sort.cpp
+++ b/z3/src/z3_sort.cpp
@@ -3,6 +3,7 @@
 #include <sstream>
 
 #include "exceptions.h"
+#include "z3_datatype.h"
 
 using namespace std;
 
@@ -126,7 +127,10 @@ SortVec Z3Sort::get_uninterpreted_param_sorts() const
 
 Datatype Z3Sort::get_datatype() const
 {
-  throw NotImplementedException("get_datatype");
+  if (type.is_datatype())
+    return std::make_shared<Z3Datatype>(*ctx, type);
+  else
+    throw InternalSolverException("Sort is not datatype");
 };
 
 bool Z3Sort::compare(const Sort & s) const