From 2bad1e1d32da5e2f2f11aa1cfb2389d7b75799f2 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 23 Mar 2026 16:14:09 +0000
Subject: [PATCH 01/19] Add and test computing a MUS via IIS

---
 cpmpy/tools/explain/mus.py | 48 +++++++++++++++++++++++++++++++++++++-
 tests/test_tools_mus.py    | 16 ++++++++++++-
 2 files changed, 62 insertions(+), 2 deletions(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 6fa385dba..b5238aae5 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -330,6 +330,52 @@ def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="
     """
     return ocus_naive(soft, hard, weights, meta_constraint=True, solver=solver, hs_solver=hs_solver)
 
-   
 
+def mus_iis(soft, hard=[], solver="gurobi", time_limit=None, mem_limit=None):
+    """
+        Compute a MUS using an IIS (Irreducible Inconsistent Subsystem) algorithm.
+
+        Uses indicator variables to group linear constraints so that each CPMpy
+        soft constraint is treated as a group of linear constraints.
+
+        :param soft: soft constraints, list of expressions
+        :param hard: hard constraints, optional, list of expressions
+        :param solver: which ILP solver to use (only 'gurobi' supported)
+        :param time_limit: maximum time in seconds for IIS computation (None = no limit)
+        :param mem_limit: maximum memory in GB for IIS computation (None = no limit)
+    """
+    assert solver == "gurobi", f"Only Gurobi supported as IIS solver, but was given {solver}"
+
+    # Create indicator variables and model with hard + (indicator -> soft)
+    m, soft, assumptions = make_assump_model(soft, hard)
+
+    # Instantiate solver (will check if solver is installed and licensed)
+    s = cp.SolverLookup.get(solver, m)
+    grb_model = s.grb_model
+
+    # Force all hard constraints into the IIS (1 = force in, 0 = force out, -1 (default) = soft)
+    grb_model.update()
+    for hard_constraint in grb_model.getConstrs():
+        hard_constraint.IISConstrForce = 1
+    for hard_constraint in grb_model.getGenConstrs():
+        hard_constraint.IISGenConstrForce = 1
+
+    # Add all assumptions (and thus each group) as soft constraints
+    for assumption in assumptions:
+        grb_assumption = s.solver_var(assumption)
+        grb_model.addConstr(grb_assumption >= 1, name=assumption.name)
+
+    # Safe to import gurobipy since instantiating the Gurobi solver succeeded
+    import gurobipy
+    if time_limit is not None:
+        grb_model.Params.TimeLimit = time_limit
+    try:
+        grb_model.computeIIS()
+    except gurobipy.GurobiError as e:
+        if e.errno == gurobipy.GRB.Error.IIS_NOT_INFEASIBLE:
+            raise AssertionError("MUS: model must be UNSAT")
+        raise
+
+    # Find which assumption is in the IIS/MUS
+    return [con for assumption, con in zip(assumptions, soft) if grb_model.getConstrByName(assumption.name).IISConstr]
 
diff --git a/tests/test_tools_mus.py b/tests/test_tools_mus.py
index 0c5215754..3f331fd9a 100644
--- a/tests/test_tools_mus.py
+++ b/tests/test_tools_mus.py
@@ -2,7 +2,7 @@
 
 import cpmpy as cp
 from cpmpy.tools import mss_opt, marco, OCUSException
-from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs, ocus, ocus_naive
+from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs, ocus, ocus_naive, mus_iis
 
 
 class TestMus:
@@ -84,6 +84,20 @@ def test_wglobal(self):
         assert not cp.Model(ms).solve()
         # self.assertEqual(set(self.naive_func(cons)), set(cons[:2]))
 
+    def test_decomposed_global(self):
+        x = cp.intvar(1, 5, shape=3, name="x")
+        soft = [x[0] == x[1], x[1] == x[2]]
+        hard = [cp.AllDifferent(x)]
+
+        mus_cons = self.mus_func(soft=soft, hard=hard)
+        assert len(set(mus_cons)) == 1
+        mus_naive_cons = self.naive_func(soft=soft, hard=hard)
+        assert len(set(mus_naive_cons)) == 1
+
+class TestIIS(TestMus):
+    def setup_method(self):
+        self.mus_func = lambda soft, hard=[], solver="ortools": mus_iis(soft, hard=hard)
+        self.naive_func = mus_naive
 
 class TestQuickXplain(TestMus):
 

From e06c6927aaf979fea7e699a09e7cb68719b398b0 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 23 Mar 2026 16:27:45 +0000
Subject: [PATCH 02/19] Add missing mem limit param

---
 cpmpy/tools/explain/mus.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index b5238aae5..50d540976 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -369,6 +369,8 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None, mem_limit=None):
     import gurobipy
     if time_limit is not None:
         grb_model.Params.TimeLimit = time_limit
+    if mem_limit is not None:
+        grb_model.Params.MemLimit = mem_limit
     try:
         grb_model.computeIIS()
     except gurobipy.GurobiError as e:

From 6bd835ae3c2373dbce58e59398b9a24c920476df Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 23 Mar 2026 16:30:56 +0000
Subject: [PATCH 03/19] Remove mem_limit for simplicity

---
 cpmpy/tools/explain/mus.py | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 50d540976..b5421f136 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -331,7 +331,7 @@ def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="
     return ocus_naive(soft, hard, weights, meta_constraint=True, solver=solver, hs_solver=hs_solver)
 
 
-def mus_iis(soft, hard=[], solver="gurobi", time_limit=None, mem_limit=None):
+def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     """
         Compute a MUS using an IIS (Irreducible Inconsistent Subsystem) algorithm.
 
@@ -342,7 +342,6 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None, mem_limit=None):
         :param hard: hard constraints, optional, list of expressions
         :param solver: which ILP solver to use (only 'gurobi' supported)
         :param time_limit: maximum time in seconds for IIS computation (None = no limit)
