diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index 3d75a7d..879830e 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/cvc5_pythonic_api/cvc5_pythonic.py
@@ -135,25 +135,24 @@ class Context(object):
     is that essentially all functions have a context threaded through them.
     There is a default "main" context.
 
-    In cvc5's API, terms and sorts are created using a solver, but stored
-    globally and are freely transferable.
+    Similarly, terms and sorts are created using a term manager in cvc5's API.
 
     Our compatibility solution is:
-    * a context wraps a solver, so that a context can be used to create terms
+    * a context wraps a term manager, so that a context can be used to create terms
     * also, a context does these things:
         * making fresh identifiers for a given sort
         * looking up previously defined constants
     """
 
-    def __init__(self, solver=None):
-        self.solver = solver.solver if solver is not None else SimpleSolver().solver
+    def __init__(self):
+        self.tm = pc.TermManager()
         # Map from (name, sort) pairs to constant terms
         self.vars = {}
         # An increasing identifier used to make fresh identifiers
         self.next_fresh_var = 0
 
     def __del__(self):
-        self.solver = None
+        self.tm = None
 
     def get_var(self, name, sort):
         """Get the variable identified by `name`.
@@ -164,7 +163,7 @@ def get_var(self, name, sort):
         Returns a Term
         """
         if (name, sort) not in self.vars:
-            self.vars[(name, sort)] = self.solver.mkConst(sort.ast, name)
+            self.vars[(name, sort)] = self.tm.mkConst(sort.ast, name)
         return self.vars[(name, sort)]
 
     def next_fresh(self, sort, prefix):
@@ -178,7 +177,7 @@ def next_fresh(self, sort, prefix):
         return name
 
     def __eq__(self, o):
-        return self.solver is o.solver
+        return self.tm is o.tm
 
 
 # Global SMT context
@@ -374,7 +373,7 @@ def __eq__(self, other):
             return False
         a, b = _coerce_exprs(self, other)
         c = self.ctx
-        return BoolRef(c.solver.mkTerm(Kind.EQUAL, a.as_ast(), b.as_ast()), c)
+        return BoolRef(c.tm.mkTerm(Kind.EQUAL, a.as_ast(), b.as_ast()), c)
 
     def __hash__(self):
         """Hash code."""
@@ -398,7 +397,7 @@ def __ne__(self, other):
             return True
         a, b = _coerce_exprs(self, other)
         c = self.ctx
-        return BoolRef(c.solver.mkTerm(Kind.DISTINCT, a.as_ast(), b.as_ast()), c)
+        return BoolRef(c.tm.mkTerm(Kind.DISTINCT, a.as_ast(), b.as_ast()), c)
 
     def decl(self):
         """Return the SMT function declaration associated with an SMT application.
@@ -734,7 +733,7 @@ def DeclareSort(name, ctx=None):
     [a = (as @A_0 A), b = (as @A_0 A)]
     """
     ctx = _get_ctx(ctx)
-    return SortRef(ctx.solver.mkUninterpretedSort(name), ctx)
+    return SortRef(ctx.tm.mkUninterpretedSort(name), ctx)
 
 
 def is_sort(s):
@@ -881,7 +880,7 @@ def _higherorder_apply(func, args, kind):
     for i in range(num):
         tmp = func.domain(i).cast(args[i])
         _args.append(tmp.as_ast())
-    return _to_expr_ref(func.ctx.solver.mkTerm(kind, func.ast, *_args), func.ctx)
+    return _to_expr_ref(func.ctx.tm.mkTerm(kind, func.ast, *_args), func.ctx)
 
 
 def is_func_decl(a):
@@ -912,7 +911,7 @@ def Function(name, *sig):
     if debugging():
         _assert(is_sort(rng), "SMT sort expected")
     ctx = rng.ctx
-    sort = ctx.solver.mkFunctionSort([sig[i].ast for i in range(arity)], rng.ast)
+    sort = ctx.tm.mkFunctionSort([sig[i].ast for i in range(arity)], rng.ast)
     e = ctx.get_var(name, _to_sort_ref(sort, ctx))
     return FuncDeclRef(e, ctx)
 
@@ -933,7 +932,7 @@ def FreshFunction(*sig):
     if debugging():
         _assert(is_sort(rng), "SMT sort expected")
     ctx = rng.ctx
-    sort = ctx.solver.mkFunctionSort([sig[i].ast for i in range(arity)], rng.ast)
+    sort = ctx.tm.mkFunctionSort([sig[i].ast for i in range(arity)], rng.ast)
     name = ctx.next_fresh(sort, "freshfn")
     return Function(name, *sig)
 
@@ -1121,7 +1120,7 @@ def _nary_kind_builder(kind, *args):
             "At least one of the arguments must be an SMT expression",
         )
     args = _coerce_expr_list(args, ctx)
-    return _to_expr_ref(ctx.solver.mkTerm(kind, *[a.ast for a in args]), ctx)
+    return _to_expr_ref(ctx.tm.mkTerm(kind, *[a.ast for a in args]), ctx)
 
 
 def is_expr(a):
@@ -1244,7 +1243,7 @@ def If(a, b, c, ctx=None):
     s = BoolSort(ctx)
     a = s.cast(a)
     b, c = _coerce_exprs(b, c, ctx)
-    return _to_expr_ref(ctx.solver.mkTerm(Kind.ITE, a.ast, b.ast, c.ast), ctx)
+    return _to_expr_ref(ctx.tm.mkTerm(Kind.ITE, a.ast, b.ast, c.ast), ctx)
 
 
 def Distinct(*args):
@@ -1265,7 +1264,7 @@ def Distinct(*args):
             ctx is not None, "At least one of the arguments must be an SMT expression"
         )
     args = _coerce_expr_list(args, ctx)
-    return BoolRef(ctx.solver.mkTerm(Kind.DISTINCT, *[a.ast for a in args]), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.DISTINCT, *[a.ast for a in args]), ctx)
 
 
 def Const(name, sort):
@@ -1490,7 +1489,7 @@ def is_true(a):
     >>> is_true(True)
     False
     """
-    return is_app_of(a, Kind.CONST_BOOLEAN) and a.ast == a.ctx.solver.mkTrue()
+    return is_app_of(a, Kind.CONST_BOOLEAN) and a.ast == a.ctx.tm.mkTrue()
 
 
 def is_false(a):
@@ -1504,7 +1503,7 @@ def is_false(a):
     >>> is_false(BoolVal(False))
     True
     """
-    return is_app_of(a, Kind.CONST_BOOLEAN) and a.ast == a.ctx.solver.mkFalse()
+    return is_app_of(a, Kind.CONST_BOOLEAN) and a.ast == a.ctx.tm.mkFalse()
 
 
 def is_and(a):
@@ -1604,7 +1603,7 @@ def BoolSort(ctx=None):
     True
     """
     ctx = _get_ctx(ctx)
-    return BoolSortRef(ctx.solver.getBooleanSort(), ctx)
+    return BoolSortRef(ctx.tm.getBooleanSort(), ctx)
 
 
 def BoolVal(val, ctx=None):
@@ -1622,9 +1621,9 @@ def BoolVal(val, ctx=None):
     """
     ctx = _get_ctx(ctx)
     if not val:
-        return BoolRef(ctx.solver.mkFalse(), ctx)
+        return BoolRef(ctx.tm.mkFalse(), ctx)
     else:
-        return BoolRef(ctx.solver.mkTrue(), ctx)
+        return BoolRef(ctx.tm.mkTrue(), ctx)
 
 
 def Bool(name, ctx=None):
@@ -1698,7 +1697,7 @@ def Implies(a, b, ctx=None):
     s = BoolSort(ctx)
     a = s.cast(a)
     b = s.cast(b)
-    return BoolRef(ctx.solver.mkTerm(Kind.IMPLIES, a.as_ast(), b.as_ast()), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.IMPLIES, a.as_ast(), b.as_ast()), ctx)
 
 
 def Xor(a, b, ctx=None):
@@ -1712,7 +1711,7 @@ def Xor(a, b, ctx=None):
     s = BoolSort(ctx)
     a = s.cast(a)
     b = s.cast(b)
-    return BoolRef(ctx.solver.mkTerm(Kind.XOR, a.as_ast(), b.as_ast()), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.XOR, a.as_ast(), b.as_ast()), ctx)
 
 
 def Not(a, ctx=None):
@@ -1725,7 +1724,7 @@ def Not(a, ctx=None):
     ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
     s = BoolSort(ctx)
     a = s.cast(a)
-    return BoolRef(ctx.solver.mkTerm(Kind.NOT, a.as_ast()), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.NOT, a.as_ast()), ctx)
 
 
 def mk_not(a):
@@ -1833,9 +1832,7 @@ def __getitem__(self, i):
         """
         if _is_int(i):
             i = IntVal(i, self.ctx)
-        return _to_expr_ref(
-            self.ctx.solver.mkTerm(Kind.SEQ_NTH, self.ast, i.ast), self.ctx
-        )
+        return _to_expr_ref(self.ctx.tm.mkTerm(Kind.SEQ_NTH, self.ast, i.ast), self.ctx)
 
     def at(self, i):
         """Return the sequence at index i
@@ -1848,7 +1845,7 @@ def at(self, i):
         """
         if _is_int(i):
             i = IntVal(i, self.ctx)
-        return SeqRef(self.ctx.solver.mkTerm(Kind.SEQ_AT, self.ast, i.ast), self.ctx)
+        return SeqRef(self.ctx.tm.mkTerm(Kind.SEQ_AT, self.ast, i.ast), self.ctx)
 
     def is_string(self):
         return isinstance(self, StringRef)
@@ -1929,7 +1926,7 @@ def __getitem__(self, i):
         if isinstance(i, int):
             i = IntVal(i, self.ctx)
         return StringRef(
-            self.ctx.solver.mkTerm(Kind.STRING_CHARAT, self.ast, i.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.STRING_CHARAT, self.ast, i.ast), self.ctx
         )
 
     def at(self, i):
@@ -1943,7 +1940,7 @@ def __le__(self, other):
         s <= t
         """
         return BoolRef(
-            self.ctx.solver.mkTerm(Kind.STRING_LEQ, self.ast, other.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.STRING_LEQ, self.ast, other.ast), self.ctx
         )
 
     def __lt__(self, other):
@@ -1954,7 +1951,7 @@ def __lt__(self, other):
         s < t
         """
         return BoolRef(
-            self.ctx.solver.mkTerm(Kind.STRING_LT, self.ast, other.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.STRING_LT, self.ast, other.ast), self.ctx
         )
 
     def __ge__(self, other):
@@ -1965,7 +1962,7 @@ def __ge__(self, other):
         t <= s
         """
         return BoolRef(
-            self.ctx.solver.mkTerm(Kind.STRING_LEQ, other.ast, self.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.STRING_LEQ, other.ast, self.ast), self.ctx
         )
 
     def __gt__(self, other):
@@ -1976,7 +1973,7 @@ def __gt__(self, other):
         t < s
         """
         return BoolRef(
-            self.ctx.solver.mkTerm(Kind.STRING_LT, other.ast, self.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.STRING_LT, other.ast, self.ast), self.ctx
         )
 
 
