diff --git a/cpmpy/solvers/__init__.py b/cpmpy/solvers/__init__.py
index 3ff12c435..384d2f676 100644
--- a/cpmpy/solvers/__init__.py
+++ b/cpmpy/solvers/__init__.py
@@ -36,6 +36,7 @@
         gurobi
         exact
         z3
+        cvc5
         pysat
         pysdd
         pindakaas
diff --git a/cpmpy/solvers/cvc5.py b/cpmpy/solvers/cvc5.py
new file mode 100644
index 000000000..dbb12b02a
--- /dev/null
+++ b/cpmpy/solvers/cvc5.py
@@ -0,0 +1,526 @@
+#!/usr/bin/env python
+#-*- coding:utf-8 -*-
+##
+## cvc5.py
+##
+"""
+    Interface to CVC5's Python API.
+
+    cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems that
+    supports a large number of theories and their combination. It is the successor of CVC4 and is intended 
+    to be an open and extensible SMT engine. cvc5 is a joint project led by Stanford University and the 
+    University of Iowa.(see https://cvc5.github.io/)
+
+    This implemantation makes use of cvc5's "pythonic" API, closely replicating the Z3 API.
+
+    Always use :func:`cp.SolverLookup.get("cvc5") <cpmpy.solvers.utils.SolverLookup.get>` to instantiate the solver object.
+
+    ============
+    Installation
+    ============
+
+    Requires that the 'cvc5' python package is installed:
+
+    .. code-block:: console
+    
+        $ pip install cvc5
+
+    See detailed installation instructions at:
+    https://cvc5.github.io/docs/latest/api/python/python.html
+
+    The rest of this documentation is for advanced users.
+
+    ===============
+    List of classes
+    ===============
+
+    .. autosummary::
+        :nosignatures:
+
+        CPM_cvc5
+
+    ==============
+    Module details
+    ==============
+"""
+from typing import Optional
+import pkg_resources
+
+from cpmpy.transformations.get_variables import get_variables
+from .solver_interface import SolverInterface, SolverStatus, ExitStatus
+from ..exceptions import NotSupportedError
+from ..expressions.core import Expression, Comparison, Operator, BoolVal
+from ..expressions.globalconstraints import GlobalConstraint, DirectConstraint
+from ..expressions.globalfunctions import GlobalFunction
+from ..expressions.variables import _BoolVarImpl, NegBoolView, _NumVarImpl, _IntVarImpl, intvar
+from ..expressions.utils import is_num, is_any_list, is_bool, is_int, is_boolexpr, eval_comparison
+from ..transformations.decompose_global import decompose_in_tree
+from ..transformations.normalize import toplevel_list
+from ..transformations.safening import no_partial_functions
+
+
+class CPM_cvc5(SolverInterface):
+    """
+    Interface to cvc5's Python API.
+
+    Creates the following attributes (see parent constructor for more):
+        
+    - ``cvc5_solver``: object, cvc5's Solver() object
+
+    The :class:`~cpmpy.expressions.globalconstraints.DirectConstraint`, when used, calls a function in the `cvc5` namespace and ``cvc5_solver.add()``'s the result.
+
+    Documentation of the solver's own Python API:
+    https://cvc5.github.io/api/python/pythonic/cvc5.html
+
+    .. note::
+        Terminology note: a 'model' for cvc5 is a solution!
+    """
+
+    @staticmethod
+    def supported():
+        # try to import the package
+        try:
+            import cvc5
+            return True
+        except ModuleNotFoundError:
+            return False
+        except Exception as e:
+            raise e
+        
+    @classmethod
+    def version(cls) -> Optional[str]:
+        """
+        Returns the installed version of the solver's Python API.
+        """
+        try:
+            return pkg_resources.get_distribution('cvc5').version
+        except pkg_resources.DistributionNotFound:
+            return None
+        
+    def __init__(self, cpm_model=None, subsolver="sat"):
+        """
+        Constructor of the native solver object
+
+        Arguments:
+        - cpm_model: Model(), a CPMpy Model() (optional)
+        - subsolver: None
+        """
+        if not self.supported():
+            raise Exception("CPM_cvc5: Install the python package 'cvc5' to use this solver interface.")
+
+        import cvc5.pythonic as cvc5
+
+
+        # initialise the native solver object
+        self.cvc5_solver = cvc5.Solver()
+   
+        # initialise everything else and post the constraints
+        super().__init__(name="cvc5", cpm_model=cpm_model)
+
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        return self.cvc5_solver
+
+
+    def solve(self, time_limit=None, assumptions=[], **kwargs):
+        """
+            Call the cvc5 solver
+
+            Arguments:
+                time_limit (float, optional):       maximum solve time in seconds
+                assumptions:                        list of CPMpy Boolean variables (or their negation) that are assumed to be true.
+                                                    For repeated solving, and/or for use with :func:`s.get_core() <get_core()>`: if the model is UNSAT,
+                                                    get_core() returns a small subset of assumption variables that are unsat together.
+                **kwargs:                           any keyword argument, sets parameters of solver object
+
+            An overview of the cvc5 solver parameters can found at 
+            https://cvc5.github.io/docs/cvc5-1.0.8/options.html
+
+            You can use any of these parameters as keyword argument to `solve()` and they will
+            be forwarded to the solver. Examples include:
+
+            =============================   ============
+            Argument                        Description
+            =============================   ============
+            ``rlimit-per``                    set resource limit
+            ``random_seed``                   random seed
+            ``compute-partitions``            number of parallel workers (default=0)
+            =============================   ============
+        """  
+
+        import cvc5.pythonic as cvc5
+
+        # ensure all vars are known to solver
+        self.solver_vars(list(self.user_vars))
+
+        # set time limit
+        if time_limit is not None:
+            if time_limit <= 0:
+                raise ValueError("Time limit must be positive")
+            # cvc5 expects milliseconds in int
+            self.cvc5_solver.set(**{"tlimit-per":int(time_limit*1000)})
+
+        # process assumption variables
+        cvc5_assum_vars = self.solver_vars(assumptions)
+        self.assumption_dict = {cvc5_var : cpm_var for (cpm_var, cvc5_var) in zip(assumptions, cvc5_assum_vars)}
+
+        # call the solver, with parameters
+        for (key,value) in kwargs.items():
+            self.cvc5_solver.setOption(key, value)
+
+        # check assumption variables
+        my_status = repr(self.cvc5_solver.check(*cvc5_assum_vars))
+
+        # new status, translate runtime
+        self.cpm_status = SolverStatus(self.name)
+        st = self.cvc5_solver.statistics()
+        self.cpm_status.runtime = float(st['global::totalTime']["value"][:-2])/1000
+
+        # translate exit status
+        if my_status == "sat":
+            if self.has_objective(): # COP
+                # check if optimal solution found and proven, i.e. bounds are equal
+                lower_bound = self.cvc5_solver.lower(self.obj_handle)
+                upper_bound = self.cvc5_solver.upper(self.obj_handle)
+                if lower_bound == upper_bound: # found optimal
+                    self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+                else: # suboptimal / not proven
+                    self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            else: # CSP
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+        elif my_status == "unsat":
+            self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+        elif my_status == "unknown":
+            try:
+                model = self.cvc5_solver.model()
+                if model: # a solution was found, just not the optimal one (or not proven)
+                    self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+                # can happen when timeout is reached...
+                else:
+                    self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+            # can happen when timeout is reached...
+            except cvc5.Exception as e: # no model has been initialized, not even an empty one
+                self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+
+        else:  # another?
+            raise NotImplementedError(my_status)  # a new status type was introduced, please report on github
+
+        # True/False depending on self.cpm_status
+        has_sol = self._solve_return(self.cpm_status)
+
+        # translate solution values (of user specified variables only)
+        self.objective_value_ = None
+        if has_sol:
+            sol = self.cvc5_solver.model() # the solution (called model in cvc5)
+            # fill in variable values
+            for cpm_var in self.user_vars:
+                sol_var = self.solver_var(cpm_var)
+                if isinstance(cpm_var, _BoolVarImpl):
+                    cpm_var._value = bool(sol[sol_var])
+                elif isinstance(cpm_var, _NumVarImpl):
+                    cpm_var._value = sol[sol_var].as_long()
+
+            # translate objective, for optimisation problems only
+            if self.has_objective():
+                obj = self.cvc5_solver.objectives()[0]
+                self.objective_value_ = sol.evaluate(obj).as_long()
+
+        else:  # clear values of variables
+            for cpm_var in self.user_vars:
+                cpm_var._value = None
+
+        return has_sol
+
+
+    def solver_var(self, cpm_var):
+        """
+            Creates solver variable for cpmpy variable
+            or returns from cache if previously created
+        """
+        import cvc5.pythonic as cvc5
+
+        if is_num(cpm_var): # shortcut, eases posting constraints
+            return cpm_var
+
+        # special case, negative-bool-view
+        # work directly on var inside the view
+        if isinstance(cpm_var, NegBoolView):
+            return cvc5.Not(self.solver_var(cpm_var._bv))
+
+        # create if it does not exit
+        if cpm_var not in self._varmap:
+            # we assume al variables are user variables (because nested expressions)
+            self.user_vars.add(cpm_var)
+            if isinstance(cpm_var, _BoolVarImpl):
+                revar = cvc5.Bool(str(str(cpm_var))) # TODO: first str call shouldn't return a np.str_
+            elif isinstance(cpm_var, _IntVarImpl):
+                revar = cvc5.Int(str(str(cpm_var)))
+                # set bounds
+                self.cvc5_solver.add(revar >= cpm_var.lb)
+                self.cvc5_solver.add(revar <= cpm_var.ub)
+            else:
+                raise NotImplementedError("Not a know var {}".format(cpm_var))
+            self._varmap[cpm_var] = revar
+
+        return self._varmap[cpm_var]
+
+    def objective(self, expr, minimize=True):
+        raise NotSupportedError("CVC5 only supports satisfaction problems.")
+
+    def transform(self, cpm_expr):
+        """
+            Transform arbitrary CPMpy expressions to constraints the solver supports
+
+            Implemented through chaining multiple solver-independent **transformation functions** from
+            the `cpmpy/transformations/` directory.
+
+            See the :ref:`Adding a new solver` docs on readthedocs for more information.
+
+            :param cpm_expr: CPMpy expression, or list thereof
+            :type cpm_expr: Expression or list of Expression
+
+            :return: list of Expression
+        """
+
+        cpm_cons = toplevel_list(cpm_expr)
+        cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"div", "mod"})
+        supported = {"alldifferent", "xor", "ite"}  # TODO: check which else
+        cpm_cons = decompose_in_tree(cpm_cons, supported, supported, csemap=self._csemap)
+        return cpm_cons
+
+    def add(self, cpm_expr):
+        """
+            CVC5 supports nested expressions so translate expression tree and post to solver API directly
+
+            Any CPMpy expression given is immediately transformed (through `transform()`)
+            and then posted to the solver in this function.
+
+            This can raise 'NotImplementedError' for any constraint not supported after transformation
+
+            The variables used in expressions given to add are stored as 'user variables'. Those are the only ones
+            the user knows and cares about (and will be populated with a value after solve). All other variables
+            are auxiliary variables created by transformations.
+
+        Arguments:
+            cpm_expr (Expression or list of Expression): CPMpy expression, or list thereof
+        
+        Returns:
+            self
+
+        """
+        # all variables are user variables, handled in `solver_var()`
+        # unless their constraint gets simplified away, so lets collect them anyway
+        get_variables(cpm_expr, collect=self.user_vars)
+
+        # transform and post the constraints
+        for cpm_con in self.transform(cpm_expr):
+            # translate each expression tree, then post straight away
+            cvc5_con = self._cvc5_expr(cpm_con)
+            self.cvc5_solver.add(cvc5_con)
+
+        return self
+    __add__ = add  # avoid redirect in superclass
+
+    def _cvc5_expr(self, cpm_con):
+        """
+            CVC5 supports nested expressions,
+            so we recursively translate our expressions to theirs.
+
+            Accepts single constraints or a list thereof, return type changes accordingly.
+
+        """
+        import cvc5.pythonic as cvc5
+
+        if is_num(cpm_con):
+            # translate numpy to python native
+            if is_bool(cpm_con):
+                return bool(cpm_con)
+            elif is_int(cpm_con):
+                return cvc5.IntVal(int(cpm_con))
+            return float(cpm_con)
+
+        elif is_any_list(cpm_con):
+            # arguments can be lists
+            return [self._cvc5_expr(con) for con in cpm_con]
+
+        elif isinstance(cpm_con, BoolVal):
+            return cpm_con.args[0]
+
+        elif isinstance(cpm_con, _NumVarImpl):
+            return self.solver_var(cpm_con)
+
+        # Operators: base (bool), lhs=numexpr, lhs|rhs=boolexpr (reified ->)
+        elif isinstance(cpm_con, Operator):
+            arity, _ = Operator.allowed[cpm_con.name]
+            # 'and'/n, 'or'/n, '->'/2
+            if cpm_con.name == 'and':
+                return cvc5.And(self._cvc5_expr(cpm_con.args))
+            elif cpm_con.name == 'or':
+                return cvc5.Or(self._cvc5_expr(cpm_con.args))
+            elif cpm_con.name == '->':
+                return cvc5.Implies(*self._cvc5_expr(cpm_con.args))
+            elif cpm_con.name == 'not':
+                return cvc5.Not(self._cvc5_expr(cpm_con.args[0]))
+
+            # 'sum'/n, 'wsum'/2
+            elif cpm_con.name == 'sum':
+                # Check for boolean variables and replace with auxiliary integer variables
+                cvc5_args = []
+                for arg in cpm_con.args:
+                    cvc5_arg = self._cvc5_expr(arg)
+                    # Check if this is a boolean variable that needs to be converted
+                    if isinstance(cvc5_arg, cvc5.BoolRef):
+                        # Create auxiliary integer variable with domain [0, 1]
+                        aux_var_name = f"__bool_aux_{arg}"
+                        aux_int_var = cvc5.Int(aux_var_name)
+                        # Add bounds constraint
+                        self.cvc5_solver.add(aux_int_var >= 0)
+                        self.cvc5_solver.add(aux_int_var <= 1)
+                        # Add channeling constraint: bool_var ↔ (aux_int_var == 1)
+                        # This is equivalent to: (bool_var → aux_int_var == 1) ∧ (~bool_var → aux_int_var == 0)
+                        self.cvc5_solver.add(cvc5.Implies(cvc5_arg, aux_int_var == 1))
+                        self.cvc5_solver.add(cvc5.Implies(cvc5.Not(cvc5_arg), aux_int_var == 0))
+                        cvc5_args.append(aux_int_var)
+                    else:
+                        cvc5_args.append(cvc5_arg)
+                return cvc5.Sum(cvc5_args)
+            elif cpm_con.name == 'wsum':
+                w = cpm_con.args[0]
+                # Check for boolean variables in the second argument and replace with auxiliary integer variables
+                cvc5_args = []
+                for arg in cpm_con.args[1]:
+                    cvc5_arg = self._cvc5_expr(arg)
+                    # Check if this is a boolean variable that needs to be converted
+                    if isinstance(cvc5_arg, cvc5.BoolRef):
+                        # Create auxiliary integer variable with domain [0, 1]
+                        aux_var_name = f"__bool_aux_{arg}"
+                        aux_int_var = cvc5.Int(aux_var_name)
+                        # Add bounds constraint
+                        self.cvc5_solver.add(aux_int_var >= 0)
+                        self.cvc5_solver.add(aux_int_var <= 1)
+                        # Add channeling constraint: bool_var ↔ (aux_int_var == 1)
+                        # This is equivalent to: (bool_var → aux_int_var == 1) ∧ (~bool_var → aux_int_var == 0)
+                        self.cvc5_solver.add(cvc5.Implies(cvc5_arg, aux_int_var == 1))
+                        self.cvc5_solver.add(cvc5.Implies(cvc5.Not(cvc5_arg), aux_int_var == 0))
+                        cvc5_args.append(aux_int_var)
+                    else:
+                        cvc5_args.append(cvc5_arg)
+                return cvc5.Sum([wi*xi for wi,xi in zip(w,cvc5_args)])
+
+            # 'sub'/2, 'mul'/2, 'div'/2, 'pow'/2, 'm2od'/2
+            elif arity == 2 or cpm_con.name == "mul":
+                assert len(cpm_con.args) == 2, "Currently only support multiplication with 2 vars"
+                x, y = self._cvc5_expr(cpm_con.args)
+                if isinstance(x, cvc5.BoolRef):
+                    x = cvc5.If(x, 1, 0)
+                if isinstance(y, cvc5.BoolRef):
+                    y = cvc5.If(y, 1, 0)
+
+                if cpm_con.name == 'sub':
+                    return x - y
+                elif cpm_con.name == "mul":
+                    return x * y
+                elif cpm_con.name == "div":
+                    # cvc5 rounds towards negative infinity, need this hack when result is negative
+                    return cvc5.If (cvc5.And(x >= 0, y >= 0), x / y,
+                         cvc5.If (cvc5.And(x <= 0, y <= 0), -x / -y,
+                         cvc5.If (cvc5.And(x >= 0, y <= 0), -(x / -y),
+                         cvc5.If (cvc5.And(x <= 0, y >= 0), -(-x / y), 0))))
+
+                elif cpm_con.name == "pow":
+                    if not is_num(cpm_con.args[1]):
+                        # tricky in cvc5 not all power constraints are decidable
+                        # solver will return 'unknown', even if theory is satisfiable.
+                        # https://stackoverflow.com/questions/70289335/power-and-logarithm-in-z3
+                        # raise error to be consistent with other solvers
+                        raise NotSupportedError(f"CVC5 only supports power constraint with constant exponent, got {cpm_con}")
+                    return x ** y
+                elif cpm_con.name == "mod":
+                    # minimic modulo with integer division (round towards o)
+                    return cvc5.If (cvc5.And(x >= 0), x % y,-(-x % y))
+
+            # '-'/1
+            elif cpm_con.name == "-":
+                if is_boolexpr(cpm_con.args[0]):
+                    return  cvc5.If(self._cvc5_expr(cpm_con.args[0]), 1, 0)
+                return -self._cvc5_expr(cpm_con.args[0])
+
+            else:
+                raise NotImplementedError(f"Operator {cpm_con} not (yet) implemented for CVC5, "
+                                          f"please report on github if you need it")
+
+        # Comparisons (just translate the subexpressions and re-post)
+        elif isinstance(cpm_con, Comparison):
+            lhs, rhs = cpm_con.args
+
+            lhs_bexpr = is_boolexpr(lhs)
+            rhs_bexpr = is_boolexpr(rhs)
+
+            lhs, rhs = self._cvc5_expr(cpm_con.args)
+
+            if cpm_con.name == "==" or cpm_con.name == "!=":
+                # cvc5 supports bool <-> bool comparison but not bool <-> arith
+                if lhs_bexpr and not rhs_bexpr:
+                    # upcast lhs to integer
+                    lhs = cvc5.If(lhs, 1, 0)
+                elif rhs_bexpr and not lhs_bexpr:
+                    # upcase rhs to integer
+                    rhs = cvc5.If(rhs, 1, 0)
+            else:
+                # other comparisons are not supported on boolexpr
+                if lhs_bexpr: # upcast lhs
+                    lhs = cvc5.If(lhs, 1, 0)
+                if rhs_bexpr: # upcase rhs
+                    rhs = cvc5.If(rhs, 1, 0)
+
+            # post the comparison
+            return eval_comparison(cpm_con.name, lhs, rhs)
+
+        # rest: base (Boolean) global constraints
+        elif isinstance(cpm_con, GlobalConstraint):
+            # TODO:
+
+            if cpm_con.name == 'alldifferent':
+                if len(cpm_con.args) > 1:
+                    return cvc5.Distinct(self._cvc5_expr(cpm_con.args))
+                else:
+                    return True
+            elif cpm_con.name == 'xor':
+                cvc5_args = self._cvc5_expr(cpm_con.args)
+                if len(cvc5_args) == 1: # just the arg
+                    return cvc5_args[0]
+                cvc5_cons = cvc5.Xor(cvc5_args[0], cvc5_args[1])
+                for a in cvc5_args[2:]:
+                    cvc5_cons = cvc5.Xor(cvc5_cons, a)
+                return cvc5_cons
+            elif cpm_con.name == 'ite':
+                return cvc5.If(self._cvc5_expr(cpm_con.args[0]), self._cvc5_expr(cpm_con.args[1]),
+                             self._cvc5_expr(cpm_con.args[2]))
+
+            raise ValueError(f"Global constraint {cpm_con} should be decomposed already, please report on github.")
+
+        # a direct constraint, make with cvc5 (will be posted to it by calling function)
+        elif isinstance(cpm_con, DirectConstraint):
+            return cpm_con.callSolver(self, cvc5)
+
+        raise NotImplementedError("CVC5: constraint not (yet) supported", cpm_con)
+
+    # CVC5 currently to does not provide access to unsat cores through the "pythonic" Python API
+    # def get_core(self):
+    #     """
+    #         For use with :func:`s.solve(assumptions=[...]) <solve()>`. Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together.
+
+    #         CPMpy will return only those variables that are False (in the UNSAT core)
+
+    #         Note that there is no guarantee that the core is minimal, though this interface does upon up the possibility to add more advanced Minimal Unsatisfiabile Subset algorithms on top. All contributions welcome!
+    #     """
+    #     assert (self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE), "Can only extract core form UNSAT model"
+    #     assert (len(self.assumption_dict) > 0), "Assumptions must be set using s.solve(assumptions=[...])"
+
+    #     return [self.assumption_dict[cvc5_var] for cvc5_var in self.cvc5_solver.unsat_core()]
+
+
+
diff --git a/cpmpy/solvers/utils.py b/cpmpy/solvers/utils.py
index 6d71e1367..a47a91e24 100644
--- a/cpmpy/solvers/utils.py
+++ b/cpmpy/solvers/utils.py
@@ -32,6 +32,7 @@
 from .cplex import CPM_cplex
 from .pindakaas import CPM_pindakaas
 from .hexaly import CPM_hexaly