-        :param mem_limit: maximum memory in GB for IIS computation (None = no limit)
     """
     assert solver == "gurobi", f"Only Gurobi supported as IIS solver, but was given {solver}"
 
@@ -369,8 +368,6 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None, mem_limit=None):
     import gurobipy
     if time_limit is not None:
         grb_model.Params.TimeLimit = time_limit
-    if mem_limit is not None:
-        grb_model.Params.MemLimit = mem_limit
     try:
         grb_model.computeIIS()
     except gurobipy.GurobiError as e:

From 2bbfaa2f89728b6a1c794f9f971a8e1add2e2da2 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 23 Mar 2026 16:51:42 +0000
Subject: [PATCH 04/19] Remove unneeded update

---
 cpmpy/tools/explain/mus.py | 1 -
 1 file changed, 1 deletion(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index b5421f136..d67c7efdd 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -353,7 +353,6 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     grb_model = s.grb_model
 
     # Force all hard constraints into the IIS (1 = force in, 0 = force out, -1 (default) = soft)
-    grb_model.update()
     for hard_constraint in grb_model.getConstrs():
         hard_constraint.IISConstrForce = 1
     for hard_constraint in grb_model.getGenConstrs():

From ecb0c2118fa902e9641d28f889d07e657afb8c31 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 23 Mar 2026 16:51:59 +0000
Subject: [PATCH 05/19] Refactor how assumptions are added to Gurobi

---
 cpmpy/tools/explain/mus.py | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index d67c7efdd..c7d947f37 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -358,10 +358,12 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     for hard_constraint in grb_model.getGenConstrs():
         hard_constraint.IISGenConstrForce = 1
 
-    # Add all assumptions (and thus each group) as soft constraints
-    for assumption in assumptions:
-        grb_assumption = s.solver_var(assumption)
-        grb_model.addConstr(grb_assumption >= 1, name=assumption.name)
+    # Add each assumption as a single soft constraint which enables its group
+    # We use Gurobi directly here (as opposed to e.g. `s+=a>=1`) in order to gain access to the returned Gurobi constraints
+    grb_assumptions = grb_model.addConstrs(s.solver_var(a) >= 1 for a in assumptions)
+
+    # Gurobi returns its own `tupledict`; we only need the constraints/values
+    grb_assumptions = grb_assumptions.values()
 
     # Safe to import gurobipy since instantiating the Gurobi solver succeeded
     import gurobipy
@@ -375,5 +377,5 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
         raise
 
     # Find which assumption is in the IIS/MUS
-    return [con for assumption, con in zip(assumptions, soft) if grb_model.getConstrByName(assumption.name).IISConstr]
+    return [soft for soft, grb_assumption in zip(soft, grb_assumptions) if grb_assumption.IISConstr]
 

From 213c3d949d12272f60e251cf5b1ad703c64ce6ea Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Tue, 24 Mar 2026 10:04:52 +0000
Subject: [PATCH 06/19] Add missing update to fix bug in PR

---
 cpmpy/tools/explain/mus.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index c7d947f37..09a0b00e8 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -353,6 +353,7 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     grb_model = s.grb_model
 
     # Force all hard constraints into the IIS (1 = force in, 0 = force out, -1 (default) = soft)
+    grb_model.update()
     for hard_constraint in grb_model.getConstrs():
         hard_constraint.IISConstrForce = 1
     for hard_constraint in grb_model.getGenConstrs():

From ecd0ad01a4937120de5ecec4918c032d44f72f12 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Tue, 24 Mar 2026 10:05:02 +0000
Subject: [PATCH 07/19] Refactor

---
 cpmpy/tools/explain/mus.py | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 09a0b00e8..29f46a3ee 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -353,18 +353,17 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     grb_model = s.grb_model
 
     # Force all hard constraints into the IIS (1 = force in, 0 = force out, -1 (default) = soft)
-    grb_model.update()
+    # Force also all assumptions `s -> c` for assumption `s` and all constraints `c` in its group
+    grb_model.update()  # update required ; otherwise `getConstrs` can return empty
     for hard_constraint in grb_model.getConstrs():
         hard_constraint.IISConstrForce = 1
-    for hard_constraint in grb_model.getGenConstrs():
+    for hard_constraint in grb_model.getGenConstrs():  # CPMpy also posts general constraints
         hard_constraint.IISGenConstrForce = 1
 
-    # Add each assumption as a single soft constraint which enables its group
+    # Add each assumption as a single soft constraint `s>=1` which activates each constraint `c` in its group via hard constraint `s -> c`
     # We use Gurobi directly here (as opposed to e.g. `s+=a>=1`) in order to gain access to the returned Gurobi constraints
-    grb_assumptions = grb_model.addConstrs(s.solver_var(a) >= 1 for a in assumptions)
-
-    # Gurobi returns its own `tupledict`; we only need the constraints/values
-    grb_assumptions = grb_assumptions.values()
+    # Gurobi returns its own `tupledict`, we just need the constraint (i.e. values)
+    grb_assumptions = grb_model.addConstrs((s.solver_var(assumptions[i]) >= 1 for i in range(len(assumptions)))).values()
 
     # Safe to import gurobipy since instantiating the Gurobi solver succeeded
     import gurobipy

From 6ce518b8f683d13403c84816213afac8ab321153 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Tue, 24 Mar 2026 10:08:17 +0000
Subject: [PATCH 08/19] Skip IIS test if no gurobi

---
 tests/test_tools_mus.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/test_tools_mus.py b/tests/test_tools_mus.py
index 3f331fd9a..95e3c9a0f 100644
--- a/tests/test_tools_mus.py
+++ b/tests/test_tools_mus.py
@@ -94,6 +94,8 @@ def test_decomposed_global(self):
         mus_naive_cons = self.naive_func(soft=soft, hard=hard)
         assert len(set(mus_naive_cons)) == 1
 
+
+@pytest.mark.requires_solver("gurobi")
 class TestIIS(TestMus):
     def setup_method(self):
         self.mus_func = lambda soft, hard=[], solver="ortools": mus_iis(soft, hard=hard)
@@ -233,4 +235,4 @@ def test_circular(self):
             x[3] > x[0],
             (x[3] > x[1]).implies((x[3] > x[2]) & ((x[3] == 3) | (x[1] == x[2])))
         ]
-        assert len(mcs(cons)) == 1
\ No newline at end of file
+        assert len(mcs(cons)) == 1

From 44d4691b6e348227d473ed15926914ca2f9c3470 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Tue, 24 Mar 2026 10:19:30 +0000
Subject: [PATCH 09/19] Polish comments

---
 cpmpy/tools/explain/mus.py | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 29f46a3ee..b5bbf6f5c 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -345,7 +345,7 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     """
     assert solver == "gurobi", f"Only Gurobi supported as IIS solver, but was given {solver}"
 