@@ -1990,7 +1987,7 @@ def StringSort(ctx=None):
     True
     """
     ctx = _get_ctx(ctx)
-    return StringSortRef(ctx.solver.getStringSort(), ctx)
+    return StringSortRef(ctx.tm.getStringSort(), ctx)
 
 
 def String(name, ctx=None):
@@ -2026,7 +2023,7 @@ def SeqSort(s):
     >>> s == Unit(IntVal(1)).sort()
     True
     """
-    return SeqSortRef(s.ctx.solver.mkSequenceSort(s.ast), s.ctx)
+    return SeqSortRef(s.ctx.tm.mkSequenceSort(s.ast), s.ctx)
 
 
 def Empty(s):
@@ -2041,10 +2038,10 @@ def Empty(s):
     (as seq.empty (Seq Int))()
     """
     if isinstance(s, ReSortRef):
-        return ReRef(s.ctx.solver.mkRegexpNone(), s.ctx)
+        return ReRef(s.ctx.tm.mkRegexpNone(), s.ctx)
     if isinstance(s, StringSortRef):
-        return StringRef(s.ctx.solver.mkString(""), s.ctx)
-    return _to_expr_ref(s.ctx.solver.mkEmptySequence(s.elem_sort().ast), s.ctx)
+        return StringRef(s.ctx.tm.mkString(""), s.ctx)
+    return _to_expr_ref(s.ctx.tm.mkEmptySequence(s.elem_sort().ast), s.ctx)
 
 
 def is_seq(a):
@@ -2089,7 +2086,7 @@ def Unit(a):
     >>> i.sort()
     (Seq Int)
     """
-    return SeqRef(a.ctx.solver.mkTerm(Kind.SEQ_UNIT, a.ast), a.ctx)
+    return SeqRef(a.ctx.tm.mkTerm(Kind.SEQ_UNIT, a.ast), a.ctx)
 
 
 def StringVal(val, ctx=None):
@@ -2104,7 +2101,7 @@ def StringVal(val, ctx=None):
     String
     """
     ctx = _get_ctx(ctx)
-    return StringRef(ctx.solver.mkString(str(val)), ctx)
+    return StringRef(ctx.tm.mkString(str(val)), ctx)
 
 
 def Length(s, ctx=None):
@@ -2117,7 +2114,7 @@ def Length(s, ctx=None):
     """
     s = _py2expr(s)
     ctx = _get_ctx(ctx)
-    return ArithRef(ctx.solver.mkTerm(Kind.SEQ_LENGTH, s.ast), ctx)
+    return ArithRef(ctx.tm.mkTerm(Kind.SEQ_LENGTH, s.ast), ctx)
 
 
 def SubString(s, offset, length, ctx=None):
@@ -2133,7 +2130,7 @@ def SubString(s, offset, length, ctx=None):
     offset = _py2expr(offset)
     length = _py2expr(length)
     return StringRef(
-        ctx.solver.mkTerm(Kind.STRING_SUBSTR, s.ast, offset.ast, length.ast), ctx
+        ctx.tm.mkTerm(Kind.STRING_SUBSTR, s.ast, offset.ast, length.ast), ctx
     )
 
 
@@ -2150,7 +2147,7 @@ def SubSeq(s, offset, length):
     offset = _py2expr(offset)
     length = _py2expr(length)
     return SeqRef(
-        s.ctx.solver.mkTerm(Kind.SEQ_EXTRACT, s.ast, offset.ast, length.ast), s.ctx
+        s.ctx.tm.mkTerm(Kind.SEQ_EXTRACT, s.ast, offset.ast, length.ast), s.ctx
     )
 
 
@@ -2166,7 +2163,7 @@ def SeqUpdate(s, t, i):
     (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))()
     """
     i = _py2expr(i)
-    return SeqRef(t.ctx.solver.mkTerm(Kind.SEQ_UPDATE, s.ast, i.ast, t.ast), t.ctx)
+    return SeqRef(t.ctx.tm.mkTerm(Kind.SEQ_UPDATE, s.ast, i.ast, t.ast), t.ctx)
 
 
 def Full(ctx=None):
@@ -2180,7 +2177,7 @@ def Full(ctx=None):
     True
     """
     ctx = _get_ctx(ctx)
-    return ReRef(ctx.solver.mkRegexpAll(), ctx)
+    return ReRef(ctx.tm.mkRegexpAll(), ctx)
 
 
 def Contains(a, b, ctx=None):
@@ -2197,8 +2194,8 @@ def Contains(a, b, ctx=None):
     a = _py2expr(a)
     b = _py2expr(b)
     if is_string(a) and is_string(b):
-        return BoolRef(ctx.solver.mkTerm(Kind.STRING_CONTAINS, a.ast, b.ast), ctx)
-    return BoolRef(ctx.solver.mkTerm(Kind.SEQ_CONTAINS, a.ast, b.ast), ctx)
+        return BoolRef(ctx.tm.mkTerm(Kind.STRING_CONTAINS, a.ast, b.ast), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.SEQ_CONTAINS, a.ast, b.ast), ctx)
 
 
 def PrefixOf(a, b, ctx=None):
@@ -2215,8 +2212,8 @@ def PrefixOf(a, b, ctx=None):
     a = _py2expr(a)
     b = _py2expr(b)
     if is_string(a) and is_string(b):
-        return BoolRef(ctx.solver.mkTerm(Kind.STRING_PREFIX, a.ast, b.ast), ctx)
-    return BoolRef(ctx.solver.mkTerm(Kind.SEQ_PREFIX, a.ast, b.ast), ctx)
+        return BoolRef(ctx.tm.mkTerm(Kind.STRING_PREFIX, a.ast, b.ast), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.SEQ_PREFIX, a.ast, b.ast), ctx)
 
 
 def SuffixOf(a, b, ctx=None):
@@ -2233,8 +2230,8 @@ def SuffixOf(a, b, ctx=None):
     a = _py2expr(a)
     b = _py2expr(b)
     if is_string(a) and is_string(b):
-        return BoolRef(ctx.solver.mkTerm(Kind.STRING_SUFFIX, a.ast, b.ast), ctx)
-    return BoolRef(ctx.solver.mkTerm(Kind.SEQ_SUFFIX, a.ast, b.ast), ctx)
+        return BoolRef(ctx.tm.mkTerm(Kind.STRING_SUFFIX, a.ast, b.ast), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.SEQ_SUFFIX, a.ast, b.ast), ctx)
 
 
 def IndexOf(s, substr, offset=None):
@@ -2256,11 +2253,9 @@ def IndexOf(s, substr, offset=None):
         offset = IntVal(offset, ctx)
     if is_string(s) and is_string(substr):
         return ArithRef(
-            ctx.solver.mkTerm(Kind.STRING_INDEXOF, s.ast, substr.ast, offset.ast), ctx
+            ctx.tm.mkTerm(Kind.STRING_INDEXOF, s.ast, substr.ast, offset.ast), ctx
         )
-    return ArithRef(
-        ctx.solver.mkTerm(Kind.SEQ_INDEXOF, s.ast, substr.ast, offset.ast), ctx
-    )
+    return ArithRef(ctx.tm.mkTerm(Kind.SEQ_INDEXOF, s.ast, substr.ast, offset.ast), ctx)
 
 
 def Replace(s, src, dst):
@@ -2280,9 +2275,9 @@ def Replace(s, src, dst):
     ctx = _get_ctx(None)
     if is_string(s) and is_string(src) and is_string(dst):
         return StringRef(
-            ctx.solver.mkTerm(Kind.STRING_REPLACE, s.ast, src.ast, dst.ast), ctx
+            ctx.tm.mkTerm(Kind.STRING_REPLACE, s.ast, src.ast, dst.ast), ctx
         )
-    return SeqRef(ctx.solver.mkTerm(Kind.SEQ_REPLACE, s.ast, src.ast, dst.ast), ctx)
+    return SeqRef(ctx.tm.mkTerm(Kind.SEQ_REPLACE, s.ast, src.ast, dst.ast), ctx)
 
 
 def StrToInt(s):
@@ -2297,7 +2292,7 @@ def StrToInt(s):
     """
     s = _py2expr(s)
     ctx = _get_ctx(s.ctx)
-    return ArithRef(ctx.solver.mkTerm(Kind.STRING_TO_INT, s.ast), ctx)
+    return ArithRef(ctx.tm.mkTerm(Kind.STRING_TO_INT, s.ast), ctx)
 
 
 def IntToStr(s):
@@ -2312,7 +2307,7 @@ def IntToStr(s):
     """
     s = _py2expr(s)
     ctx = _get_ctx(s.ctx)
-    return StringRef(ctx.solver.mkTerm(Kind.STRING_FROM_INT, s.ast), ctx)
+    return StringRef(ctx.tm.mkTerm(Kind.STRING_FROM_INT, s.ast), ctx)
 
 
 def StrToCode(s):
@@ -2325,7 +2320,7 @@ def StrToCode(s):
     """
     if not is_expr(s):
         s = _py2expr(s)
-    return ArithRef(s.ctx.solver.mkTerm(Kind.STRING_TO_CODE, s.ast), s.ctx)
+    return ArithRef(s.ctx.tm.mkTerm(Kind.STRING_TO_CODE, s.ast), s.ctx)
 
 
 def StrFromCode(c):
@@ -2337,7 +2332,7 @@ def StrFromCode(c):
     """
     if not is_expr(c):
         c = _py2expr(c)
-    return StringRef(c.ctx.solver.mkTerm(Kind.STRING_FROM_CODE, c.ast), c.ctx)
+    return StringRef(c.ctx.tm.mkTerm(Kind.STRING_FROM_CODE, c.ast), c.ctx)
 
 
 #########################################
@@ -2376,7 +2371,7 @@ def ReSort(ctx=None):
 
     if ctx is None or isinstance(ctx, Context):
         ctx = _get_ctx(ctx)
-        return ReSortRef(ctx.solver.getRegExpSort(), ctx)
+        return ReSortRef(ctx.tm.getRegExpSort(), ctx)
 
 
 def Re(s, ctx=None):
@@ -2389,7 +2384,7 @@ def Re(s, ctx=None):
     False
     """
     s = _py2expr(s)
-    return ReRef(s.ctx.solver.mkTerm(Kind.STRING_TO_REGEXP, s.ast), s.ctx)
+    return ReRef(s.ctx.tm.mkTerm(Kind.STRING_TO_REGEXP, s.ast), s.ctx)
 
 
 def is_re(s):
@@ -2416,7 +2411,7 @@ def InRe(s, re):
     False
     """
     s = _py2expr(s)
-    return BoolRef(s.ctx.solver.mkTerm(Kind.STRING_IN_REGEXP, s.ast, re.ast), s.ctx)
+    return BoolRef(s.ctx.tm.mkTerm(Kind.STRING_IN_REGEXP, s.ast, re.ast), s.ctx)
 
 
 def Union(*args):