+from .cvc5 import CPM_cvc5
 
 def param_combinations(all_params, remaining_keys=None, cur_params=None):
     """
@@ -87,7 +88,8 @@ def base_solvers(cls):
                 ("cpo", CPM_cpo),
                 ("cplex", CPM_cplex),
                 ("pindakaas", CPM_pindakaas),
-                ("hexaly", CPM_hexaly)
+                ("hexaly", CPM_hexaly),
+                ("cvc5", CPM_cvc5)
                ]
 
     @classmethod
diff --git a/docs/api/solvers/cvc5.rst b/docs/api/solvers/cvc5.rst
new file mode 100644
index 000000000..7cc868709
--- /dev/null
+++ b/docs/api/solvers/cvc5.rst
@@ -0,0 +1,7 @@
+CPMpy cvc5 interface (:mod:`cpmpy.solvers.cvc5`)
+=====================================================
+
+.. automodule:: cpmpy.solvers.cvc5
+    :members:
+    :undoc-members:
+    :inherited-members:
\ No newline at end of file
diff --git a/docs/index.rst b/docs/index.rst
index 1cabdd9d9..21d2496c0 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -60,6 +60,11 @@ Supported solvers
      - SAT ASAT ISAT - OPT IOPT
      - pip
      - 
+   * - :doc:`cvc5 <api/solvers/cvc5>`
+     - SMT
+     - SAT
+     - pip
+     - 
    * - :doc:`Gurobi <api/solvers/gurobi>`
      - ILP
      - SAT - OPT IOPT - PAR
diff --git a/gbd_tst.py b/gbd_tst.py
new file mode 100644
index 000000000..9d72d96a7
--- /dev/null
+++ b/gbd_tst.py
@@ -0,0 +1,41 @@
+import cpmpy as cp
+from cpmpy.tools.dataset.problem.jsplib import JSPLibDataset
+from cpmpy.tools.jsplib.parser import read_jsplib, _parse_jsplib, _model_jsplib
+from cpmpy.tools.dimacs import write_dimacs
+import tqdm
+
+from cpmpy.transformations.int2bool import int2bool
+from cpmpy.transformations.decompose_global import decompose_in_tree
+from cpmpy.transformations.flatten_model import flatten_constraint, flatten_model
+from cpmpy.transformations.linearize import linearize_constraint, only_positive_bv, only_positive_coefficients
+from cpmpy.transformations.normalize import simplify_boolean, toplevel_list
+from cpmpy.transformations.reification import only_bv_reifies, only_implies
+
+if __name__ == "__main__":
+
+    dataset = JSPLibDataset(root=".", download=True)
+    for instance, metadata in tqdm.tqdm(dataset):
+        model = read_jsplib(instance)
+
+        cnf_model = cp.Model()
+        csemap = {}
+        encoding = "auto"
+        ivarmap = dict()
+        for cpm_expr in model.constraints:
+            cpm_cons = toplevel_list(cpm_expr)
+            cpm_cons = decompose_in_tree(cpm_cons, csemap=csemap)
+            cpm_cons = simplify_boolean(cpm_cons)
+            cpm_cons = flatten_constraint(cpm_cons, csemap=csemap)  # flat normal form
+            cpm_cons = only_bv_reifies(cpm_cons, csemap=csemap)
+            cpm_cons = only_implies(cpm_cons, csemap=csemap)
+            cpm_cons = linearize_constraint(cpm_cons, csemap=csemap)  # the core of the MIP-linearization
+            cpm_cons = int2bool(cpm_cons, ivarmap, encoding=encoding)
+            cpm_cons = only_positive_coefficients(cpm_cons)
+            cpm_cons = only_positive_bv(cpm_cons, csemap=csemap)
+            cnf_model += (cpm_cons)
+        
+        cnf_model = flatten_model(cnf_model)
+
+        fname = instance + ".dimacs.cnf"
+        write_dimacs(cnf_model, fname)
+        
\ No newline at end of file
diff --git a/setup.py b/setup.py
index 7223d890d..dac36d4a0 100644
--- a/setup.py
+++ b/setup.py
@@ -33,6 +33,7 @@ def get_version(rel_path):
     "pumpkin": ["pumpkin-solver>=0.2.1"],
     "pindakaas": ["pindakaas>=0.2.1"],
     "cplex": ["docplex", "cplex"],
+    "cvc5": ["cvc5"],
 }
 solver_dependencies["all"] = list({pkg for group in solver_dependencies.values() for pkg in group}) 
 
diff --git a/tests/test_solverinterface.py b/tests/test_solverinterface.py
index fcf2b4dbc..e1faa5021 100644
--- a/tests/test_solverinterface.py
+++ b/tests/test_solverinterface.py
@@ -142,6 +142,9 @@ def test_minimize(solver_name):
 
     ivar = intvar(1, 10)
 
+    if solver_name == "cvc5":
+        return # TODO: should be skipped instead, need to rework pytest decorators / markers
+
     try:
         solver.minimize(ivar)
     except NotImplementedError:
@@ -157,7 +160,7 @@ def test_minimize(solver_name):
 def test_maximize(solver_name):
     """Test maximize functionality"""
     solver_class = SolverLookup.lookup(solver_name)
-    if solver_name == "z3":
+    if solver_name == "cvc5":
         return
     solver = solver_class() if solver_name != "z3" else solver_class(subsolver="opt")
 
@@ -303,6 +306,9 @@ def test_has_objective(solver_name):
     except NotImplementedError:
         # Solver doesn't support objectives
         assert not solver.has_objective()
+    except NotSupportedError:
+        # Solver doesn't support objectives
+        assert not solver.has_objective()
 
 @pytest.mark.parametrize("solver_name", SOLVERNAMES)
 @skip_on_missing_pblib(skip_on_exception_only=True)
diff --git a/tests/test_solvers.py b/tests/test_solvers.py
index bb4add10d..0bb9562ea 100644
--- a/tests/test_solvers.py
+++ b/tests/test_solvers.py
@@ -13,6 +13,7 @@
 from cpmpy.solvers.pindakaas import CPM_pindakaas
 from cpmpy.solvers.solver_interface import ExitStatus
 from cpmpy.solvers.z3 import CPM_z3
+from cpmpy.solvers.cvc5 import CPM_cvc5
 from cpmpy.solvers.minizinc import CPM_minizinc
 from cpmpy.solvers.gurobi import CPM_gurobi
 from cpmpy.solvers.exact import CPM_exact
@@ -493,6 +494,38 @@ def test_z3(self):
         s = cp.SolverLookup.get("z3", m)
         self.assertFalse(s.solve()) # upgrade z3 with pip install --upgrade z3-solver
 
+    @pytest.mark.skipif(not CPM_cvc5.supported(),
+                    reason="cvc5 not installed")
+    def test_cvc5(self):
+        bv = cp.boolvar(shape=3)
+        iv = cp.intvar(0, 9, shape=3)
+        # circular 'bigger then', UNSAT
+        m = cp.Model([
+            bv[0].implies(iv[0] > iv[1]),
+            bv[1].implies(iv[1] > iv[2]),
+            bv[2].implies(iv[2] > iv[0])
+        ])
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertFalse(s.solve(assumptions=bv))
+
+        m = cp.Model(~(iv[0] != iv[1]))
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertTrue(s.solve())
+
+        m = cp.Model((iv[0] == 0) & ((iv[0] != iv[1]) == 0))
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertTrue(s.solve())
+
+        m = cp.Model([~bv, ~((iv[0] + abs(iv[1])) == sum(iv))])
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertTrue(s.solve())
+
+        x = cp.intvar(0, 1)
+        m = cp.Model((x >= 0.1) & (x != 1))
+        s = cp.SolverLookup.get("cvc5", m)
+        self.assertFalse(s.solve()) # TODO: same bug as z3?
+
+
     def test_pow(self):
         iv1 = cp.intvar(2,9)
         for i in [0,1,2]:
@@ -956,8 +989,8 @@ def test_incremental_assumptions(self, solver):
         if "assumptions" not in inspect.signature((s.solve)).parameters:
             return # solver does not support solving under assumptions
         
-        if solver == "pysdd":
-            return # not implemented in pysdd
+        if solver == "pysdd" or solver == "cvc5":
+            return # not implemented in pysdd or cvc5
         
         s += x | y
         assert s.solve(assumptions=[x])