-    # Create indicator variables and model with hard + (indicator -> soft)
+    # Create assumption variables and model with hard + (assumption -> soft)
     m, soft, assumptions = make_assump_model(soft, hard)
 
     # Instantiate solver (will check if solver is installed and licensed)
@@ -360,13 +360,11 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     for hard_constraint in grb_model.getGenConstrs():  # CPMpy also posts general constraints
         hard_constraint.IISGenConstrForce = 1
 
-    # Add each assumption as a single soft constraint `s>=1` which activates each constraint `c` in its group via hard constraint `s -> c`
-    # We use Gurobi directly here (as opposed to e.g. `s+=a>=1`) in order to gain access to the returned Gurobi constraints
-    # Gurobi returns its own `tupledict`, we just need the constraint (i.e. values)
+    # Add each assumption as a soft constraint `s>=1` using Gurobi directly (as opposed to e.g. `s+=assumptions`), in order to gain access to the returned Gurobi constraints so we can access their `IISConstr` later
+    # Gurobi returns its own `tupledict`, we just need the constraints (i.e. values)
     grb_assumptions = grb_model.addConstrs((s.solver_var(assumptions[i]) >= 1 for i in range(len(assumptions)))).values()
 
-    # Safe to import gurobipy since instantiating the Gurobi solver succeeded
-    import gurobipy
+    import gurobipy  # Safe to import gurobipy since instantiating the Gurobi solver succeeded
     if time_limit is not None:
         grb_model.Params.TimeLimit = time_limit
     try:

From 6e6b9210ee6d2218d22750bec3daff1e24422ffc Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Tue, 24 Mar 2026 10:33:00 +0000
Subject: [PATCH 10/19] Fix time limit behaviour

---
 cpmpy/tools/explain/mus.py | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index b5bbf6f5c..2b815c60e 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -341,9 +341,10 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
         :param soft: soft constraints, list of expressions
         :param hard: hard constraints, optional, list of expressions
         :param solver: which ILP solver to use (only 'gurobi' supported)