@@ -2435,9 +2430,9 @@ def Union(*args):
     if sz == 1:
         return args[0]
     ctx = args[0].ctx
-    v = ReRef(ctx.solver.mkTerm(Kind.REGEXP_UNION, args[0].ast, args[1].ast), ctx)
+    v = ReRef(ctx.tm.mkTerm(Kind.REGEXP_UNION, args[0].ast, args[1].ast), ctx)
     for i in range(2, sz):
-        v = ReRef(ctx.solver.mkTerm(Kind.REGEXP_UNION, v.ast, args[i].ast), ctx)
+        v = ReRef(ctx.tm.mkTerm(Kind.REGEXP_UNION, v.ast, args[i].ast), ctx)
     return v
 
 
@@ -2458,9 +2453,9 @@ def Intersect(*args):
     if sz == 1:
         return args[0]
     ctx = args[0].ctx
-    v = ReRef(ctx.solver.mkTerm(Kind.REGEXP_INTER, args[0].ast, args[1].ast), ctx)
+    v = ReRef(ctx.tm.mkTerm(Kind.REGEXP_INTER, args[0].ast, args[1].ast), ctx)
     for i in range(2, sz):
-        v = ReRef(ctx.solver.mkTerm(Kind.REGEXP_INTER, v.ast, args[i].ast), ctx)
+        v = ReRef(ctx.tm.mkTerm(Kind.REGEXP_INTER, v.ast, args[i].ast), ctx)
     return v
 
 
@@ -2475,7 +2470,7 @@ def Option(re):
     >>> print(simplify(InRe("aa", re)))
     False
     """
-    return ReRef(re.ctx.solver.mkTerm(Kind.REGEXP_OPT, re.ast), re.ctx)
+    return ReRef(re.ctx.tm.mkTerm(Kind.REGEXP_OPT, re.ast), re.ctx)
 
 
 def Complement(re):
@@ -2488,7 +2483,7 @@ def Complement(re):
     >>> simplify(InRe('aa',comp_re))
     True
     """
-    return ReRef(re.ctx.solver.mkTerm(Kind.REGEXP_COMPLEMENT, re.ast), re.ctx)
+    return ReRef(re.ctx.tm.mkTerm(Kind.REGEXP_COMPLEMENT, re.ast), re.ctx)
 
 
 def Plus(re):
@@ -2502,7 +2497,7 @@ def Plus(re):
     >>> print(simplify(InRe("", re)))
     False
     """
-    return ReRef(re.ctx.solver.mkTerm(Kind.REGEXP_PLUS, re.ast), re.ctx)
+    return ReRef(re.ctx.tm.mkTerm(Kind.REGEXP_PLUS, re.ast), re.ctx)
 
 
 def Star(re):
@@ -2516,7 +2511,7 @@ def Star(re):
     >>> print(simplify(InRe("", re)))
     True
     """
-    return ReRef(re.ctx.solver.mkTerm(Kind.REGEXP_STAR, re.ast), re.ctx)
+    return ReRef(re.ctx.tm.mkTerm(Kind.REGEXP_STAR, re.ast), re.ctx)
 
 
 def Loop(re, lo, hi=0):
@@ -2531,7 +2526,7 @@ def Loop(re, lo, hi=0):
     False
     """
     return ReRef(
-        re.ctx.solver.mkTerm(re.ctx.solver.mkOp(Kind.REGEXP_LOOP, lo, hi), re.ast),
+        re.ctx.tm.mkTerm(re.ctx.tm.mkOp(Kind.REGEXP_LOOP, lo, hi), re.ast),
         re.ctx,
     )
 
@@ -2547,7 +2542,7 @@ def Range(lo, hi, ctx=None):
     """
     lo = _py2expr(lo, ctx)
     hi = _py2expr(hi, ctx)
-    return ReRef(lo.ctx.solver.mkTerm(Kind.REGEXP_RANGE, lo.ast, hi.ast), lo.ctx)
+    return ReRef(lo.ctx.tm.mkTerm(Kind.REGEXP_RANGE, lo.ast, hi.ast), lo.ctx)
 
 
 def Diff(a, b, ctx=None):
@@ -2560,7 +2555,7 @@ def Diff(a, b, ctx=None):
     >>> simplify(InRe('b',Diff(r2,r1)))
     True
     """
-    return ReRef(a.ctx.solver.mkTerm(Kind.REGEXP_DIFF, a.ast, b.ast), a.ctx)
+    return ReRef(a.ctx.tm.mkTerm(Kind.REGEXP_DIFF, a.ast, b.ast), a.ctx)
 
 
 def AllChar():
@@ -2575,7 +2570,7 @@ def AllChar():
     False
     """
     ctx = _get_ctx(None)
-    return ReRef(ctx.solver.mkRegexpAllchar(), ctx)
+    return ReRef(ctx.tm.mkRegexpAllchar(), ctx)
 
 
 #########################################
@@ -2600,7 +2595,7 @@ def is_real(self):
         >>> x.is_real()
         False
         """
-        return self.ast == self.ctx.solver.getRealSort()
+        return self.ast == self.ctx.tm.getRealSort()
 
     def is_int(self):
         """Return `True` if `self` is of the sort Integer.
@@ -2614,7 +2609,7 @@ def is_int(self):
         >>> x.is_int()
         False
         """
-        return self.ast == self.ctx.solver.getIntegerSort()
+        return self.ast == self.ctx.tm.getIntegerSort()
 
     def subsort(self, other):
         """Return `True` if `self` is a subsort of `other`."""
@@ -2735,7 +2730,7 @@ def __add__(self, other):
         Int
         """
         a, b = _coerce_exprs(self, other)
-        return ArithRef(a.ctx.solver.mkTerm(Kind.ADD, a.ast, b.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.ADD, a.ast, b.ast), self.ctx)
 
     def __radd__(self, other):
         """Create the SMT expression `other + self`.
@@ -2745,7 +2740,7 @@ def __radd__(self, other):
         10 + x
         """
         a, b = _coerce_exprs(self, other)
-        return ArithRef(a.ctx.solver.mkTerm(Kind.ADD, b.ast, a.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.ADD, b.ast, a.ast), self.ctx)
 
     def __mul__(self, other):
         """Create the SMT expression `self * other`.
@@ -2762,7 +2757,7 @@ def __mul__(self, other):
         if isinstance(other, BoolRef):
             return other.__mul__(self)
         a, b = _coerce_exprs(self, other)
-        return ArithRef(a.ctx.solver.mkTerm(Kind.MULT, a.ast, b.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.MULT, a.ast, b.ast), self.ctx)
 
     def __rmul__(self, other):
         """Create the SMT expression `other * self`.
@@ -2772,7 +2767,7 @@ def __rmul__(self, other):
         10*x
         """
         a, b = _coerce_exprs(self, other)
-        return ArithRef(a.ctx.solver.mkTerm(Kind.MULT, b.ast, a.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.MULT, b.ast, a.ast), self.ctx)
 
     def __sub__(self, other):
         """Create the SMT expression `self - other`.
@@ -2785,7 +2780,7 @@ def __sub__(self, other):
         Int
         """
         a, b = _coerce_exprs(self, other)
-        return ArithRef(a.ctx.solver.mkTerm(Kind.SUB, a.ast, b.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.SUB, a.ast, b.ast), self.ctx)
 
     def __rsub__(self, other):
         """Create the SMT expression `other - self`.
@@ -2795,7 +2790,7 @@ def __rsub__(self, other):
         10 - x
         """
         a, b = _coerce_exprs(self, other)
-        return ArithRef(a.ctx.solver.mkTerm(Kind.SUB, b.ast, a.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.SUB, b.ast, a.ast), self.ctx)
 
     def __pow__(self, other):
         """Create the SMT expression `self**other` (** is the power operator).
@@ -2809,7 +2804,7 @@ def __pow__(self, other):
         [x = 1]
         """
         a, b = _coerce_exprs(self, other)
-        return ArithRef(a.ctx.solver.mkTerm(Kind.POW, a.ast, b.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.POW, a.ast, b.ast), self.ctx)
 
     def __rpow__(self, other):
         """Create the SMT expression `other**self` (** is the power operator).
@@ -2821,7 +2816,7 @@ def __rpow__(self, other):
         Real
         """
         a, b = _coerce_exprs(self, other)
-        return ArithRef(a.ctx.solver.mkTerm(Kind.POW, b.ast, a.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.POW, b.ast, a.ast), self.ctx)
 
     def __div__(self, other):
         """Create the SMT expression `other/self`.
@@ -2848,7 +2843,7 @@ def __div__(self, other):
             k = Kind.INTS_DIVISION
         else:
             k = Kind.DIVISION
-        return ArithRef(a.ctx.solver.mkTerm(k, a.ast, b.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(k, a.ast, b.ast), self.ctx)
 
     def __truediv__(self, other):
         """Create the SMT expression `other/self`."""
@@ -2873,7 +2868,7 @@ def __rdiv__(self, other):
             k = Kind.INTS_DIVISION
         else:
             k = Kind.DIVISION
-        return ArithRef(a.ctx.solver.mkTerm(k, b.ast, a.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(k, b.ast, a.ast), self.ctx)
 
     def __rtruediv__(self, other):
         """Create the SMT expression `other/self`."""
@@ -2890,7 +2885,7 @@ def __mod__(self, other):
         a, b = _coerce_exprs(self, other)
         if debugging():
             _assert(a.sort().is_int(), "SMT integer expression expected")
-        return ArithRef(a.ctx.solver.mkTerm(Kind.INTS_MODULUS, a.ast, b.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.INTS_MODULUS, a.ast, b.ast), self.ctx)
 
     def __rmod__(self, other):
         """Create the SMT expression `other%self`.
@@ -2902,7 +2897,7 @@ def __rmod__(self, other):
         a, b = _coerce_exprs(self, other)
         if debugging():
             _assert(a.sort().is_int(), "SMT integer expression expected")
-        return ArithRef(a.ctx.solver.mkTerm(Kind.INTS_MODULUS, b.ast, a.ast), self.ctx)
+        return ArithRef(a.ctx.tm.mkTerm(Kind.INTS_MODULUS, b.ast, a.ast), self.ctx)
 
     def __neg__(self):
         """Return an expression representing `-self`.
@@ -2911,7 +2906,7 @@ def __neg__(self):
         >>> -x
         -x
         """
-        return ArithRef(self.ctx.solver.mkTerm(Kind.NEG, self.ast), self.ctx)
+        return ArithRef(self.ctx.tm.mkTerm(Kind.NEG, self.ast), self.ctx)
 
     def __pos__(self):
         """Return `self`.
@@ -2933,7 +2928,7 @@ def __le__(self, other):
         ToReal(x) <= y
         """
         a, b = _coerce_exprs(self, other)
-        return BoolRef(a.ctx.solver.mkTerm(Kind.LEQ, a.ast, b.ast), self.ctx)
+        return BoolRef(a.ctx.tm.mkTerm(Kind.LEQ, a.ast, b.ast), self.ctx)
 
     def __lt__(self, other):
         """Create the SMT expression `other < self`.
@@ -2946,7 +2941,7 @@ def __lt__(self, other):
         ToReal(x) < y
         """
         a, b = _coerce_exprs(self, other)
-        return BoolRef(a.ctx.solver.mkTerm(Kind.LT, a.ast, b.ast), self.ctx)
+        return BoolRef(a.ctx.tm.mkTerm(Kind.LT, a.ast, b.ast), self.ctx)
 
     def __gt__(self, other):
         """Create the SMT expression `other > self`.
@@ -2959,7 +2954,7 @@ def __gt__(self, other):
         ToReal(x) > y
         """
         a, b = _coerce_exprs(self, other)
-        return BoolRef(a.ctx.solver.mkTerm(Kind.GT, a.ast, b.ast), self.ctx)
+        return BoolRef(a.ctx.tm.mkTerm(Kind.GT, a.ast, b.ast), self.ctx)
 
     def __ge__(self, other):
         """Create the SMT expression `other >= self`.
@@ -2972,7 +2967,7 @@ def __ge__(self, other):
         ToReal(x) >= y
         """
         a, b = _coerce_exprs(self, other)
-        return BoolRef(a.ctx.solver.mkTerm(Kind.GEQ, a.ast, b.ast), self.ctx)
+        return BoolRef(a.ctx.tm.mkTerm(Kind.GEQ, a.ast, b.ast), self.ctx)
 
 
 def is_arith(a):
@@ -3465,7 +3460,7 @@ def IntVal(val, ctx=None):
     100
     """
     ctx = _get_ctx(ctx)
-    return IntNumRef(ctx.solver.mkInteger(_to_int_str(val)), ctx)
+    return IntNumRef(ctx.tm.mkInteger(_to_int_str(val)), ctx)
 
 
 def RealVal(val, ctx=None):
@@ -3484,7 +3479,7 @@ def RealVal(val, ctx=None):
     3/2
     """
     ctx = _get_ctx(ctx)
-    return RatNumRef(ctx.solver.mkReal(str(val)), ctx)
+    return RatNumRef(ctx.tm.mkReal(str(val)), ctx)
 
 
 def RatVal(a, b, ctx=None):
@@ -3507,7 +3502,7 @@ def RatVal(a, b, ctx=None):
             _is_int(b) or isinstance(b, str),
             "Second argument cannot be converted into an integer",
         )
-    return RatNumRef(ctx.solver.mkReal(a, b), ctx)
+    return RatNumRef(ctx.tm.mkReal(a, b), ctx)
 
 
 def Q(a, b, ctx=None):
@@ -3540,7 +3535,7 @@ def ToReal(a):
     if debugging():
         _assert(a.is_int(), "SMT integer expression expected.")
     ctx = a.ctx
-    return ArithRef(ctx.solver.mkTerm(Kind.TO_REAL, a.ast), ctx)
+    return ArithRef(ctx.tm.mkTerm(Kind.TO_REAL, a.ast), ctx)
 
 
 def ToInt(a):
@@ -3558,7 +3553,7 @@ def ToInt(a):
     if debugging():
         _assert(a.is_real(), "SMT real expression expected.")
     ctx = a.ctx
-    return ArithRef(ctx.solver.mkTerm(Kind.TO_INTEGER, a.ast), ctx)
+    return ArithRef(ctx.tm.mkTerm(Kind.TO_INTEGER, a.ast), ctx)
 
 
 def IntSort(ctx=None):
@@ -3575,7 +3570,7 @@ def IntSort(ctx=None):
     False
     """
     ctx = _get_ctx(ctx)
-    return ArithSortRef(ctx.solver.getIntegerSort(), ctx)
+    return ArithSortRef(ctx.tm.getIntegerSort(), ctx)
 
 
 def RealSort(ctx=None):
@@ -3592,7 +3587,7 @@ def RealSort(ctx=None):
     True
     """
     ctx = _get_ctx(ctx)
-    return ArithSortRef(ctx.solver.getRealSort(), ctx)
+    return ArithSortRef(ctx.tm.getRealSort(), ctx)
 
 
 def Int(name, ctx=None):
@@ -3725,7 +3720,7 @@ def IsInt(a):
     if debugging():
         _assert(a.is_real(), "SMT real expression expected.")
     ctx = a.ctx
-    return BoolRef(ctx.solver.mkTerm(Kind.IS_INTEGER, a.ast), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.IS_INTEGER, a.ast), ctx)
 
 
 def Sqrt(a, ctx=None):
@@ -3931,7 +3926,7 @@ def Pi(ctx=None):
     Pi
     """
     ctx = get_ctx(ctx)
-    return _to_expr_ref(ctx.solver.mkTerm(Kind.PI), ctx)
+    return _to_expr_ref(ctx.tm.mkTerm(Kind.PI), ctx)
 
 
 def Exponential(x):
@@ -4146,9 +4141,7 @@ def __add__(self, other):
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_ADD, a.ast, b.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_ADD, a.ast, b.ast), self.ctx)
 
     def __radd__(self, other):
         """Create the SMT expression `other + self`.
@@ -4158,9 +4151,7 @@ def __radd__(self, other):
         10 + x
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_ADD, b.ast, a.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_ADD, b.ast, a.ast), self.ctx)
 
     def __mul__(self, other):
         """Create the SMT expression `self * other`.
@@ -4174,7 +4165,7 @@ def __mul__(self, other):
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_MULT, a.ast, b.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.BITVECTOR_MULT, a.ast, b.ast), self.ctx
         )
 
     def __rmul__(self, other):
@@ -4186,7 +4177,7 @@ def __rmul__(self, other):
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_MULT, b.ast, a.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.BITVECTOR_MULT, b.ast, a.ast), self.ctx
         )
 
     def __sub__(self, other):
@@ -4200,9 +4191,7 @@ def __sub__(self, other):
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SUB, a.ast, b.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SUB, a.ast, b.ast), self.ctx)
 
     def __rsub__(self, other):
         """Create the SMT expression `other - self`.
@@ -4212,9 +4201,7 @@ def __rsub__(self, other):
         10 - x
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SUB, b.ast, a.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SUB, b.ast, a.ast), self.ctx)
 
     def __or__(self, other):
         """Create the SMT expression bitwise-or `self | other`.
@@ -4227,9 +4214,7 @@ def __or__(self, other):
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_OR, a.ast, b.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_OR, a.ast, b.ast), self.ctx)
 
     def __ror__(self, other):
         """Create the SMT expression bitwise-or `other | self`.
@@ -4239,9 +4224,7 @@ def __ror__(self, other):
         10 | x
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_OR, b.ast, a.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_OR, b.ast, a.ast), self.ctx)
 
     def __and__(self, other):
         """Create the SMT expression bitwise-and `self & other`.
@@ -4254,9 +4237,7 @@ def __and__(self, other):
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_AND, a.ast, b.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_AND, a.ast, b.ast), self.ctx)
 
     def __rand__(self, other):
         """Create the SMT expression bitwise-or `other & self`.
@@ -4266,9 +4247,7 @@ def __rand__(self, other):
         10 & x
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_AND, b.ast, a.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_AND, b.ast, a.ast), self.ctx)
 
     def __xor__(self, other):
         """Create the SMT expression bitwise-xor `self ^ other`.
@@ -4281,9 +4260,7 @@ def __xor__(self, other):
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_XOR, a.ast, b.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_XOR, a.ast, b.ast), self.ctx)
 
     def __rxor__(self, other):
         """Create the SMT expression bitwise-xor `other ^ self`.
@@ -4293,9 +4270,7 @@ def __rxor__(self, other):
         10 ^ x
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_XOR, b.ast, a.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_XOR, b.ast, a.ast), self.ctx)
 
     def __pos__(self):
         """Return `self`.
@@ -4315,7 +4290,7 @@ def __neg__(self):
         >>> solve([-(-x) != x])
         no solution
         """
-        return BitVecRef(self.ctx.solver.mkTerm(Kind.BITVECTOR_NEG, self.ast), self.ctx)
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_NEG, self.ast), self.ctx)
 
     def __invert__(self):
         """Create the SMT expression bitwise-not `~self`.
@@ -4326,7 +4301,7 @@ def __invert__(self):
         >>> solve([~(~x) != x])
         no solution
         """
-        return BitVecRef(self.ctx.solver.mkTerm(Kind.BITVECTOR_NOT, self.ast), self.ctx)
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_NOT, self.ast), self.ctx)
 
     def __div__(self, other):
         """Create the SMT expression (signed) division `self / other`.
@@ -4346,7 +4321,7 @@ def __div__(self, other):
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SDIV, a.ast, b.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.BITVECTOR_SDIV, a.ast, b.ast), self.ctx
         )
 
     def __truediv__(self, other):
@@ -4368,7 +4343,7 @@ def __rdiv__(self, other):
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SDIV, b.ast, a.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.BITVECTOR_SDIV, b.ast, a.ast), self.ctx
         )
 
     def __rtruediv__(self, other):
@@ -4395,7 +4370,7 @@ def __mod__(self, other):
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SMOD, a.ast, b.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.BITVECTOR_SMOD, a.ast, b.ast), self.ctx
         )
 
     def __rmod__(self, other):
@@ -4415,7 +4390,7 @@ def __rmod__(self, other):
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SMOD, b.ast, a.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.BITVECTOR_SMOD, b.ast, a.ast), self.ctx
         )
 
     def __le__(self, other):
@@ -4432,9 +4407,7 @@ def __le__(self, other):
         '(bvule x y)'
         """
         a, b = _coerce_exprs(self, other)
-        return BoolRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SLE, a.ast, b.ast), self.ctx
-        )
+        return BoolRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SLE, a.ast, b.ast), self.ctx)
 
     def __lt__(self, other):
         """Create the SMT expression (signed) `other < self`.
@@ -4450,9 +4423,7 @@ def __lt__(self, other):
         '(bvult x y)'
         """
         a, b = _coerce_exprs(self, other)
-        return BoolRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SLT, a.ast, b.ast), self.ctx
-        )
+        return BoolRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SLT, a.ast, b.ast), self.ctx)
 
     def __gt__(self, other):
         """Create the SMT expression (signed) `other > self`.
@@ -4468,9 +4439,7 @@ def __gt__(self, other):
         '(bvugt x y)'
         """
         a, b = _coerce_exprs(self, other)
-        return BoolRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SGT, a.ast, b.ast), self.ctx
-        )
+        return BoolRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SGT, a.ast, b.ast), self.ctx)
 
     def __ge__(self, other):
         """Create the SMT expression (signed) `other >= self`.
@@ -4486,9 +4455,7 @@ def __ge__(self, other):
         '(bvuge x y)'
         """
         a, b = _coerce_exprs(self, other)
-        return BoolRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SGE, a.ast, b.ast), self.ctx
-        )
+        return BoolRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SGE, a.ast, b.ast), self.ctx)
 
     def __rshift__(self, other):
         """Create the SMT expression (arithmetical) right shift `self >> other`
@@ -4519,7 +4486,7 @@ def __rshift__(self, other):
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_ASHR, a.ast, b.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.BITVECTOR_ASHR, a.ast, b.ast), self.ctx
         )
 
     def __lshift__(self, other):
@@ -4534,9 +4501,7 @@ def __lshift__(self, other):
         4
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SHL, a.ast, b.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SHL, a.ast, b.ast), self.ctx)
 
     def __rrshift__(self, other):
         """Create the SMT expression (arithmetical) right shift `other` >> `self`.
@@ -4551,7 +4516,7 @@ def __rrshift__(self, other):
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_ASHR, b.ast, a.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.BITVECTOR_ASHR, b.ast, a.ast), self.ctx
         )
 
     def __rlshift__(self, other):
@@ -4566,9 +4531,7 @@ def __rlshift__(self, other):
         '(bvshl #b00000000000000000000000000001010 x)'
         """
         a, b = _coerce_exprs(self, other)
-        return BitVecRef(
-            self.ctx.solver.mkTerm(Kind.BITVECTOR_SHL, b.ast, a.ast), self.ctx
-        )
+        return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SHL, b.ast, a.ast), self.ctx)
 
 
 class BitVecNumRef(BitVecRef):
@@ -4668,7 +4631,7 @@ def BV2Int(a, is_signed=False):
         nat = BV2Int(a)
         return If(a < 0, nat - (2**w), nat)
     else:
-        return ArithRef(ctx.solver.mkTerm(Kind.BITVECTOR_TO_NAT, a.ast), ctx)
+        return ArithRef(ctx.tm.mkTerm(Kind.BITVECTOR_TO_NAT, a.ast), ctx)
 
 
 def Int2BV(a, num_bits):
@@ -4684,7 +4647,7 @@ def Int2BV(a, num_bits):
     """
     ctx = a.ctx
     return BitVecRef(
-        ctx.solver.mkTerm(ctx.solver.mkOp(Kind.INT_TO_BITVECTOR, num_bits), a.ast), ctx
+        ctx.tm.mkTerm(ctx.tm.mkOp(Kind.INT_TO_BITVECTOR, num_bits), a.ast), ctx
     )
 
 
@@ -4700,7 +4663,7 @@ def BitVecSort(sz, ctx=None):
     True
     """
     ctx = _get_ctx(ctx)
-    return BitVecSortRef(ctx.solver.mkBitVectorSort(sz), ctx)
+    return BitVecSortRef(ctx.tm.mkBitVectorSort(sz), ctx)
 
 
 def BitVecVal(val, bv, ctx=None):
@@ -4725,7 +4688,7 @@ def BitVecVal(val, bv, ctx=None):
         ctx = _get_ctx(ctx)
     modulus = 2**size
     val = (val + modulus) % modulus
-    return BitVecNumRef(ctx.solver.mkBitVector(size, str(val), 10), ctx)
+    return BitVecNumRef(ctx.tm.mkBitVector(size, str(val), 10), ctx)
 
 
 def BitVec(name, bv, ctx=None):
@@ -4799,12 +4762,12 @@ def Concat(*args):
             "All arguments must be SMT bit-vector, string, sequence or re expressions.",
         )
     if is_string(args[0]):
-        return StringRef(ctx.solver.mkTerm(Kind.STRING_CONCAT, *[a.ast for a in args]))
+        return StringRef(ctx.tm.mkTerm(Kind.STRING_CONCAT, *[a.ast for a in args]))
     if is_seq(args[0]):
-        return SeqRef(ctx.solver.mkTerm(Kind.SEQ_CONCAT, *[a.ast for a in args]), ctx)
+        return SeqRef(ctx.tm.mkTerm(Kind.SEQ_CONCAT, *[a.ast for a in args]), ctx)
     if is_re(args[0]):
-        return ReRef(ctx.solver.mkTerm(Kind.REGEXP_CONCAT, *[a.ast for a in args]))
-    return BitVecRef(ctx.solver.mkTerm(Kind.BITVECTOR_CONCAT, *[a.ast for a in args]))
+        return ReRef(ctx.tm.mkTerm(Kind.REGEXP_CONCAT, *[a.ast for a in args]))
+    return BitVecRef(ctx.tm.mkTerm(Kind.BITVECTOR_CONCAT, *[a.ast for a in args]))
 
 
 def Extract(high, low, a):
@@ -4827,9 +4790,7 @@ def Extract(high, low, a):
         )
         _assert(is_bv(a), "Third argument must be an SMT bit-vector expression")
     return BitVecRef(
-        a.ctx.solver.mkTerm(
-            a.ctx.solver.mkOp(Kind.BITVECTOR_EXTRACT, high, low), a.ast
-        ),
+        a.ctx.tm.mkTerm(a.ctx.tm.mkOp(Kind.BITVECTOR_EXTRACT, high, low), a.ast),
         a.ctx,
     )
 
@@ -4857,7 +4818,7 @@ def ULE(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BoolRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_ULE, a.ast, b.ast), a.ctx)
+    return BoolRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_ULE, a.ast, b.ast), a.ctx)
 
 
 def ULT(a, b):
@@ -4875,7 +4836,7 @@ def ULT(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BoolRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_ULT, a.ast, b.ast), a.ctx)
+    return BoolRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_ULT, a.ast, b.ast), a.ctx)
 
 
 def UGE(a, b):
@@ -4893,7 +4854,7 @@ def UGE(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BoolRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_UGE, a.ast, b.ast), a.ctx)
+    return BoolRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_UGE, a.ast, b.ast), a.ctx)
 
 
 def UGT(a, b):
@@ -4911,7 +4872,7 @@ def UGT(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BoolRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_UGT, a.ast, b.ast), a.ctx)
+    return BoolRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_UGT, a.ast, b.ast), a.ctx)
 
 
 def SLE(a, b):
@@ -4925,7 +4886,7 @@ def SLE(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BoolRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_SLE, a.ast, b.ast), a.ctx)
+    return BoolRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_SLE, a.ast, b.ast), a.ctx)
 
 
 def SLT(a, b):
@@ -4939,7 +4900,7 @@ def SLT(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BoolRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_SLT, a.ast, b.ast), a.ctx)
+    return BoolRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_SLT, a.ast, b.ast), a.ctx)
 
 
 def SGE(a, b):
@@ -4953,7 +4914,7 @@ def SGE(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BoolRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_SGE, a.ast, b.ast), a.ctx)
+    return BoolRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_SGE, a.ast, b.ast), a.ctx)
 
 
 def SGT(a, b):
@@ -4967,7 +4928,7 @@ def SGT(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BoolRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_SGT, a.ast, b.ast), a.ctx)
+    return BoolRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_SGT, a.ast, b.ast), a.ctx)
 
 
 def UDiv(a, b):
@@ -4988,7 +4949,7 @@ def UDiv(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BitVecRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_UDIV, a.ast, b.ast), a.ctx)
+    return BitVecRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_UDIV, a.ast, b.ast), a.ctx)
 
 
 def URem(a, b):
@@ -5009,7 +4970,7 @@ def URem(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BitVecRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_UREM, a.ast, b.ast), a.ctx)
+    return BitVecRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_UREM, a.ast, b.ast), a.ctx)
 
 
 def SDiv(a, b):
@@ -5056,7 +5017,7 @@ def SRem(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BitVecRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_SREM, a.ast, b.ast), a.ctx)
+    return BitVecRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_SREM, a.ast, b.ast), a.ctx)
 
 
 def LShR(a, b):
@@ -5088,7 +5049,7 @@ def LShR(a, b):
     """
     _check_bv_args(a, b)
     a, b = _coerce_exprs(a, b)
-    return BitVecRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_LSHR, a.ast, b.ast), a.ctx)
+    return BitVecRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_LSHR, a.ast, b.ast), a.ctx)
 
 
 def _check_rotate_args(a, b):
@@ -5109,7 +5070,7 @@ def RotateLeft(a, b):
     >>> simplify(RotateLeft(a, 16))
     a
     """
-    s = a.ctx.solver
+    s = a.ctx.tm
     _check_rotate_args(a, b)
     return BitVecRef(s.mkTerm(s.mkOp(Kind.BITVECTOR_ROTATE_LEFT, b), a.ast), a.ctx)
 
@@ -5125,7 +5086,7 @@ def RotateRight(a, b):
     >>> simplify(RotateRight(a, 16))
     a
     """
-    s = a.ctx.solver
+    s = a.ctx.tm
     _check_rotate_args(a, b)
     return BitVecRef(s.mkTerm(s.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, b), a.ast), a.ctx)
 
@@ -5157,7 +5118,7 @@ def SignExt(n, a):
     if debugging():
         _assert(_is_int(n), "First argument must be an integer")
         _assert(is_bv(a), "Second argument must be an SMT bit-vector expression")
-    s = a.ctx.solver
+    s = a.ctx.tm
     return BitVecRef(s.mkTerm(s.mkOp(Kind.BITVECTOR_SIGN_EXTEND, n), a.ast), a.ctx)
 
 
@@ -5186,7 +5147,7 @@ def ZeroExt(n, a):
     if debugging():
         _assert(_is_int(n), "First argument must be an integer")
         _assert(is_bv(a), "Second argument must be an SMT bit-vector expression")
-    s = a.ctx.solver
+    s = a.ctx.tm
     return BitVecRef(s.mkTerm(s.mkOp(Kind.BITVECTOR_ZERO_EXTEND, n), a.ast), a.ctx)
 
 
@@ -5212,7 +5173,7 @@ def RepeatBitVec(n, a):
         _assert(_is_int(n), "First argument must be an integer")
         _assert(is_bv(a), "Second argument must be an SMT bit-vector expression")
     return BitVecRef(
-        a.ctx.solver.mkTerm(a.ctx.solver.mkOp(Kind.BITVECTOR_REPEAT, n), a.ast), a.ctx
+        a.ctx.tm.mkTerm(a.ctx.tm.mkOp(Kind.BITVECTOR_REPEAT, n), a.ast), a.ctx
     )
 
 
@@ -5225,7 +5186,7 @@ def BVRedAnd(a):
     """
     if debugging():
         _assert(is_bv(a), "First argument must be an SMT bit-vector expression")
-    return BitVecRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_REDAND, a.ast), a.ctx)
+    return BitVecRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_REDAND, a.ast), a.ctx)
 
 
 def BVRedOr(a):
@@ -5237,7 +5198,7 @@ def BVRedOr(a):
     """
     if debugging():
         _assert(is_bv(a), "First argument must be an SMT bit-vector expression")
-    return BitVecRef(a.ctx.solver.mkTerm(Kind.BITVECTOR_REDOR, a.ast), a.ctx)
+    return BitVecRef(a.ctx.tm.mkTerm(Kind.BITVECTOR_REDOR, a.ast), a.ctx)
 
 
 def BVAdd(*args):
@@ -5409,7 +5370,7 @@ def __getitem__(self, arg):
         """
         arg = self.domain().cast(arg)
         return _to_expr_ref(
-            self.ctx.solver.mkTerm(Kind.SELECT, self.ast, arg.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.SELECT, self.ast, arg.ast), self.ctx
         )
 
     def arg(self, idx):
@@ -5519,7 +5480,7 @@ def ArraySort(*sig):
             _assert(is_sort(s), "SMT sort expected")
     ctx = d.ctx
     if len(sig) == 2:
-        return ArraySortRef(ctx.solver.mkArraySort(d.ast, r.ast), ctx)
+        return ArraySortRef(ctx.tm.mkArraySort(d.ast, r.ast), ctx)
     else:
         unimplemented("multi-domain array")
 
@@ -5534,7 +5495,7 @@ def Array(name, dom, rng):
     a[0]
     """
     ctx = dom.ctx
-    s = ctx.solver.mkArraySort(dom.ast, rng.ast)
+    s = ctx.tm.mkArraySort(dom.ast, rng.ast)
     e = ctx.get_var(name, _to_sort_ref(s, ctx))
     return ArrayRef(e, ctx)
 
@@ -5576,7 +5537,7 @@ def Store(a, i, v):
     i = a.sort().domain().cast(i)
     v = a.sort().range().cast(v)
     ctx = a.ctx
-    return _to_expr_ref(ctx.solver.mkTerm(Kind.STORE, a.ast, i.ast, v.ast), ctx)
+    return _to_expr_ref(ctx.tm.mkTerm(Kind.STORE, a.ast, i.ast, v.ast), ctx)
 
 
 def Select(a, i):
@@ -5631,7 +5592,7 @@ def ConstArray(dom, v):
     if not is_expr(v):
         v = _py2expr(v, ctx)
     sort = ArraySort(dom, v.sort())
-    return ArrayRef(ctx.solver.mkConstArray(sort.ast, v.ast), ctx)
+    return ArrayRef(ctx.tm.mkConstArray(sort.ast, v.ast), ctx)
 
 
 def is_select(a):
@@ -5746,7 +5707,7 @@ def __getitem__(self, arg):
         """
         arg = self.domain().cast(arg)
         return _to_expr_ref(
-            self.ctx.solver.mkTerm(Kind.SET_MEMBER, arg.ast, self.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.SET_MEMBER, arg.ast, self.ast), self.ctx
         )
 
     def default(self):
@@ -5759,7 +5720,7 @@ def default(self):
         False
 
         """
-        return BoolRef(self.ctx.solver.mkFalse(), self.ctx)
+        return BoolRef(self.ctx.tm.mkFalse(), self.ctx)
 
     def __and__(self, other):
         """Intersection
@@ -5788,7 +5749,7 @@ def SetSort(s):
     """Create a set sort over element sort s"""
     ctx = s.ctx
     instance_check(s, SortRef)
-    sort = ctx.solver.mkSetSort(s.ast)
+    sort = ctx.tm.mkSetSort(s.ast)
     return SetSortRef(sort, ctx)
 
 
@@ -5808,7 +5769,7 @@ def EmptySet(s):
     """
     ctx = s.ctx
     sort = SetSort(s)
-    return SetRef(ctx.solver.mkEmptySet(sort.ast), ctx)
+    return SetRef(ctx.tm.mkEmptySet(sort.ast), ctx)
 
 
 def FullSet(s):
@@ -5819,7 +5780,7 @@ def FullSet(s):
     """
     ctx = s.ctx
     sort = SetSort(s)
-    return SetRef(ctx.solver.mkUniverseSet(sort.ast), ctx)
+    return SetRef(ctx.tm.mkUniverseSet(sort.ast), ctx)
 
 
 def SetUnion(*args):
@@ -5832,7 +5793,7 @@ def SetUnion(*args):
     """
     args = _get_args(args)
     ctx = _ctx_from_ast_arg_list(args)
-    return SetRef(ctx.solver.mkTerm(Kind.SET_UNION, *[a.ast for a in args]), ctx)
+    return SetRef(ctx.tm.mkTerm(Kind.SET_UNION, *[a.ast for a in args]), ctx)
 
 
 def SetIntersect(*args):
@@ -5845,7 +5806,7 @@ def SetIntersect(*args):
     """
     args = _get_args(args)
     ctx = _ctx_from_ast_arg_list(args)
-    return SetRef(ctx.solver.mkTerm(Kind.SET_INTER, *[a.ast for a in args]), ctx)
+    return SetRef(ctx.tm.mkTerm(Kind.SET_INTER, *[a.ast for a in args]), ctx)
 
 
 def SetAdd(s, e):
@@ -5859,7 +5820,7 @@ def SetAdd(s, e):
     """
     ctx = _ctx_from_ast_arg_list([s, e])
     e = _py2expr(e, ctx)
-    return SetRef(ctx.solver.mkTerm(Kind.SET_INSERT, e.ast, s.ast), ctx, True)
+    return SetRef(ctx.tm.mkTerm(Kind.SET_INSERT, e.ast, s.ast), ctx, True)
 
 
 def SetDel(s, e):
@@ -5880,7 +5841,7 @@ def SetComplement(s):
     SetComplement(a)
     """
     ctx = s.ctx
-    return ArrayRef(ctx.solver.mkTerm(Kind.SET_COMPLEMENT, s.ast), ctx)
+    return ArrayRef(ctx.tm.mkTerm(Kind.SET_COMPLEMENT, s.ast), ctx)
 
 
 def Singleton(s):
@@ -5891,7 +5852,7 @@ def Singleton(s):
     """
     s = _py2expr(s)
     ctx = s.ctx
-    return SetRef(ctx.solver.mkTerm(Kind.SET_SINGLETON, s.ast), ctx)
+    return SetRef(ctx.tm.mkTerm(Kind.SET_SINGLETON, s.ast), ctx)
 
 
 def SetDifference(a, b):
@@ -5903,7 +5864,7 @@ def SetDifference(a, b):
     SetDifference(a, b)
     """
     ctx = _ctx_from_ast_arg_list([a, b])
-    return SetRef(ctx.solver.mkTerm(Kind.SET_MINUS, a.ast, b.ast), ctx)
+    return SetRef(ctx.tm.mkTerm(Kind.SET_MINUS, a.ast, b.ast), ctx)
 
 
 def SetMinus(a, b):
@@ -5926,7 +5887,7 @@ def IsMember(e, s):
     """
     ctx = _ctx_from_ast_arg_list([s, e])
     arg = s.domain().cast(e)
-    return BoolRef(ctx.solver.mkTerm(Kind.SET_MEMBER, arg.ast, s.ast), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.SET_MEMBER, arg.ast, s.ast), ctx)
 
 
 def IsSubset(a, b):
@@ -5938,7 +5899,7 @@ def IsSubset(a, b):
     IsSubset(a, b)
     """
     ctx = _ctx_from_ast_arg_list([a, b])
-    return BoolRef(ctx.solver.mkTerm(Kind.SET_SUBSET, a.ast, b.ast), ctx)
+    return BoolRef(ctx.tm.mkTerm(Kind.SET_SUBSET, a.ast, b.ast), ctx)
 
 
 #########################################
@@ -6012,7 +5973,7 @@ class Solver(object):
     * etc."""
 
     def __init__(self, ctx=None, logFile=None):
-        # ignore ctx (the paramter is kept for z3 compatibility)
+        self.ctx = _get_ctx(ctx)
         self.solver = None
         self.logic = None
         self.initFromLogic()
@@ -6024,7 +5985,7 @@ def __init__(self, ctx=None, logFile=None):
 
     def initFromLogic(self):
         """Create the base-API solver from the logic"""
-        self.solver = pc.Solver()
+        self.solver = pc.Solver(self.ctx.tm)
         if self.logic is not None:
             self.solver.setLogic(self.logic)
         self.solver.setOption("produce-models", "true")
@@ -6143,7 +6104,7 @@ def assert_exprs(self, *args):
         [x > 0, x < 2]
         """
         args = _get_args(args)
-        s = BoolSort()
+        s = BoolSort(self.ctx)
         for arg in args:
             arg = s.cast(arg)
             self.assertions_[-1].append(arg)
@@ -6406,7 +6367,7 @@ def unsat_core(self):
         sat
         """
         core = self.solver.getUnsatCore()
-        return [_to_expr_ref(c, Context(self)) for c in core]
+        return [_to_expr_ref(c, self.ctx) for c in core]
 
 
 def SolverFor(logic, ctx=None, logFile=None):
@@ -6718,7 +6679,7 @@ def eval(self, t, model_completion=False):
         >>> m.eval(x == 1)
         True
         """
-        return _to_expr_ref(self.solver.solver.getValue(t.ast), Context(self.solver))
+        return _to_expr_ref(self.solver.solver.getValue(t.ast), self.solver.ctx)
 
     def evaluate(self, t, model_completion=False):
         """Alias for `eval`.
@@ -6879,7 +6840,7 @@ def getResult(self):
         >>> p.getResult()
         Not(And(a + 2 == 0, a == 0))
         """
-        return _to_expr_ref(self.proof.getResult(), Context(self.solver))
+        return _to_expr_ref(self.proof.getResult(), self.solver.ctx)
 
     def getChildren(self):
         """Returns the premises, i.e., proofs themselvels, of the root step of
@@ -6918,7 +6879,7 @@ def getArguments(self):
         [a + 2 == 0, a == 0]
         """
         args = self.proof.getArguments()
-        return [_to_expr_ref(a, Context(self.solver)) for a in args]
+        return [_to_expr_ref(a, self.solver.ctx) for a in args]
 
 
 def simplify(a):
@@ -6932,7 +6893,7 @@ def simplify(a):
     if debugging():
         _assert(is_expr(a), "SMT expression expected")
     instance_check(a, ExprRef)
-    return _to_expr_ref(a.ctx.solver.simplify(a.ast), a.ctx)
+    return _to_expr_ref(Solver(ctx=a.ctx).solver.simplify(a.ast), a.ctx)
 
 
 #########################################
@@ -7006,7 +6967,7 @@ def cast(self, val):
 def Float16(ctx=None):
     """Floating-point 16-bit (half) sort."""
     ctx = _get_ctx(ctx)
-    return FPSortRef(ctx.solver.mkFloatingPointSort(5, 11), ctx)
+    return FPSortRef(ctx.tm.mkFloatingPointSort(5, 11), ctx)
 
 
 def FloatHalf(ctx=None):
@@ -7017,7 +6978,7 @@ def FloatHalf(ctx=None):
 def Float32(ctx=None):
     """Floating-point 32-bit (single) sort."""
     ctx = _get_ctx(ctx)
-    return FPSortRef(ctx.solver.mkFloatingPointSort(8, 24), ctx)
+    return FPSortRef(ctx.tm.mkFloatingPointSort(8, 24), ctx)
 
 
 def FloatSingle(ctx=None):
@@ -7028,7 +6989,7 @@ def FloatSingle(ctx=None):
 def Float64(ctx=None):
     """Floating-point 64-bit (double) sort."""
     ctx = _get_ctx(ctx)
-    return FPSortRef(ctx.solver.mkFloatingPointSort(11, 53), ctx)
+    return FPSortRef(ctx.tm.mkFloatingPointSort(11, 53), ctx)
 
 
 def FloatDouble(ctx=None):
@@ -7039,7 +7000,7 @@ def FloatDouble(ctx=None):
 def Float128(ctx=None):
     """Floating-point 128-bit (quadruple) sort."""
     ctx = _get_ctx(ctx)
-    return FPSortRef(ctx.solver.mkFloatingPointSort(15, 113), ctx)
+    return FPSortRef(ctx.tm.mkFloatingPointSort(15, 113), ctx)
 
 
 def FloatQuadruple(ctx=None):
@@ -7267,7 +7228,7 @@ def RoundNearestTiesToEven(ctx=None):
     """
     ctx = _get_ctx(ctx)
     return FPRMRef(
-        ctx.solver.mkRoundingMode(pc.RoundingMode.ROUND_NEAREST_TIES_TO_EVEN), ctx
+        ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_NEAREST_TIES_TO_EVEN), ctx
     )
 
 
@@ -7298,7 +7259,7 @@ def RoundNearestTiesToAway(ctx=None):
     """
     ctx = _get_ctx(ctx)
     return FPRMRef(
-        ctx.solver.mkRoundingMode(pc.RoundingMode.ROUND_NEAREST_TIES_TO_AWAY), ctx
+        ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_NEAREST_TIES_TO_AWAY), ctx
     )
 
 
@@ -7328,9 +7289,7 @@ def RoundTowardPositive(ctx=None):
     fpMul(RTP(), x, y)
     """
     ctx = _get_ctx(ctx)
-    return FPRMRef(
-        ctx.solver.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_POSITIVE), ctx
-    )
+    return FPRMRef(ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_POSITIVE), ctx)
 
 
 def RTP(ctx=None):
@@ -7359,9 +7318,7 @@ def RoundTowardNegative(ctx=None):
     fpMul(RTN(), x, y)
     """
     ctx = _get_ctx(ctx)
-    return FPRMRef(
-        ctx.solver.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_NEGATIVE), ctx
-    )
+    return FPRMRef(ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_NEGATIVE), ctx)
 
 
 def RTN(ctx=None):
@@ -7390,7 +7347,7 @@ def RoundTowardZero(ctx=None):
     x * y
     """
     ctx = _get_ctx(ctx)
-    return FPRMRef(ctx.solver.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_ZERO), ctx)
+    return FPRMRef(ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_ZERO), ctx)
 
 
 def RTZ(ctx=None):
@@ -7438,7 +7395,7 @@ def get_default_rounding_mode(ctx=None):
             isinstance(_dflt_rounding_mode, pc.RoundingMode), "illegal rounding mode"
         )
     ctx = _get_ctx(ctx)
-    return FPRMRef(ctx.solver.mkRoundingMode(_dflt_rounding_mode), ctx)
+    return FPRMRef(ctx.tm.mkRoundingMode(_dflt_rounding_mode), ctx)
 
 
 def set_default_rounding_mode(rm, ctx=None):
@@ -7655,7 +7612,7 @@ def FPSort(ebits, sbits, ctx=None):
     True
     """
     ctx = _get_ctx(ctx)
-    return FPSortRef(ctx.solver.mkFloatingPointSort(ebits, sbits), ctx)
+    return FPSortRef(ctx.tm.mkFloatingPointSort(ebits, sbits), ctx)
 
 
 def _to_float_str(val, exp=0):
@@ -7716,7 +7673,7 @@ def fpNaN(s):
     >>> set_fpa_pretty(pb)
     """
     _assert(isinstance(s, FPSortRef), "sort mismatch")
-    return FPNumRef(s.ctx.solver.mkFloatingPointNaN(s.ebits(), s.sbits()), s.ctx)
+    return FPNumRef(s.ctx.tm.mkFloatingPointNaN(s.ebits(), s.sbits()), s.ctx)
 
 
 def fpPlusInfinity(s):
@@ -7733,13 +7690,13 @@ def fpPlusInfinity(s):
     >>> set_fpa_pretty(pb)
     """
     _assert(isinstance(s, FPSortRef), "sort mismatch")
-    return FPNumRef(s.ctx.solver.mkFloatingPointPosInf(s.ebits(), s.sbits()), s.ctx)
+    return FPNumRef(s.ctx.tm.mkFloatingPointPosInf(s.ebits(), s.sbits()), s.ctx)
 
 
 def fpMinusInfinity(s):
     """Create a SMT floating-point -oo term."""
     _assert(isinstance(s, FPSortRef), "sort mismatch")
-    return FPNumRef(s.ctx.solver.mkFloatingPointNegInf(s.ebits(), s.sbits()), s.ctx)
+    return FPNumRef(s.ctx.tm.mkFloatingPointNegInf(s.ebits(), s.sbits()), s.ctx)
 
 
 def fpInfinity(s, negative):
@@ -7752,13 +7709,13 @@ def fpInfinity(s, negative):
 def fpPlusZero(s):
     """Create a SMT floating-point +0.0 term."""
     _assert(isinstance(s, FPSortRef), "sort mismatch")
-    return FPNumRef(s.ctx.solver.mkFloatingPointPosZero(s.ebits(), s.sbits()), s.ctx)
+    return FPNumRef(s.ctx.tm.mkFloatingPointPosZero(s.ebits(), s.sbits()), s.ctx)
 
 
 def fpMinusZero(s):
     """Create a SMT floating-point -0.0 term."""
     _assert(isinstance(s, FPSortRef), "sort mismatch")
-    return FPNumRef(s.ctx.solver.mkFloatingPointNegZero(s.ebits(), s.sbits()), s.ctx)
+    return FPNumRef(s.ctx.tm.mkFloatingPointNegZero(s.ebits(), s.sbits()), s.ctx)
 
 
 def fpZero(s, negative):
@@ -7814,12 +7771,12 @@ def FPVal(val, exp=None, fps=None, ctx=None):
         bv_str = bin(ctypes.c_uint64.from_buffer(ctypes.c_double(val)).value)[2:]
         bv_str = "0" * (64 - len(bv_str)) + bv_str
         dub = Float64(ctx)
-        bv = ctx.solver.mkBitVector(len(bv_str), bv_str, 2)
-        fp64 = ctx.solver.mkFloatingPoint(dub.ebits(), dub.sbits(), bv)
-        fp_to_fp_op = ctx.solver.mkOp(
+        bv = ctx.tm.mkBitVector(len(bv_str), bv_str, 2)
+        fp64 = ctx.tm.mkFloatingPoint(dub.ebits(), dub.sbits(), bv)
+        fp_to_fp_op = ctx.tm.mkOp(
             Kind.FLOATINGPOINT_TO_FP_FROM_FP, fps.ebits(), fps.sbits()
         )
-        fp = ctx.solver.mkTerm(fp_to_fp_op, _dflt_rm(ctx).ast, fp64)
+        fp = ctx.tm.mkTerm(fp_to_fp_op, _dflt_rm(ctx).ast, fp64)
         presimp = FPNumRef(fp, ctx)
         post = simplify(presimp)
         return post
@@ -7892,7 +7849,7 @@ def fpAbs(a, ctx=None):
     """
     ctx = _get_ctx(ctx)
     [a] = _coerce_fp_expr_list([a], ctx)
-    return FPRef(ctx.solver.mkTerm(Kind.FLOATINGPOINT_ABS, a.ast), ctx)
+    return FPRef(ctx.tm.mkTerm(Kind.FLOATINGPOINT_ABS, a.ast), ctx)
 
 
 def fpNeg(a, ctx=None):
@@ -7908,7 +7865,7 @@ def fpNeg(a, ctx=None):
     """
     ctx = _get_ctx(ctx)
     [a] = _coerce_fp_expr_list([a], ctx)
-    return FPRef(ctx.solver.mkTerm(Kind.FLOATINGPOINT_NEG, a.ast), ctx)
+    return FPRef(ctx.tm.mkTerm(Kind.FLOATINGPOINT_NEG, a.ast), ctx)
 
 
 def _mk_fp_unary(kind, rm, a, ctx):
@@ -7920,7 +7877,7 @@ def _mk_fp_unary(kind, rm, a, ctx):
             "First argument must be a SMT floating-point rounding mode expression",
         )
         _assert(is_fp(a), "Second argument must be a SMT floating-point expression")
-    return FPRef(ctx.solver.mkTerm(kind, rm.as_ast(), a.as_ast()), ctx)
+    return FPRef(ctx.tm.mkTerm(kind, rm.as_ast(), a.as_ast()), ctx)
 
 
 def _mk_fp_unary_pred(kind, a, ctx):
@@ -7928,7 +7885,7 @@ def _mk_fp_unary_pred(kind, a, ctx):
     [a] = _coerce_fp_expr_list([a], ctx)
     if debugging():
         _assert(is_fp(a), "First argument must be a SMT floating-point expression")
-    return BoolRef(ctx.solver.mkTerm(kind, a.as_ast()), ctx)
+    return BoolRef(ctx.tm.mkTerm(kind, a.as_ast()), ctx)
 
 
 def _mk_fp_bin(kind, rm, a, b, ctx):
@@ -7943,7 +7900,7 @@ def _mk_fp_bin(kind, rm, a, b, ctx):
             is_fp(a) or is_fp(b),
             "Second or third argument must be a SMT floating-point expression",
         )
-    return FPRef(ctx.solver.mkTerm(kind, rm.as_ast(), a.as_ast(), b.as_ast()), ctx)
+    return FPRef(ctx.tm.mkTerm(kind, rm.as_ast(), a.as_ast(), b.as_ast()), ctx)
 
 
 def _mk_fp_bin_norm(kind, a, b, ctx):
@@ -7954,7 +7911,7 @@ def _mk_fp_bin_norm(kind, a, b, ctx):
             is_fp(a) or is_fp(b),
             "First or second argument must be a SMT floating-point expression",
         )
-    return FPRef(ctx.solver.mkTerm(kind, a.as_ast(), b.as_ast()), ctx)
+    return FPRef(ctx.tm.mkTerm(kind, a.as_ast(), b.as_ast()), ctx)
 
 
 def _mk_fp_bin_pred(kind, a, b, ctx):
@@ -7965,7 +7922,7 @@ def _mk_fp_bin_pred(kind, a, b, ctx):
             is_fp(a) or is_fp(b),
             "First or second argument must be a SMT floating-point expression",
         )
-    return BoolRef(ctx.solver.mkTerm(kind, a.as_ast(), b.as_ast()), ctx)
+    return BoolRef(ctx.tm.mkTerm(kind, a.as_ast(), b.as_ast()), ctx)
 
 
 def _mk_fp_tern(kind, rm, a, b, c, ctx):
@@ -7981,7 +7938,7 @@ def _mk_fp_tern(kind, rm, a, b, c, ctx):
             "Second, third or fourth argument must be a SMT floating-point expression",
         )
     return FPRef(
-        ctx.solver.mkTerm(kind, rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx
+        ctx.tm.mkTerm(kind, rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx
     )
 
 
@@ -8260,9 +8217,7 @@ def fpFP(sgn, exp, sig, ctx=None):
     _assert(sgn.sort().size() == 1, "sort mismatch")
     ctx = _get_ctx(ctx)
     _assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
-    bv = BitVecRef(
-        ctx.solver.mkTerm(Kind.BITVECTOR_CONCAT, sgn.ast, exp.ast, sig.ast), ctx
-    )
+    bv = BitVecRef(ctx.tm.mkTerm(Kind.BITVECTOR_CONCAT, sgn.ast, exp.ast, sig.ast), ctx)
     sort = FPSort(exp.size(), sig.size() + 1)
     return fpBVToFP(bv, sort)
 
@@ -8319,10 +8274,10 @@ def fpBVToFP(v, sort, ctx=None):
     _assert(is_bv(v), "First argument must be a SMT bit-vector expression")
     _assert(is_fp_sort(sort), "Second argument must be a SMT floating-point sort.")
     ctx = _get_ctx(ctx)
-    to_fp_op = ctx.solver.mkOp(
+    to_fp_op = ctx.tm.mkOp(
         Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, sort.ebits(), sort.sbits()
     )
-    return FPRef(ctx.solver.mkTerm(to_fp_op, v.ast), ctx)
+    return FPRef(ctx.tm.mkTerm(to_fp_op, v.ast), ctx)
 
 
 def fpFPToFP(rm, v, sort, ctx=None):
@@ -8345,10 +8300,8 @@ def fpFPToFP(rm, v, sort, ctx=None):
     _assert(is_fp(v), "Second argument must be a SMT floating-point expression.")
     _assert(is_fp_sort(sort), "Third argument must be a SMT floating-point sort.")
     ctx = _get_ctx(ctx)
-    to_fp_op = ctx.solver.mkOp(
-        Kind.FLOATINGPOINT_TO_FP_FROM_FP, sort.ebits(), sort.sbits()
-    )
-    return FPRef(ctx.solver.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
+    to_fp_op = ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_FP_FROM_FP, sort.ebits(), sort.sbits())
+    return FPRef(ctx.tm.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
 
 
 def fpRealToFP(rm, v, sort, ctx=None):
@@ -8369,10 +8322,10 @@ def fpRealToFP(rm, v, sort, ctx=None):
     _assert(is_real(v), "Second argument must be a SMT expression or real sort.")
     _assert(is_fp_sort(sort), "Third argument must be a SMT floating-point sort.")
     ctx = _get_ctx(ctx)
-    to_fp_op = ctx.solver.mkOp(
+    to_fp_op = ctx.tm.mkOp(
         Kind.FLOATINGPOINT_TO_FP_FROM_REAL, sort.ebits(), sort.sbits()
     )
-    return FPRef(ctx.solver.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
+    return FPRef(ctx.tm.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
 
 
 def fpSignedToFP(rm, v, sort, ctx=None):
@@ -8393,10 +8346,10 @@ def fpSignedToFP(rm, v, sort, ctx=None):
     _assert(is_bv(v), "Second argument must be a SMT bit-vector expression")
     _assert(is_fp_sort(sort), "Third argument must be a SMT floating-point sort.")
     ctx = _get_ctx(ctx)
-    to_fp_op = ctx.solver.mkOp(
+    to_fp_op = ctx.tm.mkOp(
         Kind.FLOATINGPOINT_TO_FP_FROM_SBV, sort.ebits(), sort.sbits()
     )
-    return FPRef(ctx.solver.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
+    return FPRef(ctx.tm.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
 
 
 def fpUnsignedToFP(rm, v, sort, ctx=None):
@@ -8417,10 +8370,10 @@ def fpUnsignedToFP(rm, v, sort, ctx=None):
     _assert(is_bv(v), "Second argument must be a SMT bit-vector expression")
     _assert(is_fp_sort(sort), "Third argument must be a SMT floating-point sort.")
     ctx = _get_ctx(ctx)
-    to_fp_op = ctx.solver.mkOp(
+    to_fp_op = ctx.tm.mkOp(
         Kind.FLOATINGPOINT_TO_FP_FROM_UBV, sort.ebits(), sort.sbits()
     )
-    return FPRef(ctx.solver.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
+    return FPRef(ctx.tm.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
 
 
 def fpToFPUnsigned(rm, x, s, ctx=None):
@@ -8433,8 +8386,8 @@ def fpToFPUnsigned(rm, x, s, ctx=None):
         _assert(is_bv(x), "Second argument must be a SMT bit-vector expression")
         _assert(is_fp_sort(s), "Third argument must be SMT floating-point sort")
     ctx = _get_ctx(ctx)
-    to_fp_op = ctx.solver.mkOp(Kind.FLOATINGPOINT_TO_FP_FROM_UBV, s.ebits(), s.sbits())
-    return FPRef(ctx.solver.mkTerm(to_fp_op, rm.ast, x.ast), ctx)
+    to_fp_op = ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_FP_FROM_UBV, s.ebits(), s.sbits())
+    return FPRef(ctx.tm.mkTerm(to_fp_op, rm.ast, x.ast), ctx)
 
 
 def fpToSBV(rm, x, s, ctx=None):
@@ -8460,9 +8413,7 @@ def fpToSBV(rm, x, s, ctx=None):
         _assert(is_bv_sort(s), "Third argument must be SMT bit-vector sort")
     ctx = _get_ctx(ctx)
     return BitVecRef(
-        ctx.solver.mkTerm(
-            ctx.solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, s.size()), rm.ast, x.ast
-        ),
+        ctx.tm.mkTerm(ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_SBV, s.size()), rm.ast, x.ast),
         ctx,
     )
 
@@ -8490,9 +8441,7 @@ def fpToUBV(rm, x, s, ctx=None):
         _assert(is_bv_sort(s), "Third argument must be SMT bit-vector sort")
     ctx = _get_ctx(ctx)
     return BitVecRef(
-        ctx.solver.mkTerm(
-            ctx.solver.mkOp(Kind.FLOATINGPOINT_TO_UBV, s.size()), rm.ast, x.ast
-        ),
+        ctx.tm.mkTerm(ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_UBV, s.size()), rm.ast, x.ast),
         ctx,
     )
 
@@ -8514,7 +8463,7 @@ def fpToReal(x, ctx=None):
     if debugging():
         _assert(is_fp(x), "First argument must be a SMT floating-point expression")
     ctx = _get_ctx(ctx)
-    return ArithRef(ctx.solver.mkTerm(Kind.FLOATINGPOINT_TO_REAL, x.ast), ctx)
+    return ArithRef(ctx.tm.mkTerm(Kind.FLOATINGPOINT_TO_REAL, x.ast), ctx)
 
 
 #########################################
@@ -8666,7 +8615,7 @@ def CreateDatatypes(*ds):
         )
         _assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
     ctx = ds[0].ctx
-    s = ctx.solver
+    s = ctx.tm
     num = len(ds)
     uninterp_sorts = {}
     for d in ds:
@@ -9195,11 +9144,11 @@ def _mk_quant(vs, body, kind):
     if not isinstance(vs, list):
         vs = [vs]
     c = vs[0].ctx
-    s = c.solver
+    tm = c.tm
     consts = [v.ast for v in vs]
-    vars_ = [s.mkVar(v.sort().ast, str(v)) for v in vs]
+    vars_ = [tm.mkVar(v.sort().ast, str(v)) for v in vs]
     subbed_body = body.ast.substitute(consts, vars_)
-    ast = s.mkTerm(kind, s.mkTerm(Kind.VARIABLE_LIST, *vars_), subbed_body)
+    ast = tm.mkTerm(kind, tm.mkTerm(Kind.VARIABLE_LIST, *vars_), subbed_body)
     return QuantifierRef(ast, c)
 
 
@@ -9394,7 +9343,7 @@ def __neg__(self):
         no solution
         """
         return FiniteFieldRef(
-            self.ctx.solver.mkTerm(Kind.FINITE_FIELD_NEG, self.ast), self.ctx
+            self.ctx.tm.mkTerm(Kind.FINITE_FIELD_NEG, self.ast), self.ctx
         )
 
 
@@ -9472,7 +9421,7 @@ def FiniteFieldSort(sz, ctx=None):
     True
     """
     ctx = _get_ctx(ctx)
-    return FiniteFieldSortRef(ctx.solver.mkFiniteFieldSort(sz), ctx)
+    return FiniteFieldSortRef(ctx.tm.mkFiniteFieldSort(sz), ctx)
 
 
 def FiniteFieldVal(val, ff, ctx=None):
@@ -9496,8 +9445,8 @@ def FiniteFieldVal(val, ff, ctx=None):
         if debugging():
             _assert(isinstance(ff, int), "non-integer in FiniteFieldVal")
         ctx = _get_ctx(ctx)
-        sort = ctx.solver.mkFiniteFieldSort(ff)
-    return FiniteFieldNumRef(ctx.solver.mkFiniteFieldElem(val, sort), ctx)
+        sort = ctx.tm.mkFiniteFieldSort(ff)
+    return FiniteFieldNumRef(ctx.tm.mkFiniteFieldElem(val, sort), ctx)
 
 
 def FiniteFieldElem(name, ff, ctx=None):
@@ -9579,8 +9528,8 @@ def FFSub(a, b):
     """
     a, b = _coerce_exprs(a, b)
     ctx = a.ctx
-    neg_b = ctx.solver.mkTerm(Kind.FINITE_FIELD_NEG, b.ast)
-    return FiniteFieldRef(ctx.solver.mkTerm(Kind.FINITE_FIELD_ADD, a.ast, neg_b), ctx)
+    neg_b = ctx.tm.mkTerm(Kind.FINITE_FIELD_NEG, b.ast)
+    return FiniteFieldRef(ctx.tm.mkTerm(Kind.FINITE_FIELD_ADD, a.ast, neg_b), ctx)
 
 
 def FFNeg(a):
diff --git a/cvc5_pythonic_api/cvc5_pythonic_printer.py b/cvc5_pythonic_api/cvc5_pythonic_printer.py
index fab4f0c..8e3de6b 100644
--- a/cvc5_pythonic_api/cvc5_pythonic_printer.py
+++ b/cvc5_pythonic_api/cvc5_pythonic_printer.py
@@ -84,6 +84,7 @@ def _assert(cond, msg):
     Kind.BITVECTOR_CONCAT: "Concat",
     Kind.BITVECTOR_EXTRACT: "Extract",
     Kind.BITVECTOR_TO_NAT: "BV2Int",
+    Kind.BITVECTOR_UBV_TO_INT: "BV2Int",
     Kind.FINITE_FIELD_ADD: "+",
     Kind.FINITE_FIELD_MULT: "*",
     Kind.FINITE_FIELD_NEG: "-",