diff --git a/requirements.txt b/requirements.txt
index 060f196..a79a35a 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -1,8 +1,6 @@
 # The lower bounds are the oldest releases that pass the tests on Python 3.11; CI tests them next to the newest
 # releases.
 numpy>=1.23.2
-# 0.9.0 fails to import on Python 3.12+ (it bundles an old six), 0.9.5 crashes in the pysmt mode
-PySMT>=0.9.6
 # 2.7 fails with Gurobi through PuLP; 4.0 removed PULP_CBC_CMD
 PuLP>=2.8.0,<4
 # 12.0 added the nonlinear expressions of the gurobi mode (2 ** x, division by a variable), but the size-limited
diff --git a/src/complex/classic.py b/src/complex/classic.py
index 498cc91..258496d 100644
--- a/src/complex/classic.py
+++ b/src/complex/classic.py
@@ -6,7 +6,6 @@
 """
 
 import numpy as np
-from pysmt.shortcuts import Plus, Minus, Times, Equals, And, Real
 
 class Complex:
     def __init__(self, a=None, b=None, name=None, generator=None, bound=None):
diff --git a/src/complex/fivetuple.py b/src/complex/fivetuple.py
index d543be3..f6f116a 100644
--- a/src/complex/fivetuple.py
+++ b/src/complex/fivetuple.py
@@ -6,7 +6,6 @@
 """
 
 import numpy as np
-from pysmt.shortcuts import Plus, Minus, Times, Equals, And, Real
 from .classic import Complex
 
 class FiveTuple:
diff --git a/src/generator.py b/src/generator.py
index 332f155..8492130 100644
--- a/src/generator.py
+++ b/src/generator.py
@@ -5,17 +5,11 @@
 @brief: Generator class, responsible for generating the SMT/MILP/Gurobi formulae for synthesis
 """
 
-from ast import Return
-from pysmt.smtlib.parser import SmtLibParser
-from pysmt.shortcuts import Real, Int, Bool, Symbol, And, Div, Plus, GT, LT, get_env, Int, Or, Not, Implies, GE, LE, Ite, Times, Minus, Plus
-from pysmt.shortcuts import Equals as pysmtEquals
-from pysmt.typing import REAL, INT, BOOL
 from pulp import *
 from gates import self_adjoints, gate_to_qubits
 import gurobipy as gp
 from gurobipy import GRB, quicksum
 from solvers import SMTSolver, SolverError
-from pysmt.exceptions import SolverReturnedUnknownResultError
 import logging
 from timing import timed
 import os
@@ -40,8 +34,8 @@ def _gurobi_status_name(status: int) -> str:
     return str(status)
 
 class Generator:
-    def __init__(self, mode : str = "pysmt", solver : str = "opensmt", logic : str = "QF_LIA") -> None:
-        # modes - ["pysmt", "smtlib", "milp", "gurobi"] -- however, pysmt is inaccessible from the CLI program
+    def __init__(self, mode : str = "smtlib", solver : str = "opensmt", logic : str = "QF_LIA") -> None:
+        # modes - ["smtlib", "milp", "gurobi"]
         self.mode = mode
         self.declarations = []
         self.declared_names = set()
@@ -49,10 +43,6 @@ def __init__(self, mode : str = "pysmt", solver : str = "opensmt", logic : str =
         self.optimize_objectives = []
         self.solver = solver
         self.logic = logic
-        self.Symbol = Symbol
-        self.REAL = REAL
-        self.INT = INT
-        self.BOOL = BOOL
         self.symbols = {}
         self.stats = {}
         self.lp_problem = None
@@ -97,11 +87,7 @@ def _gp_params(self):
         self.lp_problem.Params.OutputFlag = 0
 
     def add_assertion(self, assertion):
-        if self.mode == "pysmt":
-            if self.solver is None:
-                raise ValueError("solver is not set")
-            self.solver.add_assertion(assertion)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             if self.incremental_mode:
                 self.write_incremental(f"(assert {assertion})")
             else:
@@ -138,9 +124,7 @@ def add_quadratic_assertion(self, assertion):
 
     def add_objective(self, objective):
         # add objective to the LP problem
-        if self.mode == "pysmt":
-            return
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return
         elif self.mode == "milp":
             self.lp_problem += objective, f"assertion_{self.stats['assertions']}"
@@ -167,12 +151,7 @@ def add_selection_variables(self, layer, gate_set, qubits, include_identity=True
         return selection_variables, bool_variables
 
     def Plus(self, x, y):
-        if self.mode == "pysmt":
-            plus_expr = x + y
-            if isinstance(plus_expr, bool):
-                return Plus(x, y)
-            return plus_expr
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             if isinstance(x, str) and isinstance(y, str):
                 return f"(+ {x} {y})"
             elif isinstance(x, str) and isinstance(y, (int, float)):
@@ -185,12 +164,7 @@ def Plus(self, x, y):
             return x + y
     
     def Minus(self, x, y):
-        if self.mode == "pysmt":
-            minus_expr = x - y
-            if isinstance(minus_expr, bool):
-                return Minus(x, y)
-            return minus_expr
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             if isinstance(x, str) and isinstance(y, str):
                 return f"(- {x} {y})"
             elif isinstance(x, str) and isinstance(y, (int, float)):
@@ -203,12 +177,7 @@ def Minus(self, x, y):
             return x - y
     
     def Times(self, x, y):
-        if self.mode == "pysmt":
-            times_expr = x * y
-            if isinstance(times_expr, bool):
-                return Times(x, y)
-            return times_expr
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             if isinstance(x, str) and isinstance(y, str):
                 return f"(* {x} {y})"
             elif isinstance(x, str) and isinstance(y, (int, float)):
@@ -232,20 +201,13 @@ def Square(self, x):
             raise NotImplementedError("square not yet supported")
         
     def Div(self, x, y):
-        if self.mode == "pysmt":
-            return Div(x, y)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(/ {x} {y})"
         elif self.mode == "milp" or self.mode == "gurobi":
             return x / y
     
     def Equals(self, x, y):
-        if self.mode == "pysmt":
-            eq_expr = (x == y)
-            if isinstance(eq_expr, bool):
-                return pysmtEquals(x, y)
-            return eq_expr
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             eq_expr = (x == y)
             if isinstance(eq_expr, bool) :
                 return f"(= {x} {y})"
@@ -257,47 +219,37 @@ def Equals(self, x, y):
             return x == y
 
     def ConstrainedEquals(self, sel, x, y, bigM=None):
-        if self.mode == "pysmt" or self.mode == "smtlib":
+        if self.mode == "smtlib":
             return self.add_assertion(self.Implies(sel, self.Equals(x, y)))
         elif self.mode == "milp" or self.mode == "gurobi":
             return x.constrained_equals(sel, bigM, x, y)
     
     def GE(self, x, y):
-        if self.mode == "pysmt":
-            return GE(x, y)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(>= {x} {y})"
         elif self.mode == "milp" or self.mode == "gurobi":
             return x >= y
     
     def LE(self, x, y):
-        if self.mode == "pysmt":
-            return LE(x, y)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(<= {x} {y})"
         elif self.mode == "milp" or self.mode == "gurobi":
             return x <= y
     
     def LT(self, x, y):
-        if self.mode == "pysmt":
-            return LT(x, y)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(< {x} {y})"
         elif self.mode == "milp" or self.mode == "gurobi":
             return x < y
     
     def GT(self, x, y):
-        if self.mode == "pysmt":
-            return GT(x, y)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(> {x} {y})"
         elif self.mode == "milp" or self.mode == "gurobi":
             return x > y
     
     def Ite(self, condition, true_value, false_value):
-        if self.mode == "pysmt":
-            return Ite(condition, true_value, false_value)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(ite {condition} {true_value} {false_value})"
         elif self.mode == "milp":
             raise NotImplementedError("explicit Ite not supported in milp mode")
@@ -307,18 +259,14 @@ def Ite(self, condition, true_value, false_value):
             return true_value
     
     def And(self, *args):
-        if self.mode == "pysmt":
-            return And(*args)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(and {' '.join(args)})"
         elif self.mode == "milp" or self.mode == "gurobi":
             for arg in args:
                 self.add_assertion(arg)
         
     def LAnd(self, *args):
-        if self.mode == "pysmt":
-            return And(*args)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(and {' '.join(args)})"
         elif self.mode == "gurobi":
             return gp.and_(args)
@@ -330,9 +278,7 @@ def LAnd(self, *args):
             return and_var
     
     def Or(self, *args):
-        if self.mode == "pysmt":
-            return Or(*args)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(or {' '.join(args)})"
         elif self.mode == "milp" or self.mode == "gurobi":
             or_var = self.declare_bool(f"or_{self.stats['bools']}")
@@ -345,30 +291,28 @@ def Indicator(self, sel, expr):
         if self.mode == "gurobi":
             return ((sel == 1) >> expr)
         else:
-            raise NotImplementedError("Indicator not supported in milp/pysmt/smtlib mode")
+            raise NotImplementedError("Indicator not supported in milp/smtlib mode")
     
     def NotIndicator(self, sel, expr):
         if self.mode == "gurobi":
             return ((sel == 0) >> expr)
         else:
-            raise NotImplementedError("NotIndicator not supported in milp/pysmt/smtlib mode")
+            raise NotImplementedError("NotIndicator not supported in milp/smtlib mode")
         
     def Abs(self, x):
         if self.mode == "gurobi":
             return gp.abs_(x)
         else:
-            raise NotImplementedError("Abs not supported in milp/pysmt/smtlib mode")
+            raise NotImplementedError("Abs not supported in milp/smtlib mode")
         
     def Exp(self, x):
         if self.mode == "gurobi":
             return 2 ** x
         else:
-            raise NotImplementedError("Exp not supported in milp/pysmt/smtlib mode")
+            raise NotImplementedError("Exp not supported in milp/smtlib mode")
 
     def Not(self, x):
-        if self.mode == "pysmt":
-            return Not(x)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(not {x})"
         elif self.mode == "milp":
             return 1 - x
@@ -378,7 +322,7 @@ def Not(self, x):
             return not_var
         
     def Sum(self, *args):
-        if self.mode == "pysmt" or self.mode == "smtlib":
+        if self.mode == "smtlib":
             return (f"(+ {' '.join(args)})")
         elif self.mode == "milp":
             return lpSum(args)
@@ -419,12 +363,12 @@ def AtLeastOne(self, *args):
         # OR between all 
         if self.mode == "milp" or self.mode == "gurobi":
             return self.add_assertion(self.Sum([bool_variable for bool_variable in args]) >= 1)
-        elif self.mode == "pysmt" or self.mode == "smtlib":
+        elif self.mode == "smtlib":
             return self.add_assertion(self.Or(*args))
     
     def AtMostOne(self, *args):
         # (NOT x1 or x2) and NOT (x1 and x3) ...
-        if self.mode == "milp" or self.mode == "pysmt" or self.mode == "smtlib":
+        if self.mode == "milp" or self.mode == "smtlib":
             for i in range(len(args)):
                 others = [args[j] for j in range(len(args)) if j != i]
                 for other in others:
@@ -440,9 +384,7 @@ def ExactlyOne(self, *args):
             self.AtMostOne(*args)
     
     def Implies(self, condition, expr, bigM=None):
-        if self.mode == "pysmt":
-            return Implies(condition, expr)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(=> {condition} {expr})"
         elif self.mode == "gurobi":
             return self.Indicator(condition, expr)
@@ -450,22 +392,11 @@ def Implies(self, condition, expr, bigM=None):
             raise NotImplementedError("explicit Implies not supported in milp mode")
         
     def Mod(self, x, y):
-        if self.mode == "pysmt":
-            q = self.declare_integer(f"q_mod_{self.stats['integers']}")
-            r = self.declare_integer(f"r_mod_{self.stats['integers']}")
-            self.add_assertion(self.And(self.Equals(x, self.Plus(self.Times(y, q), r)), self.GE(r, Int(0)), self.LT(r, y)))
-            return r
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             return f"(mod {x} {y})"
         elif self.mode == "milp" or self.mode == "gurobi":
             raise NotImplementedError("Mod not supported in milp/gurobi mode")
     
-    def _pysmt_declaration(self, x, type):
-        symbol = self.Symbol(x, type)
-        self.symbols[x] = symbol
-        self.declared_names.add(x)
-        return symbol
-
     def _smtlib_declaration(self, x, type):
         self.declarations.append(("declare-fun", x, f"() {type}"))
         if self.incremental_mode:
@@ -499,9 +430,7 @@ def declare_real(self, x, lb=None, ub=None):
         res = None
         if x not in self.declared_names:
             self.stats['reals'] += 1
-            if self.mode == "pysmt":
-                res = self._pysmt_declaration(x, self.REAL)
-            elif self.mode == "smtlib":
+            if self.mode == "smtlib":
                 res = self._smtlib_declaration(x, "Real")
             elif self.mode == "milp":
                 res = self._milp_declaration(x, LpContinuous, lb, ub)
@@ -515,14 +444,7 @@ def declare_real(self, x, lb=None, ub=None):
         return res
          
     def format_real(self, x):
-        if self.mode == "pysmt":
-            if isinstance(x, (int, float)):
-                return Real(float(x))
-            elif isinstance(x, str):
-                if x in self.symbols:
-                    return self.symbols[x]
-            return x
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             if isinstance(x, numbers.Real):
                 return self._smtlib_numeral(x)
             return x
@@ -556,9 +478,7 @@ def declare_integer(self, x, lb=None, ub=None):
             # even though declaring integer, in QF_NRA, reals have to be used
             if self.logic == "QF_NRA" or self.logic == "QF_LRA":
                 return self.declare_real(x)
-            if self.mode == "pysmt":
-                res = self._pysmt_declaration(x, self.INT)
-            elif self.mode == "smtlib":
+            if self.mode == "smtlib":
                 res = self._smtlib_declaration(x, "Int")
             elif self.mode == "milp":
                 res =  self._milp_declaration(x, LpInteger, lb, ub)
@@ -575,14 +495,7 @@ def declare_integer(self, x, lb=None, ub=None):
     def format_integer(self, x):
         if self.logic == "QF_NRA":
             return self.format_real(x)
-        if self.mode == "pysmt":
-            if isinstance(x, int):
-                return Int(x)
-            elif isinstance(x, str):
-                if x in self.symbols:
-                    return self.symbols[x]
-            return x
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             if isinstance(x, numbers.Integral):
                 return self._smtlib_numeral(x)
             return x
@@ -602,21 +515,14 @@ def declare_bool(self, x):
         res = None
         if x not in self.declared_names:
             self.stats['bools'] += 1
-            if self.mode == "pysmt":
-                res = self._pysmt_declaration(x, self.BOOL)
-            elif self.mode == "smtlib":
+            if self.mode == "smtlib":
                 res =  self._smtlib_declaration(x, "Bool")
             elif self.mode == "milp":
                 res = self._milp_declaration(x, LpBinary)
             elif self.mode == "gurobi":
                 res = self._gurobi_declaration(x, GRB.BINARY, lb=0.0, ub=1.0)
         else:
-            if self.mode == "pysmt":
-                if x in self.symbols:
-                    res = self.symbols[x]
-                else:
-                    res = x
-            elif self.mode == "smtlib":
+            if self.mode == "smtlib":
                 res = x
             elif self.mode == "milp" or self.mode == "gurobi":
                 if x in self.symbols:
@@ -630,7 +536,7 @@ def declare_bool(self, x):
     def declare_helpers(self):
         # possible helper methods
         # sqrt2, onehalf, inv_sqrt2 for exact representations in smt
-        if self.logic == "QF_NRA" and (self.mode in ["pysmt", "smtlib"]):
+        if self.logic == "QF_NRA" and self.mode == "smtlib":
             self.declare_real("sqrt2")
             self.add_assertion(self.Equals(self.Times(self.format_real("sqrt2"), self.format_real("sqrt2")), self.Real(2.0)))
             self.add_assertion(self.GT(self.format_real("sqrt2"), self.Real(0)))
@@ -641,9 +547,7 @@ def declare_helpers(self):
 
     def maximize(self, expression):
         # maximize objective
-        if self.mode == "pysmt":
-            pass
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             self.optimize_objectives.append(("maximize", expression))
         elif self.mode == "milp":
             raise NotImplementedError("milp mode not yet supported")
@@ -652,9 +556,7 @@ def maximize(self, expression):
     
     def minimize(self, expression):
         # minimize objective
-        if self.mode == "pysmt":
-            pass
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             self.optimize_objectives.append(("minimize", expression))
         elif self.mode == "milp":
             raise NotImplementedError("milp mode not yet supported")
@@ -665,14 +567,7 @@ def write_formula(self, filename):
         # write the full formula in given format to a file, either .smt2 or .lp
         if self.incremental_mode:
             return filename
-        if self.mode == "pysmt":
-            filename = os.path.splitext(filename)[0] + ".smt2"
-            if not hasattr(self.solver, "assertions"):
-                return filename
-            from pysmt.shortcuts import write_smtlib
-            formula = self.solver.environment.formula_manager.And(self.solver.assertions)
-            write_smtlib(formula, filename)
-        elif self.mode == "smtlib":
+        if self.mode == "smtlib":
             filename = os.path.splitext(filename)[0] + ".smt2"
             with open(filename, 'w') as f:
                 f.write(f"(set-logic {self.logic})\n")
@@ -700,7 +595,7 @@ def write_formula(self, filename):
         
     def enumerate_k_values(self, n, pair_idx):
         # enumerate all possible k values up to n for the given pair
-        if self.mode == "pysmt" or self.mode == "smtlib":
+        if self.mode == "smtlib":
             self.declare_integer(f"k{pair_idx}")
             eqs = []
             for i in range(n):
@@ -711,7 +606,7 @@ def enumerate_k_values(self, n, pair_idx):
 
     def enumerate_powers_of_2(self, n, pair_idx):
         # enumerate all possible powers of 2^k up to n for the given pair
-        if self.mode == "pysmt" or self.mode == "smtlib":
+        if self.mode == "smtlib":
             self.declare_integer(f"pow2{pair_idx}")
             self.declare_integer(f"k{pair_idx}")
             for i in range(n):
@@ -953,8 +848,6 @@ def push(self):
                     "assertions": assertions_to_push,
                     "optimize_objectives": optimize_objectives
                 }
-        elif self.mode == "pysmt":
-            self.solver.push()
     
     def pop(self):
         if self.mode == "milp":
@@ -986,8 +879,6 @@ def pop(self):
                 self.assertions = self.saved_push["assertions"]
                 self.optimize_objectives = self.saved_push["optimize_objectives"]
                 self.saved_push = None
-        elif self.mode == "pysmt":
-            self.solver.pop()
     
     def filter_model(self, model, depth):
         # not model -> not (g1 and g2 and g3 ...) -> (not g1 or not g2 or not g3 ...)
@@ -998,8 +889,6 @@ def filter_model(self, model, depth):
         elif self.mode == "smtlib":
             # SMT-LIB terms are the variable names themselves (symbols is not filled in incremental mode)
             self.add_assertion(self.Not(self.And(*model)))
-        elif self.mode == "pysmt":
-            self.add_assertion(self.Not(self.And(*[self.symbols[bool_var] for bool_var in model])))
             
     def write_incremental(self, statement : str):
         if self.mode != 'smtlib':
@@ -1058,9 +947,6 @@ def get_model(self):
                 return self.solver.get_model()
             else:
                 return self.model
-        elif self.mode == "pysmt":
-            # the same with get-value
-            return self.solver.get_model()
         
         
     def check_sat(self, formula_file: str = "formula.smt2"):
@@ -1110,16 +996,6 @@ def check_sat(self, formula_file: str = "formula.smt2"):
                 self.model = result
             log.info("Solver returned SAT")
             return True
-        elif self.mode == "pysmt":
-            try:
-                result = self.solver.solve()
-            except SolverReturnedUnknownResultError:
-                return self._unknown()
-            except Exception as e:
-                # a crash or a parse error is a failure, not an answer
-                raise SolverError(f"pySMT solver failed: {type(e).__name__}: {e}") from e
-            log.info("Solver returned %s", "SAT" if result else "UNSAT")
-            return result
 
     def _unknown(self) -> bool:
         # unknown is not UNSAT: the caller searches on, and synthesis() reports what stayed unproven
diff --git a/src/parser.py b/src/parser.py
index 8a8538d..2862a1c 100644
--- a/src/parser.py
+++ b/src/parser.py
@@ -107,9 +107,6 @@ def filter_items(self, model : any) -> tuple[Circuit, list[Vector]]:
                 elif isinstance(value_obj, float):
                     if abs(value_obj - 1) < 1e-6:
                         parse = True
-                else:
-                    if value_obj.is_true():
-                        parse = True
                 if parse: # parse only if the selection variable is True
                     parts = variable.split("_")
                     d = int(parts[0][1:])
@@ -153,8 +150,6 @@ def filter_items(self, model : any) -> tuple[Circuit, list[Vector]]:
                     costs[indice] = round(value_obj)
                 elif isinstance(value_obj, str):
                     costs[indice] = round(float(value_obj))
-                else:
-                    costs[indice] = int(value_obj.constant_value())
         self.stats['cost'] = costs[best_indice]
         circ.set_cost(self.stats['cost'])
         return circ, out_vectors
diff --git a/src/synth.py b/src/synth.py
index 678ca47..1efd42c 100644
--- a/src/synth.py
+++ b/src/synth.py
@@ -16,9 +16,6 @@
 import tempfile
 import subprocess
 from sim import Simulator
-from pysmt.logics import QF_NRA, QF_LIA, QF_NIA, QF_LRA
-from pysmt.shortcuts import Portfolio, Symbol, Real, And, Equals, Plus, GT, LT, get_env, Int, Or, Not, Implies, GE, LE, Ite, Minus, Div, Times, write_smtlib, Solver
-from pysmt.typing import REAL, INT
 from pareto import Pareto
 from gates import GateSet, check_supported, Circuit, k_increments, max_k_increment
 from pulp import *
@@ -101,8 +98,6 @@ def close(self) -> None:
         solver = self.gen.solver
         if isinstance(solver, (SMTSolver, PortfolioSMTSolver)):
             solver.close()
-        elif self.gen.mode == "pysmt" and hasattr(solver, "exit"):  # pySMT's Solver or Portfolio
-            solver.exit()
             
     def _load_solver_config(self, solver: str, path: str | None) -> None:
         self.solver_config = load_solver_config(path)
@@ -112,30 +107,12 @@ def _load_solver_config(self, solver: str, path: str | None) -> None:
 
     def add_solvers(self, incremental_mode : bool = False) -> None:
         # register the solvers from the solver configuration (solvers.toml)
-        if self.gen.mode == "pysmt":
-            logics = {"QF_LIA": QF_LIA, "QF_LRA": QF_LRA, "QF_NIA": QF_NIA, "QF_NRA": QF_NRA}
-        else:
-            logics = {logic: logic for logic in LOGICS}
         for name, config in self.solver_config.items():
-            # pySMT drives its generic solvers through stdin by itself
-            args = config.command(incremental_mode and self.gen.mode != "pysmt")
-            self.add_one_solver(name=name, args=args, logics=[logics[logic] for logic in config.logics],
+            self.add_one_solver(name=name, args=config.command(incremental_mode), logics=list(config.logics),
                                 incremental_mode=incremental_mode)
     
     def add_one_solver(self, name: str, args: list[str], logics: list[str], smtlib_flags: list[str] = [], incremental_mode: bool = False) -> None:
-        if name == "z3" and self.gen.mode == "pysmt": 
-            return
-        if self.gen.mode == "pysmt":
-            factory = get_env().factory
-            # pySMT keeps solvers registered for the whole process, e.g. by an earlier synthesis
-            if factory.is_generic_solver(name):
-                if factory.get_generic_solver_info(name) != (args, logics):
-                    raise SolverConfigError(f"pySMT already has a solver {name} with another command or logics; "
-                                            "use one solver configuration per process")
-                return
-            factory.add_generic_solver(name=name, args=args, logics=logics)
-        else:
-            self.solvers[name] = SMTSolver(name, args, logics, smtlib_flags, incremental_mode)
+        self.solvers[name] = SMTSolver(name, args, logics, smtlib_flags, incremental_mode)
 
     def encode_layer(self, inp : Vector, out : Vector, layer : int, inp_weight : any = None, out_weight : any = None, selection_variables : list = None, bool_variables : list = None) -> None:
         updates_k_value = []        
@@ -769,7 +746,7 @@ def synthesis(self, qasm_file=None, matrix=None, vectors=None, vector_pairs=None
                        custom -> input_vectors with qasm_file or matrix, or else vector_pairs, q, d, gate_set)
             vector_pairs -> list of pairs (input_vector, output_vector) for input and its expected output.
             input_vectors -> with vectors=custom and a qasm_file or matrix: the input states; the expected outputs are simulated from the circuit
-            solving -> smt, pysmt, milp (these need a solver) or gurobi
+            solving -> smt, milp (these need a solver) or gurobi
             solver -> specify specific solver or portfolio of solvers
             solver_config -> SMT solver configuration file (default: $MILQ_SOLVER_CONFIG, else solvers.toml in the repository root)
             mode -> specify solving method (basic -> create whole formula and get the best model, incremental -> incrementally generate the formula, binary, topdown, bottomup -> searches to optimize cost function)
@@ -818,9 +795,9 @@ def synthesis(self, qasm_file=None, matrix=None, vectors=None, vector_pairs=None
         if matrix is not None and d is None and mode not in ["incremental", "pareto-incremental"]:
             # the fixed-depth modes take d from the input's gate count, and a matrix has none
             raise ValueError("d is required for a matrix input in basic, binary, topdown and bottomup mode")
-        if solving not in ["smt", "pysmt", "milp", "gurobi"]:
-            raise ValueError("solving can be only smt, pysmt, milp, or gurobi")
-        if solving in ["smt", "milp", "pysmt"] and solver is None:
+        if solving not in ["smt", "milp", "gurobi"]:
+            raise ValueError("solving can be only smt, milp, or gurobi")
+        if solving in ["smt", "milp"] and solver is None:
             raise ValueError("a solver is required for basic smt and milp solving")
         if mode not in ["basic", "incremental", "binary", "topdown", "bottomup", "pareto-incremental"]:
             raise ValueError("mode can be only basic, incremental, binary, topdown, bottomup, or pareto-incremental")
@@ -956,23 +933,6 @@ def synthesis(self, qasm_file=None, matrix=None, vectors=None, vector_pairs=None
                                             f"{', '.join(self.solvers[solver].logics)})")
                 self.gen.solver = self.solvers[solver]
 
-        elif solving == "pysmt":
-            self._load_solver_config(solver, solver_config)
-            self.gen.mode = "pysmt"
-            incremental_mode = True if mode == "incremental" or mode == "pareto-incremental" else False
-            self.add_solvers(incremental_mode=incremental_mode)
-            if solver == "portfolio":
-                if self.gen.logic != "QF_NRA":
-                    solvers = ["z3", "cvc5", "yices2", "opensmt", "smtinterpol"]
-                else:
-                    log.warning("pySMT parser does not support some outputs from solvers that support NRA even though LIA works just fine.")
-                    solvers = ["z3", "cvc5", "yices2"]
-                # z3 is pySMT's own (z3-solver), the others have to be configured
-                solvers = [name for name in solvers if name == "z3" or (name in self.solver_config and self.solver_config[name].portfolio
-                                                                        and self.gen.logic in self.solver_config[name].logics)]
-                self.gen.solver = Portfolio(solvers, logic=self.gen.logic, incremental=incremental_mode, generate_models=True)
-            else:
-                self.gen.solver = Solver(name=solver, logic=self.gen.logic, incremental=incremental_mode, generate_models=True)
         elif solving == "milp":
             if solver not in ["gurobi", "cbc"]:
                 raise ValueError(f"Invalid solver: {solver}")
diff --git a/tests/conftest.py b/tests/conftest.py
index 2a24d92..6e945a8 100644
--- a/tests/conftest.py
+++ b/tests/conftest.py
@@ -13,10 +13,12 @@
 
 from complex.classic import Complex
 from complex.fivetuple import FiveTuple
+from generator import Generator
 from sim import Simulator
 from solver_config import ENV_VARIABLE, load_solver_config
 from solver_detection import detect, render
 from solver_download import bin_dir
+from solvers import SMTSolver
 
 OMEGA = np.exp(1j * np.pi / 4)
 
@@ -43,6 +45,17 @@ def pytest_report_header(config):
     return "SMT solvers: " + ", ".join(f"{name} ({solver.path})" for name, solver in SOLVERS.items())
 
 
+def z3_generator(logic="QF_LIA"):
+    # an SMT-LIB generator solved by z3 (installed with z3-solver); check it with z3_check
+    gen = Generator(mode="smtlib", logic=logic)
+    gen.solver = SMTSolver("z3", SOLVERS["z3"].command(), [logic])
+    return gen
+
+
+def z3_check(gen, directory):
+    return gen.check_sat(gen.write_formula(os.path.join(directory, "formula.smt2")))
+
+
 def to_complex(element, k, representation):
     # numeric value of a simulated amplitude
     if representation is FiveTuple:
diff --git a/tests/test_generator.py b/tests/test_generator.py
index fc67984..eec9a4e 100644
--- a/tests/test_generator.py
+++ b/tests/test_generator.py
@@ -2,13 +2,13 @@
 
 import pytest
 from pulp import PULP_CBC_CMD
-from pysmt.shortcuts import Solver
 
+from conftest import z3_check, z3_generator
 from gates import GateSet
 from generator import Generator
 
 
-@pytest.mark.parametrize("mode", ["pysmt", "milp", "gurobi"])
+@pytest.mark.parametrize("mode", ["smtlib", "milp", "gurobi"])
 @pytest.mark.parametrize("first, second, allowed", [
     ("t_q0", "tdg_q0", False),        # G Gdg is identity
     ("tdg_q0", "t_q0", False),        # Gdg G is identity
@@ -19,10 +19,11 @@
     ("cx_q0_q1", "cx_q1_q0", True),   # different wire order is a different gate
 ])
 def test_add_constraints_forbids_only_adjoint_pairs(tmp_path, mode, first, second, allowed):
-    gen = Generator(mode=mode)
-    if mode == "pysmt":
-        gen.solver = Solver(name="z3")
-    elif mode == "milp":
+    if mode == "smtlib":
+        gen = z3_generator()
+    else:
+        gen = Generator(mode=mode)
+    if mode == "milp":
         gen.solver = lambda: PULP_CBC_CMD(msg=False)
     gate_set = GateSet(["h", "t", "tdg", "cx"])
     for layer in (0, 1):
@@ -31,4 +32,4 @@ def test_add_constraints_forbids_only_adjoint_pairs(tmp_path, mode, first, secon
     # select the two gates
     gen.AtLeastOne(gen.symbols[f"L0_{first}"])
     gen.AtLeastOne(gen.symbols[f"L1_{second}"])
-    assert gen.check_sat() == allowed
+    assert (z3_check(gen, tmp_path) if mode == "smtlib" else gen.check_sat()) == allowed
diff --git a/tests/test_pareto.py b/tests/test_pareto.py
index adb81d5..2ff392a 100644
--- a/tests/test_pareto.py
+++ b/tests/test_pareto.py
@@ -5,15 +5,13 @@
 
 import numpy as np
 import pytest
-from pysmt.shortcuts import Solver
 
 import pareto
 from complex.classic import Complex
 from complex.fivetuple import FiveTuple
 from complex.vector import Vector
-from conftest import BENCHMARKS, unitary
+from conftest import BENCHMARKS, unitary, z3_check, z3_generator
 from gates import Circuit, Gate, GateSet
-from generator import Generator
 from pareto import Pareto
 from solvers import SolverError
 from synth import Synthesizer, rus_recovery_pairs
@@ -67,15 +65,14 @@ def test_rus_cost(workdir, representation):
     assert synthesizer.rus_cost(circuit, recovery, [half]) == (5, pytest.approx(0.5))
 
 
-def test_filter_model_pysmt_excludes_model():
-    gen = Generator(mode="pysmt")
-    gen.solver = Solver(name="z3")
+def test_filter_model_smtlib_excludes_model(tmp_path):
+    gen = z3_generator()
     names = ["L0_h_q0", "L1_cx_q0_q1"]
     for name in names:
         gen.add_assertion(gen.declare_bool(name))
-    assert gen.solver.solve()
+    assert z3_check(gen, tmp_path)
     gen.filter_model(names, 2)
-    assert not gen.solver.solve()
+    assert not z3_check(gen, tmp_path)
 
 
 @pytest.mark.parametrize("expired_after", [1, 3])
diff --git a/tests/test_rescaling_bound.py b/tests/test_rescaling_bound.py
index 8e8d767..cb94778 100644
--- a/tests/test_rescaling_bound.py
+++ b/tests/test_rescaling_bound.py
@@ -80,15 +80,6 @@ def test_custom_target_with_a_large_k(workdir, mode, k_target):
     assert synthesized_gates(circuit) == ["x"]
 
 
-def test_float_k_reaches_pysmt_as_an_integer(workdir):
-    # yices2 tolerates a k of 4.0 in the formula; pySMT crashed on it, so the vectors must carry the int
-    res, circuit, _ = Synthesizer().synthesis(vectors="custom", vector_pairs=zero_to_one(4.0), q=1, d=1,
-                                              gate_set=GateSet(["x", "h"]), mode="basic", output_qasm="out.qasm",
-                                              solving="pysmt", solver="z3", complex_representation="FiveTuple")
-    assert res
-    assert synthesized_gates(circuit) == ["x"]
-
-
 def test_custom_target_with_a_fractional_k(workdir):
     with pytest.raises(ValueError, match="k of a FiveTuple vector must be an integer, got 4.5"):
         Synthesizer().synthesis(vectors="custom", vector_pairs=zero_to_one(4.5), q=1, d=1, gate_set=GateSet(["x", "h"]),
diff --git a/tests/test_simulator.py b/tests/test_simulator.py
index 1b74b9f..1e7a0a5 100644
--- a/tests/test_simulator.py
+++ b/tests/test_simulator.py
@@ -13,7 +13,7 @@
 from complex.classic import Complex
 from complex.fivetuple import FiveTuple
 from complex.vector import Vector
-from conftest import to_complex, unitary
+from conftest import to_complex, unitary, z3_check, z3_generator
 from gates import supported_gates
 from sim import Simulator
 
@@ -132,11 +132,8 @@ def test_vector_rescale_with_rejects_generator(tmp_path):
     (2, (4, 0, -2, 0), (2, -1)),  # even k
 ])
 def test_vector_to_real_with_generator(tmp_path, name, k, element, expected):
-    from pysmt.shortcuts import Not, Solver
     from complex.vector import Vector
-    from generator import Generator
-    gen = Generator(mode="pysmt", logic="QF_NRA")
-    gen.solver = Solver(name="z3")
+    gen = z3_generator(logic="QF_NRA")
     vec = Vector(q=1, name=name, generator=gen, element_representation=FiveTuple, k=k, k_bound=4)
     if name is None:
         vec[0] = FiveTuple(*element, generator=gen)
@@ -147,9 +144,9 @@ def test_vector_to_real_with_generator(tmp_path, name, k, element, expected):
         gen.add_assertion(gen.Equals(vec.k, gen.Int(k)))
     real = vec.to_real(max_k=4)[0]
     matches = gen.And(gen.Equals(real.real, gen.Real(expected[0])), gen.Equals(real.imag, gen.Real(expected[1])))
-    assert gen.check_sat()
-    gen.add_assertion(Not(matches))
-    assert not gen.check_sat()
+    assert z3_check(gen, tmp_path)
+    gen.add_assertion(gen.Not(matches))
+    assert not z3_check(gen, tmp_path)
 
 
 # simulator stats (#87, F65)
diff --git a/tests/test_solver_config.py b/tests/test_solver_config.py
index 548f791..9e1f48f 100644
--- a/tests/test_solver_config.py
+++ b/tests/test_solver_config.py
@@ -1,6 +1,5 @@
 """The SMT solver configuration (solvers.toml) and how synthesis uses it."""
 
-import multiprocessing
 import os
 import subprocess
 import sys
@@ -172,33 +171,6 @@ def test_portfolio_without_a_solver_for_the_logic(workdir):
         synthesize("portfolio", config, representation="Classic")
 
 
-# pySMT's portfolio creates its solvers in child processes, which see the generic solvers only when forked (#93)
-PORTFOLIO_NOT_FORKED = pytest.mark.xfail(multiprocessing.get_start_method() != "fork", strict=True,
-                                         reason="#93: the configured solvers are missing in pySMT's portfolio processes")
-
-
-@pytest.mark.parametrize("solver", ["yices2", pytest.param("portfolio", marks=PORTFOLIO_NOT_FORKED)])
-def test_pysmt_solving(workdir, solver):
-    # the pySMT backend registers the configured solvers as pySMT generic solvers
-    res, circuit, _ = Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="pysmt", solver=solver, mode="basic",
-                                              output_qasm="out.qasm")
-    assert res
-    assert circuit.gate_count() == 2
-
-
-def test_pysmt_solving_rejects_a_changed_solver(workdir):
-    Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="pysmt", solver="yices2", mode="basic")
-    config = write_config(workdir / "s.toml", f'[solvers.yices2]\npath = "{YICES}"\nargs = ["-v", "0"]\nlogics = ["QF_LIA"]\n')
-    with pytest.raises(SolverConfigError, match="pySMT already has a solver yices2"):
-        Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="pysmt", solver="yices2", mode="basic",
-                                solver_config=config)
-
-
-def test_pysmt_solving_rejects_unknown_solver(workdir):
-    with pytest.raises(SolverConfigError, match="Invalid solver: yices"):
-        Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="pysmt", solver="yices", mode="basic")
-
-
 def test_cli_reports_config_errors(workdir):
     result = subprocess.run([sys.executable, os.path.join(REPO_ROOT, "milq"), "-s", "smt", "-a", "yices", GHZ2],
                             capture_output=True, text=True, env={**os.environ, ENV_VARIABLE: SOLVER_CONFIG})
diff --git a/tests/test_solver_errors.py b/tests/test_solver_errors.py
index 2278246..7c23880 100644
--- a/tests/test_solver_errors.py
+++ b/tests/test_solver_errors.py
@@ -8,7 +8,6 @@
 import threading
 
 import pytest
-from pysmt.exceptions import SolverReturnedUnknownResultError
 
 from generator import Generator
 from solvers import PortfolioSMTSolver, SMTSolver, SolverError, _describe_failure
@@ -224,30 +223,6 @@ def test_portfolio_unknown_reports_the_failed_solvers(formula, caplog):
                for r in caplog.records)
 
 
-class RaisingSolver:
-    def __init__(self, error):
-        self.error = error
-
-    def solve(self):
-        raise self.error
-
-
-def test_pysmt_unknown_is_counted():
-    gen = Generator(mode="pysmt")
-    gen.solver = RaisingSolver(SolverReturnedUnknownResultError())
-    assert gen.check_sat() is False
-    assert gen.unknowns == 1
-
-
-def test_pysmt_failure_raises():
-    # used to be logged as UNKNOWN/UNSAT and read as "no circuit" (BUGS N11)
-    gen = Generator(mode="pysmt")
-    gen.solver = RaisingSolver(RuntimeError("parse error"))
-    with pytest.raises(SolverError, match="pySMT solver failed: RuntimeError: parse error"):
-        gen.check_sat()
-    assert gen.unknowns == 0
-
-
 def answer_unknown(monkeypatch, calls=None):
     # the real solver runs, but the answers of the given calls (all if None) are replaced by unknown
     original, count = SMTSolver.solve, itertools.count()
diff --git a/tests/test_solver_processes.py b/tests/test_solver_processes.py
index 5ec2e49..b2c0658 100644
--- a/tests/test_solver_processes.py
+++ b/tests/test_solver_processes.py
@@ -122,22 +122,6 @@ def fail(synthesizer, vector_pairs, output_qasm):
     assert child_processes(YICES) == []
 
 
-def test_close_exits_the_pysmt_solver(workdir):
-    # pySMT's Solver and Portfolio are stopped with exit(); a stand-in, as a second pySMT synthesis in one process
-    # fails (#90)
-    class PySMTSolver:
-        exits = 0
-
-        def exit(self):
-            self.exits += 1
-
-    synthesizer = Synthesizer()
-    synthesizer.gen.mode = "pysmt"
-    synthesizer.gen.solver = PySMTSolver()
-    synthesizer.close()
-    assert synthesizer.gen.solver.exits == 1
-
-
 def test_synthesizer_is_a_context_manager(workdir):
     with Synthesizer():  # nothing to stop without a synthesis
         pass