-        :param time_limit: maximum time in seconds for IIS computation (None = no limit)
+        :param time_limit: maximum, strictly positive, time limit in seconds for MUS computation (None = no limit). If the time limit is reached, `None` is returned
     """
     assert solver == "gurobi", f"Only Gurobi supported as IIS solver, but was given {solver}"
+    assert time_limit is None or time_limit > 0, f"`time_limit` should be strictly positive but was {time_limit} (note: a `time_limit=0` does not behave consistently with Gurobi)"
 
     # Create assumption variables and model with hard + (assumption -> soft)
     m, soft, assumptions = make_assump_model(soft, hard)
@@ -374,6 +375,11 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
             raise AssertionError("MUS: model must be UNSAT")
         raise
 
+    # Check if IIS is minimal (IISMinimal=1) or time limit was reached (IISMinimal=0)
+    if not grb_model.IISMinimal:
+        # TODO we could return a possibly non-minimal unsatisfiable subset (along with some indication) ; but this should be made consistent across MUS algorithms
+        return None  # return `None` (in line with CPMpy solving behaviour)
+
     # Find which assumption is in the IIS/MUS
     return [soft for soft, grb_assumption in zip(soft, grb_assumptions) if grb_assumption.IISConstr]
 

From 0c8ce0cdb04932c73f501637f3b9ce020416d6d1 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Tue, 24 Mar 2026 10:37:25 +0000
Subject: [PATCH 11/19] Refactor

- Comments
- Use `solver_vars`, which may become more performant in the future
---
 cpmpy/tools/explain/mus.py | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 2b815c60e..806e5998a 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -333,15 +333,12 @@ def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="
 
 def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     """
-        Compute a MUS using an IIS (Irreducible Inconsistent Subsystem) algorithm.
-
-        Uses indicator variables to group linear constraints so that each CPMpy
-        soft constraint is treated as a group of linear constraints.
+        Compute a MUS using a MIP solver's native Irreducible Inconsistent Subsystem (IIS) algorithm (MIP equivalent of MUS)
 
         :param soft: soft constraints, list of expressions
         :param hard: hard constraints, optional, list of expressions
-        :param solver: which ILP solver to use (only 'gurobi' supported)
-        :param time_limit: maximum, strictly positive, time limit in seconds for MUS computation (None = no limit). If the time limit is reached, `None` is returned
+        :param solver: which ILP solver to use (only `gurobi` supported)
+        :param time_limit: strictly positive time limit in seconds for MUS computation (None = no limit). If the time limit is reached, `None` is returned
     """
     assert solver == "gurobi", f"Only Gurobi supported as IIS solver, but was given {solver}"
     assert time_limit is None or time_limit > 0, f"`time_limit` should be strictly positive but was {time_limit} (note: a `time_limit=0` does not behave consistently with Gurobi)"
@@ -353,21 +350,21 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     s = cp.SolverLookup.get(solver, m)
     grb_model = s.grb_model
 
-    # Force all hard constraints into the IIS (1 = force in, 0 = force out, -1 (default) = soft)
-    # Force also all assumptions `s -> c` for assumption `s` and all constraints `c` in its group
+    # Force all hard constraints into the IIS (1 = force in, 0 = force out, -1 (default) = soft), as well as all `a -> c` for each assumption `a` and constraint `c` of each group/soft constraint in `soft`
     grb_model.update()  # update required ; otherwise `getConstrs` can return empty
     for hard_constraint in grb_model.getConstrs():
         hard_constraint.IISConstrForce = 1
     for hard_constraint in grb_model.getGenConstrs():  # CPMpy also posts general constraints
         hard_constraint.IISGenConstrForce = 1
 
-    # Add each assumption as a soft constraint `s>=1` using Gurobi directly (as opposed to e.g. `s+=assumptions`), in order to gain access to the returned Gurobi constraints so we can access their `IISConstr` later
+    # Add each assumption as a soft constraint `a>=1` using Gurobi directly (as opposed to e.g. `s+=assumptions`), in order to gain access to the returned Gurobi constraints so we can access their `IISConstr` later
     # Gurobi returns its own `tupledict`, we just need the constraints (i.e. values)
-    grb_assumptions = grb_model.addConstrs((s.solver_var(assumptions[i]) >= 1 for i in range(len(assumptions)))).values()
+    grb_assumptions = grb_model.addConstrs(a >= 1 for a in s.solver_vars(assumptions)).values()
 
-    import gurobipy  # Safe to import gurobipy since instantiating the Gurobi solver succeeded
     if time_limit is not None:
         grb_model.Params.TimeLimit = time_limit
+
+    import gurobipy  # Safe to import gurobipy since instantiating the Gurobi solver succeeded
     try:
         grb_model.computeIIS()
     except gurobipy.GurobiError as e:

From eeddc3d37064a697dcfb6827be9e1755bba0b05e Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Tue, 24 Mar 2026 11:42:53 +0000
Subject: [PATCH 12/19] Remove time limit

---
 cpmpy/tools/explain/mus.py | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 806e5998a..407bea8aa 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -331,17 +331,15 @@ def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="
     return ocus_naive(soft, hard, weights, meta_constraint=True, solver=solver, hs_solver=hs_solver)
 
 
-def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
+def mus_iis(soft, hard=[], solver="gurobi"):
     """
         Compute a MUS using a MIP solver's native Irreducible Inconsistent Subsystem (IIS) algorithm (MIP equivalent of MUS)
 
         :param soft: soft constraints, list of expressions
         :param hard: hard constraints, optional, list of expressions
         :param solver: which ILP solver to use (only `gurobi` supported)
-        :param time_limit: strictly positive time limit in seconds for MUS computation (None = no limit). If the time limit is reached, `None` is returned
     """
     assert solver == "gurobi", f"Only Gurobi supported as IIS solver, but was given {solver}"
-    assert time_limit is None or time_limit > 0, f"`time_limit` should be strictly positive but was {time_limit} (note: a `time_limit=0` does not behave consistently with Gurobi)"
 
     # Create assumption variables and model with hard + (assumption -> soft)
     m, soft, assumptions = make_assump_model(soft, hard)
@@ -361,9 +359,6 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
     # Gurobi returns its own `tupledict`, we just need the constraints (i.e. values)
     grb_assumptions = grb_model.addConstrs(a >= 1 for a in s.solver_vars(assumptions)).values()
 
-    if time_limit is not None:
-        grb_model.Params.TimeLimit = time_limit
-
     import gurobipy  # Safe to import gurobipy since instantiating the Gurobi solver succeeded
     try:
         grb_model.computeIIS()
@@ -372,11 +367,6 @@ def mus_iis(soft, hard=[], solver="gurobi", time_limit=None):
             raise AssertionError("MUS: model must be UNSAT")
         raise
 
-    # Check if IIS is minimal (IISMinimal=1) or time limit was reached (IISMinimal=0)
-    if not grb_model.IISMinimal:
-        # TODO we could return a possibly non-minimal unsatisfiable subset (along with some indication) ; but this should be made consistent across MUS algorithms
-        return None  # return `None` (in line with CPMpy solving behaviour)
-
     # Find which assumption is in the IIS/MUS
     return [soft for soft, grb_assumption in zip(soft, grb_assumptions) if grb_assumption.IISConstr]
 

From d1653c7b6154a11840ec4831c6a156018ad91adf Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Wed, 25 Mar 2026 15:08:37 +0000
Subject: [PATCH 13/19] Fix "variable has not been added to model"

---
 cpmpy/tools/explain/mus.py | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 407bea8aa..223cd7328 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -357,7 +357,11 @@ def mus_iis(soft, hard=[], solver="gurobi"):
 
     # Add each assumption as a soft constraint `a>=1` using Gurobi directly (as opposed to e.g. `s+=assumptions`), in order to gain access to the returned Gurobi constraints so we can access their `IISConstr` later
     # Gurobi returns its own `tupledict`, we just need the constraints (i.e. values)
-    grb_assumptions = grb_model.addConstrs(a >= 1 for a in s.solver_vars(assumptions)).values()
+
+    # Get solver variables first and update model to register any newly created variables
+    solver_assumptions = s.solver_vars(assumptions)
+    grb_model.update()
+    grb_assumptions = grb_model.addConstrs(a >= 1 for a in solver_assumptions).values()
 
     import gurobipy  # Safe to import gurobipy since instantiating the Gurobi solver succeeded
     try:

From 6095badda69085cdb00811d2763c8143b2814d08 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Wed, 25 Mar 2026 15:32:47 +0000
Subject: [PATCH 14/19] Update doc

---
 cpmpy/solvers/gurobi.py    | 1 +
 cpmpy/tools/explain/mus.py | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py
index 26fc3bda4..cff1aa5b1 100644
--- a/cpmpy/solvers/gurobi.py
+++ b/cpmpy/solvers/gurobi.py
@@ -320,6 +320,7 @@ def _make_numexpr(self, cpm_expr):
             Used especially to post an expression as objective function
         """
         import gurobipy as gp
+        print(cpm_expr, cpm_expr.name)
 
         if is_num(cpm_expr):
             return cpm_expr
diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 223cd7328..2f7957aad 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -1,9 +1,10 @@
 """
-    Re-impementation of MUS-computation techniques in CPMPy
+    Re-implementation of MUS-computation techniques in CPMPy
 
     - Deletion-based MUS
     - QuickXplain
     - Optimal MUS
+    - IIS-based MUS extraction
 """
 import warnings
 import numpy as np

From 2f4373fb37ef8df0177555ce67a25210c6a7eecb Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 30 Mar 2026 14:43:25 +0000
Subject: [PATCH 15/19] Rm print

---
 cpmpy/solvers/gurobi.py | 1 -
 1 file changed, 1 deletion(-)

diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py
index cff1aa5b1..26fc3bda4 100644
--- a/cpmpy/solvers/gurobi.py
+++ b/cpmpy/solvers/gurobi.py
@@ -320,7 +320,6 @@ def _make_numexpr(self, cpm_expr):
             Used especially to post an expression as objective function
         """
         import gurobipy as gp
-        print(cpm_expr, cpm_expr.name)
 
         if is_num(cpm_expr):
             return cpm_expr

From 57d3e27faf77d4816e87cb811655cfdc04f5fa50 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 30 Mar 2026 14:43:35 +0000
Subject: [PATCH 16/19] MIP-> ILP in MUS

---
 cpmpy/tools/explain/mus.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py
index 2f7957aad..4899e277e 100644
--- a/cpmpy/tools/explain/mus.py
+++ b/cpmpy/tools/explain/mus.py
@@ -334,7 +334,7 @@ def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="
 
 def mus_iis(soft, hard=[], solver="gurobi"):
     """
-        Compute a MUS using a MIP solver's native Irreducible Inconsistent Subsystem (IIS) algorithm (MIP equivalent of MUS)
+        Compute a MUS using a ILP solver's native Irreducible Inconsistent Subsystem (IIS) algorithm (ILP term equivalent to MUS)
 
         :param soft: soft constraints, list of expressions
         :param hard: hard constraints, optional, list of expressions

From 7c7505e5b1ae4262b9501938c5a92ad6e6c35313 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 30 Mar 2026 14:45:59 +0000
Subject: [PATCH 17/19] Change MIP->ILP more project wide

---
 cpmpy/expressions/globalfunctions.py | 4 ++--
 cpmpy/solvers/cplex.py               | 6 +++---
 cpmpy/solvers/exact.py               | 2 +-
 cpmpy/solvers/gurobi.py              | 4 ++--
 cpmpy/solvers/pysat.py               | 2 +-
 docs/modeling.md                     | 2 +-
 6 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py
index 3072c94dc..b2ca1d250 100644
--- a/cpmpy/expressions/globalfunctions.py
+++ b/cpmpy/expressions/globalfunctions.py
@@ -312,7 +312,7 @@ class Multiplication(GlobalFunction):
     Computes the product of two expressions: `x * y`.
 
     Created when the user writes ``*`` with at least one variable (e.g. ``x * y``, ``2 * x``).
-    Supports decomposition into linear constraints for MIP solvers via :meth:`decompose`.
+    Supports decomposition into linear constraints for ILP solvers via :meth:`decompose`.
     """
 
     def __init__(self, x: ExprLike, y: ExprLike):
@@ -379,7 +379,7 @@ def get_bounds(self) -> tuple[int, int]:
 
     def decompose(self) -> tuple[Expression, list[Expression]]:
         """
-        Decomposition of Multiplication into linear constraints (e.g. for MIP).
+        Decomposition of Multiplication into linear constraints (e.g. for ILP).
 
         - If is_lhs_num (const*expr): returns the wsum equivalent and no extra constraints.
         - If both args are Boolean (0/1): bv*bv equals bv&bv (logical AND), so returns that and no extra constraints.
diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py
index 91ad93aa0..f14da239c 100644
--- a/cpmpy/solvers/cplex.py
+++ b/cpmpy/solvers/cplex.py
@@ -376,7 +376,7 @@ def transform(self, cpm_expr):
         :return: list of Expression
         """
         # apply transformations, then post internally
-        # expressions have to be linearized to fit in MIP model. See /transformations/linearize
+        # expressions have to be linearized to fit in ILP model. See /transformations/linearize
         cpm_cons = toplevel_list(cpm_expr)
         cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div", "element"})  # linearize and decompose expect safe exprs
         cpm_cons = decompose_linear(cpm_cons,
@@ -491,7 +491,7 @@ def add(self, cpm_expr_orig):
     def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]):
         """
         CPLEX supports warmstarting the solver with a (in)feasible solution.
-        This is done using MIP starts which provide the solver with a starting point
+        This is done using ILP starts which provide the solver with a starting point
         for the branch-and-bound algorithm.
 
         The solution hint does NOT need to satisfy all constraints, it should just provide 
@@ -514,7 +514,7 @@ def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]):
         
         self.cplex_model.clear_mip_starts()
 
-        # Create a MIP start solution using the proper docplex API
+        # Create a ILP start solution using the proper docplex API
         if len(cpm_vars) > 0:
             warmstart = self.cplex_model.new_solution()
             for cpm_var, val in zip(cpm_vars, vals):
diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py
index 0a1f592c9..6b34fc072 100644
--- a/cpmpy/solvers/exact.py
+++ b/cpmpy/solvers/exact.py
@@ -523,7 +523,7 @@ def transform(self, cpm_expr):
         cpm_cons = linearize_reified_variables(cpm_cons, min_values=2, csemap=self._csemap)
         cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap)
         cpm_cons = only_implies(cpm_cons, csemap=self._csemap)  # anything that can create full reif should go above...
-        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum","->","mul"}), csemap=self._csemap)  # the core of the MIP-linearization
+        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum","->","mul"}), csemap=self._csemap)  # the core of the ILP-linearization
         cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap)  # after linearisation, rewrite ~bv into 1-bv
 
         return cpm_cons
diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py
index 26fc3bda4..c25b5ce20 100644
--- a/cpmpy/solvers/gurobi.py
+++ b/cpmpy/solvers/gurobi.py
@@ -355,7 +355,7 @@ def transform(self, cpm_expr):
             :return: list of Expression
         """
         # apply transformations, then post internally
-        # expressions have to be linearized to fit in MIP model. See /transformations/linearize
+        # expressions have to be linearized to fit in ILP model. See /transformations/linearize
         cpm_cons = toplevel_list(cpm_expr)
         cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div", "element"})  # linearize and decompose expect safe exprs
         cpm_cons = decompose_linear(cpm_cons,
@@ -369,7 +369,7 @@ def transform(self, cpm_expr):
         cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap)
         cpm_cons = only_implies(cpm_cons, csemap=self._csemap)  # anything that can create full reif should go above...
         # gurobi does not round towards zero, so no 'div' in supported set: https://github.com/CPMpy/cpmpy/pull/593#issuecomment-2786707188
-        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","->","sub","min","max","mul","abs","pow"}), csemap=self._csemap)  # the core of the MIP-linearization
+        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","->","sub","min","max","mul","abs","pow"}), csemap=self._csemap)  # the core of the ILP-linearization
         cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap)  # after linearization, rewrite ~bv into 1-bv
         return cpm_cons
 
diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py
index 59c3130ec..4c7f49491 100644
--- a/cpmpy/solvers/pysat.py
+++ b/cpmpy/solvers/pysat.py
@@ -374,7 +374,7 @@ def transform(self, cpm_expr):
         cpm_cons = linearize_reified_variables(cpm_cons, min_values=2, csemap=self._csemap, ivarmap=self.ivarmap)
         cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap)
         cpm_cons = only_implies(cpm_cons, csemap=self._csemap)
-        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum", "->", "and", "or"}), csemap=self._csemap)  # the core of the MIP-linearization
+        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum", "->", "and", "or"}), csemap=self._csemap)  # the core of the ILP-linearization
         cpm_cons = int2bool(cpm_cons, self.ivarmap, encoding=self.encoding, csemap=self._csemap)
         cpm_cons = only_positive_coefficients(cpm_cons)
         return cpm_cons
diff --git a/docs/modeling.md b/docs/modeling.md
index 314fa5bc2..4ed894adb 100644
--- a/docs/modeling.md
+++ b/docs/modeling.md
@@ -512,9 +512,9 @@ If that is not sufficient or you want to debug an unexpected (non)solution, have
 
 ## Selecting a solver
 
-The default solver is [OR-Tools CP-SAT](https://developers.google.com/optimization), an award winning constraint solver. But CPMpy supports multiple other solvers: a MIP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language.
 
 
+The default solver is [OR-Tools CP-SAT](https://developers.google.com/optimization), an award winning constraint solver. But CPMpy supports multiple other solvers: an ILP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language.
 
 The list of supported solver interfaces can be found in [the API documentation](./api/solvers.rst) or by using the following:
 

From 1c8bec7eae5e79741e4af775556e826520742495 Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Mon, 30 Mar 2026 14:49:05 +0000
Subject: [PATCH 18/19] Change ghost solver

---
 tests/test_tools_mus.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/test_tools_mus.py b/tests/test_tools_mus.py
index 95e3c9a0f..0d7c02be3 100644
--- a/tests/test_tools_mus.py
+++ b/tests/test_tools_mus.py
@@ -98,7 +98,7 @@ def test_decomposed_global(self):
 @pytest.mark.requires_solver("gurobi")
 class TestIIS(TestMus):
     def setup_method(self):
-        self.mus_func = lambda soft, hard=[], solver="ortools": mus_iis(soft, hard=hard)
+        self.mus_func = lambda soft, hard=[], solver="gurobi": mus_iis(soft, hard=hard, solver="gurobi")
         self.naive_func = mus_naive
 
 class TestQuickXplain(TestMus):

From 2c689f80515dc35d7e4061bdf57e5f7f405de60f Mon Sep 17 00:00:00 2001
From: Hendrik 'Henk' Bierlee <bierlee.henk@gmail.com>
Date: Wed, 1 Apr 2026 09:57:07 +0000
Subject: [PATCH 19/19] Revert "Change MIP->ILP more project wide"

This reverts commit 7c7505e5b1ae4262b9501938c5a92ad6e6c35313.
---
 cpmpy/expressions/globalfunctions.py | 4 ++--
 cpmpy/solvers/cplex.py               | 6 +++---
 cpmpy/solvers/exact.py               | 2 +-
 cpmpy/solvers/gurobi.py              | 4 ++--
 cpmpy/solvers/pysat.py               | 2 +-
 docs/modeling.md                     | 2 +-
 6 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py
index 8923bb4e2..13abe4efa 100644
--- a/cpmpy/expressions/globalfunctions.py
+++ b/cpmpy/expressions/globalfunctions.py
@@ -312,7 +312,7 @@ class Multiplication(GlobalFunction):
     Computes the product of two expressions: `x * y`.
 
     Created when the user writes ``*`` with at least one variable (e.g. ``x * y``, ``2 * x``).
-    Supports decomposition into linear constraints for ILP solvers via :meth:`decompose`.
+    Supports decomposition into linear constraints for MIP solvers via :meth:`decompose`.
     """
 
     def __init__(self, x: ExprLike, y: ExprLike):
@@ -379,7 +379,7 @@ def get_bounds(self) -> tuple[int, int]:
 
     def decompose(self) -> tuple[Expression, list[Expression]]:
         """
-        Decomposition of Multiplication into linear constraints (e.g. for ILP).
+        Decomposition of Multiplication into linear constraints (e.g. for MIP).
 
         - If is_lhs_num (const*expr): returns the wsum equivalent and no extra constraints.
         - If both args are Boolean (0/1): bv*bv equals bv&bv (logical AND), so returns that and no extra constraints.
diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py
index bde9a0282..5b0e0e1bb 100644
--- a/cpmpy/solvers/cplex.py
+++ b/cpmpy/solvers/cplex.py
@@ -376,7 +376,7 @@ def transform(self, cpm_expr):
         :return: list of Expression
         """
         # apply transformations, then post internally
-        # expressions have to be linearized to fit in ILP model. See /transformations/linearize
+        # expressions have to be linearized to fit in MIP model. See /transformations/linearize
         cpm_cons = toplevel_list(cpm_expr)
         cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div", "element"})  # linearize and decompose expect safe exprs
         cpm_cons = decompose_linear(cpm_cons,
@@ -491,7 +491,7 @@ def add(self, cpm_expr_orig):
     def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]):
         """
         CPLEX supports warmstarting the solver with a (in)feasible solution.
-        This is done using ILP starts which provide the solver with a starting point
+        This is done using MIP starts which provide the solver with a starting point
         for the branch-and-bound algorithm.
 
         The solution hint does NOT need to satisfy all constraints, it should just provide 
@@ -514,7 +514,7 @@ def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]):
         
         self.cplex_model.clear_mip_starts()
 
-        # Create a ILP start solution using the proper docplex API
+        # Create a MIP start solution using the proper docplex API
         if len(cpm_vars) > 0:
             warmstart = self.cplex_model.new_solution()
             for cpm_var, val in zip(cpm_vars, vals):
diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py
index 0c48c420c..93f745020 100644
--- a/cpmpy/solvers/exact.py
+++ b/cpmpy/solvers/exact.py
@@ -524,7 +524,7 @@ def transform(self, cpm_expr):
         cpm_cons = linearize_reified_variables(cpm_cons, min_values=2, csemap=self._csemap)
         cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap)
         cpm_cons = only_implies(cpm_cons, csemap=self._csemap)  # anything that can create full reif should go above...
-        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum","->","mul"}), csemap=self._csemap)  # the core of the ILP-linearization
+        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum","->","mul"}), csemap=self._csemap)  # the core of the MIP-linearization
         cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap)  # after linearisation, rewrite ~bv into 1-bv
 
         return cpm_cons
diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py
index 0a7be69e0..229806403 100644
--- a/cpmpy/solvers/gurobi.py
+++ b/cpmpy/solvers/gurobi.py
@@ -355,7 +355,7 @@ def transform(self, cpm_expr):
             :return: list of Expression
         """
         # apply transformations, then post internally
-        # expressions have to be linearized to fit in ILP model. See /transformations/linearize
+        # expressions have to be linearized to fit in MIP model. See /transformations/linearize
         cpm_cons = toplevel_list(cpm_expr)
         cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div", "element"})  # linearize and decompose expect safe exprs
         cpm_cons = decompose_linear(cpm_cons,
@@ -369,7 +369,7 @@ def transform(self, cpm_expr):
         cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap)
         cpm_cons = only_implies(cpm_cons, csemap=self._csemap)  # anything that can create full reif should go above...
         # gurobi does not round towards zero, so no 'div' in supported set: https://github.com/CPMpy/cpmpy/pull/593#issuecomment-2786707188
-        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","->","sub","min","max","mul","abs","pow"}), csemap=self._csemap)  # the core of the ILP-linearization
+        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","->","sub","min","max","mul","abs","pow"}), csemap=self._csemap)  # the core of the MIP-linearization
         cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap)  # after linearization, rewrite ~bv into 1-bv
         return cpm_cons
 
diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py
index 4c7f49491..59c3130ec 100644
--- a/cpmpy/solvers/pysat.py
+++ b/cpmpy/solvers/pysat.py
@@ -374,7 +374,7 @@ def transform(self, cpm_expr):
         cpm_cons = linearize_reified_variables(cpm_cons, min_values=2, csemap=self._csemap, ivarmap=self.ivarmap)
         cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap)
         cpm_cons = only_implies(cpm_cons, csemap=self._csemap)
-        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum", "->", "and", "or"}), csemap=self._csemap)  # the core of the ILP-linearization
+        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum", "->", "and", "or"}), csemap=self._csemap)  # the core of the MIP-linearization
         cpm_cons = int2bool(cpm_cons, self.ivarmap, encoding=self.encoding, csemap=self._csemap)
         cpm_cons = only_positive_coefficients(cpm_cons)
         return cpm_cons
diff --git a/docs/modeling.md b/docs/modeling.md
index 4ed894adb..314fa5bc2 100644
--- a/docs/modeling.md
+++ b/docs/modeling.md
@@ -512,9 +512,9 @@ If that is not sufficient or you want to debug an unexpected (non)solution, have
 
 ## Selecting a solver
 
+The default solver is [OR-Tools CP-SAT](https://developers.google.com/optimization), an award winning constraint solver. But CPMpy supports multiple other solvers: a MIP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language.
 
 
-The default solver is [OR-Tools CP-SAT](https://developers.google.com/optimization), an award winning constraint solver. But CPMpy supports multiple other solvers: an ILP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language.
 
 The list of supported solver interfaces can be found in [the API documentation](./api/solvers.rst) or by using the following: