Repository: CPMpy/cpmpy

Issue:
Inconsistent model/solver status
Calling `.status()` on a CPMpy `Model` or an implementation of `SolverInterface` (like `CPM_ortools`) returns a `SolverStatus` object with two fields: `runtime` and `exitstatus`. This status object is not consistent across solver backends:


|           | Solve()  |  Solve()  | SolveAll()                                                     |
| -------- | -------- | --------- | -------------------------------------------------------------- |
| **Solver**   | **CSP**      | **COP**       | **CSP/COP**                                                            |
| exact    | FEASIBLE | OPTIMAL   | no state created                                               |
| gcs      | FEASIBLE | FEASIBLE | NOT_RUN                                                        |
| gurobi   | FEASIBLE | OPTIMAL   | no state created                                               |
| ortools  | OPTIMAL  | OPTIMAL   | same as Solve()                                                |
| minizinc | FEASIBLE | OPTIMAL   | same as Solve()                                                |
| Z3       | FEASIBLE | OPTIMAL   | UNSATISFIABLE + 0s runtime (solving with blocking constraints) |
| choco    | FEASIBLE | OPTIMAL   | NOT_RUN                                                        |

For the CSP setting, these are clear bugs to be fixed.

For the COP setting, not sure what the state + runtime should be. For the state, most logical seems:
- UNSATISFIABLE if 0 solutions found and returned within time
- UNKNOWN if 0 solutions found and timeout
- SATISFIABLE if at least 1 solution found
- NOT_RUN as default

For the runtime, the total runtime?

Discussion:

Solution patch:
diff --git a/cpmpy/solvers/TEMPLATE.py b/cpmpy/solvers/TEMPLATE.py
index 15079d03..6e859b34 100644
--- a/cpmpy/solvers/TEMPLATE.py
+++ b/cpmpy/solvers/TEMPLATE.py
@@ -151,9 +151,19 @@ class CPM_template(SolverInterface):
         self.cpm_status = SolverStatus(self.name)
         self.cpm_status.runtime = self.TPL_solver.time() # wallclock time in (float) seconds
 
-        # translate solver exit status to CPMpy exit status
+        # Translate solver exit status to CPMpy exit status
+        # CSP:                         COP:
+        # ├─ sat -> FEASIBLE           ├─ optimal -> OPTIMAL
+        # ├─ unsat -> UNSATISFIABLE    ├─ sub-optimal -> FEASIBLE
+        # └─ timeout -> UNKNOWN        ├─ unsat -> UNSATISFIABLE
+        #                              └─ timeout -> UNKNOWN
         if my_status is True:
-            self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            # COP
+            if self.has_objective():
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            # CSP
+            else:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         elif my_status is False:
             self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
         elif my_status is None:
@@ -409,7 +419,7 @@ class CPM_template(SolverInterface):
 
             If the problem is an optimization problem, returns only optimal solutions.
 
-           Arguments:
+            Arguments:
                 - display: either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping
                         default/None: nothing displayed
                 - time_limit: stop after this many seconds (default: None)
@@ -420,7 +430,7 @@ class CPM_template(SolverInterface):
             Returns: number of solutions found
         """
 
-        # check if objective function
+        # check if objective function (optional if solver doesn't support finding all solutions for COP)
         if self.has_objective():
             raise NotSupportedError("TEMPLATE does not support finding all optimal solutions")
 
@@ -430,7 +440,21 @@ class CPM_template(SolverInterface):
         else:
             callback = display
 
-        self.solve(time_limit, callback=callback, enumerate_all_solutions=True, **kwargs)
+        my_status = self.solve(time_limit, callback=callback, enumerate_all_solutions=True, **kwargs)
+
+        # new status, translate runtime
+        self.cpm_status = SolverStatus(self.name)
+        self.cpm_status.runtime = self.TPL_solver.time() # wallclock time in (float) seconds (of entire solveAll call)
+
+        # Translate solver exit status to CPMpy exit status
+        # CSP & COP:
+        # ├─ all solutions found -> OPTIMAL
+        # ├─ at least 1 found (timeout / solution limit reached) -> FEASIBLE
+        # ├─ 0 solutions found due to timeout -> UNKNOWN
+        # └─ unsat -> UNSATISFIABLE
+
+        # self.cpm_status.exitstatus = ...
+
         # clear user vars if no solution found
         if self.TPL_solver.SolutionCount() == 0:
             for var in self.user_vars:
diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py
index 9f941580..ff93ab99 100644
--- a/cpmpy/solvers/choco.py
+++ b/cpmpy/solvers/choco.py
@@ -177,13 +177,21 @@ class CPM_choco(SolverInterface):
         self.cpm_status.runtime = end - start
 
         # translate exit status
+        # A) Found a solution
         if sol is not None:
-            if time_limit is None or self.cpm_status.runtime < time_limit: # solved to optimality
-                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
-            else: # solved, but optimality not proven
+            # COP
+            if self.has_objective():
+                if time_limit is None or self.cpm_status.runtime < time_limit: # solved to optimality
+                    self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+                else: # solved, but optimality not proven
+                    self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            # CSP
+            else:
                 self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+        # B) Found unsat
         elif time_limit is None or self.cpm_status.runtime < time_limit: # proven unsat
             self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+        # C) Timeout
         else:
             self.cpm_status.exitstatus = ExitStatus.UNKNOWN  # can happen when timeout is reached...
 
@@ -228,10 +236,13 @@ class CPM_choco(SolverInterface):
         # ensure all vars are known to solver
         self.solver_vars(list(self.user_vars))
 
+        # create solver object
+        self.chc_solver = self.chc_model.get_solver()
+
+        # set time limit (if given)
         if time_limit is not None:
             self.chc_solver.limit_time(str(time_limit) + "s")
 
-        self.chc_solver = self.chc_model.get_solver()
         start = time.time()
         if self.has_objective():
             sols = self.chc_solver.find_all_optimal_solutions(maximize=not self.minimize_obj,
@@ -246,6 +257,19 @@ class CPM_choco(SolverInterface):
         self.cpm_status = SolverStatus(self.name)
         self.cpm_status.runtime = end - start
 
+        if len(sols): # solutions found
+            if (len(sols) == solution_limit): # matched the set limit (if given)
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            elif (time_limit is None) or (self.cpm_status.runtime < time_limit): # found all solutions
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            else: # reached timeout
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+        else: # no solutions found
+            if (time_limit is None) or (self.cpm_status.runtime < time_limit): # unsat problem
+                self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+            else: # timeout
+                self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+
         # if no solutions, clear values of variables
         if len(sols) == 0:
             for var in self.user_vars:
diff --git a/cpmpy/solvers/cpo.py b/cpmpy/solvers/cpo.py
index 9f38efad..82b70db3 100644
--- a/cpmpy/solvers/cpo.py
+++ b/cpmpy/solvers/cpo.py
@@ -43,6 +43,7 @@
 """
 
 import shutil
+import time
 import warnings
 
 from .solver_interface import SolverInterface, SolverStatus, ExitStatus
@@ -234,14 +235,28 @@ class CPM_cpo(SolverInterface):
 
         docp = self.get_docp()
         solution_count = 0
-        while solution_limit is None or solution_count < solution_limit:
-            cpo_result = self.solve(time_limit=time_limit, **kwargs)
-            if not cpo_result:
-                break
+        start = time.time()
+        while ((time_limit is None) or (time_limit > 0)) and self.solve(time_limit=time_limit, **kwargs):
+
+            # display if needed
+            if display is not None:
+                if isinstance(display, Expression):
+                    print(argval(display))
+                elif isinstance(display, list):
+                    print(argvals(display))
+                else:
+                    display()  # callback
+
+            # count and stop
             solution_count += 1
+            if solution_count == solution_limit:
+                break
+
             if self.has_objective():
                 # only find all optimal solutions
                 self.cpo_model.add(self.cpo_model.get_objective_expression().children[0] == self.objective_value_)
+
+            # add nogood on the user variables
             solvars = []
             vals = []
             for cpm_var in self.user_vars:
@@ -255,13 +270,26 @@ class CPM_cpo(SolverInterface):
                 solvars.append(sol_var)
                 vals.append(cpm_value)
             self.cpo_model.add(docp.modeler.forbidden_assignments(solvars, [vals]))
-            if display is not None:
-                if isinstance(display, Expression):
-                    print(argval(display))
-                elif isinstance(display, list):
-                    print(argvals(display))
-                else:
-                    display()  # callback
+
+            if time_limit is not None: # update remaining time
+                time_limit -= self.status().runtime
+        end = time.time()
+
+        # update solver status
+        self.cpm_status.runtime = end - start
+        if solution_count:
+            if solution_count == solution_limit:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            elif self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE:
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            else:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+        # else: <- is implicit since nothing needs to update
+        #     if self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE:
+        #         self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+        #     elif self.cpm_status.exitstatus == ExitStatus.UNKNOWN:
+        #         self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+
         return solution_count
 
     def solver_var(self, cpm_var):
@@ -471,7 +499,16 @@ class CPM_cpo(SolverInterface):
                 total_usage = []
                 cons = []
                 for s, d, e, h in zip(start, dur, end, height):
-                    cpo_s, cpo_d, cpo_e, cpo_h = self.solver_vars([s, d, e, h])
+                    bounds_d = get_bounds(d)
+                    # Special case for tasks with duration 0
+                    # -> cpo immediately returns UNSAT if done through tasks
+                    if bounds_d[1] == bounds_d[0] == 0:
+                        cpo_s, cpo_e = self.solver_vars([s, e])
+                        cons += [cpo_s == cpo_e] # enforce 0 duration
+                        # no restrictions on height due to zero duration and thus no contribution to capacity
+                        continue
+                    # Normal setting
+                    cpo_s, cpo_d, cpo_e, cpo_h = self.solver_vars([s, d, e, h])                   
                     task = docp.expression.interval_var(start=get_bounds(s), size=get_bounds(d), end=get_bounds(e))
                     task_height = dom.pulse(task, get_bounds(h))
                     cons += [dom.start_of(task) == cpo_s, dom.size_of(task) == cpo_d, dom.end_of(task) == cpo_e]
diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py
index 33a5200f..c2c5cc5e 100644
--- a/cpmpy/solvers/exact.py
+++ b/cpmpy/solvers/exact.py
@@ -217,18 +217,28 @@ class CPM_exact(SolverInterface):
 
         self.objective_value_ = None
         # translate exit status
+        #   see 'toOptimum' documentation:
+        #   https://gitlab.com/nonfiction-software/exact/-/blob/main/src/interface/IntProg.cpp#L877
         if my_status == "UNSAT": # found unsatisfiability
-            if self.has_objective() and self.xct_solver.hasSolution():
+            if self.has_objective() and self.xct_solver.hasSolution(): # optimisation problem -> unsat = no better solution found
                 self.cpm_status.exitstatus = ExitStatus.OPTIMAL
             else:
                 self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
-        elif my_status == "SAT": # found solution, but not optimality proven
+        elif my_status == "SAT": # the optimal value has been found
             assert self.xct_solver.hasSolution()
-            self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            # COP
+            if self.has_objective():
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            # CSP
+            else:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         elif my_status == "INCONSISTENT": # found inconsistency over assumptions
             self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
         elif my_status == "TIMEOUT": # found timeout
-            self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+            if self.xct_solver.hasSolution(): # found a (sub-)optimal solution
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            else: # no solution found
+                self.cpm_status.exitstatus = ExitStatus.UNKNOWN
         else:
             raise NotImplementedError(my_status)  # a new status type was introduced, please report on github
         
@@ -242,6 +252,15 @@ class CPM_exact(SolverInterface):
         # True/False depending on self.cpm_status
         return self._solve_return(self.cpm_status)
 
+    def _update_time(self, timelim, start, end):
+        """
+            Internal helper function to keep track of remaining time.
+        """
+        if timelim != 0:
+            timelim -= (end - start)
+            if timelim == 0: timelim = -1
+        return timelim
+
     def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs):
         """
             Compute all solutions and optionally, display the solutions.
@@ -267,30 +286,52 @@ class CPM_exact(SolverInterface):
 
         timelim = time_limit if time_limit is not None else 0
 
+        total_start = time.time()
+
         if self.has_objective():
+            start = time.time()
             if not call_from_model:
                 warnings.warn("Adding constraints to solver object to find all solutions, solver state will be invalid after this call!")
 
             (my_status, objval) = self.xct_solver.toOptimum(timelim) # fix the solution to the optimal objective
             if my_status == "UNSAT": # found unsatisfiability
+                total_end = time.time()
                 self._fillVars() # erases the solution
+                # update exit status
+                self.cpm_status = SolverStatus(self.name)
+                self.cpm_status.runtime = total_end - total_start
+                self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+                # early exit
                 return 0
             elif my_status == "INCONSISTENT": # found inconsistency
                 raise ValueError("Error: inconsistency during solveAll should not happen, please warn the developers of this bug")
             elif my_status == "TIMEOUT": # found timeout
+                total_end = time.time()
+                # update exit status
+                self.cpm_status = SolverStatus(self.name)
+                self.cpm_status.runtime = total_end - total_start
+                self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+                # early exit
                 return 0
             else:
                 assert my_status == "SAT", "Unexpected status from Exact"
             self += self.objective_ == objval # fix obj val
+            end = time.time()
+            timelim = self._update_time(timelim, start, end) # update remaining time
+
 
         solsfound = 0
-        while solution_limit is None or solsfound < solution_limit:
+        while timelim >= 0 and (solution_limit is None or solsfound < solution_limit):
             # call the solver, with parameters
+            start = time.time()
             my_status = self.xct_solver.runFull(optimize=False, timeout=timelim)
+            end = time.time()
+            timelim = self._update_time(timelim, start, end) # update remaining time
+
             assert my_status in ["UNSAT","SAT","INCONSISTENT","TIMEOUT"], "Unexpected status code for Exact: " + my_status
-            if my_status == "UNSAT": # found unsatisfiability
+            if my_status == "UNSAT": # found unsatisfiability (no more solutions to be found)
                 self._fillVars() # erases the solution
-                return solsfound
+                break
             elif my_status == "SAT": # found solution, but not optimality proven
                 assert self.xct_solver.hasSolution()
                 solsfound += 1
@@ -306,7 +347,27 @@ class CPM_exact(SolverInterface):
             elif my_status == "INCONSISTENT": # found inconsistency
                 raise ValueError("Error: inconsistency during solveAll should not happen, please warn the developers of this bug")
             elif my_status == "TIMEOUT": # found timeout
-                return solsfound
+                break
+        total_end = time.time()
+
+        # new status, translate runtime
+        self.cpm_status = SolverStatus(self.name)
+        self.cpm_status.runtime = total_end - total_start
+
+        if solsfound: # found some solutions
+            if solsfound == solution_limit: # matched solution limit
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            elif my_status == "UNSAT": # found all solutions (before limits were reached)
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            else: # timeout
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+        else:
+            if my_status == "UNSAT": # unsat problem
+                self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+            elif my_status == "TIMEOUT": # timeout
+                self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+            else:
+                raise NotImplementedError(my_status) # please report on GitHub
 
         return solsfound
 
diff --git a/cpmpy/solvers/gcs.py b/cpmpy/solvers/gcs.py
index dbf1fce4..da7b2ec1 100644
--- a/cpmpy/solvers/gcs.py
+++ b/cpmpy/solvers/gcs.py
@@ -303,6 +303,16 @@ class CPM_gcs(SolverInterface):
         self.cpm_status = SolverStatus(self.name)
         self.cpm_status.runtime = self.gcs_result["solve_time"]
 
+        num_sols = self.gcs_result["solutions"]
+        if self.gcs_result["completed"] and num_sols >= 1:
+            self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+        elif self.gcs_result["completed"] and num_sols == 0:
+            self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+        elif num_sols >= 1:
+            self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+        else: # maybe unsat, maybe not (maybe a timeout)
+            self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+
         # clear user vars if no solution found
         if self._solve_return(self.cpm_status, self.objective_value_) is False:
             for var in self.user_vars:
@@ -313,7 +323,7 @@ class CPM_gcs(SolverInterface):
             self.verify(name=self.proof_name, location=proof_location, time_limit=verify_time_limit, 
                         veripb_args=veripb_args, display_output=display_verifier_output)
 
-        return self.gcs_result["solutions"]
+        return num_sols
 
     def solver_var(self, cpm_var):
         """
diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py
index 3aaad500..5d36d397 100644
--- a/cpmpy/solvers/gurobi.py
+++ b/cpmpy/solvers/gurobi.py
@@ -181,10 +181,13 @@ class CPM_gurobi(SolverInterface):
         self.cpm_status.runtime = self.grb_model.runtime
 
         # translate exit status
-        if grb_status == GRB.OPTIMAL and not self.has_objective():
-            self.cpm_status.exitstatus = ExitStatus.FEASIBLE
-        elif grb_status == GRB.OPTIMAL and self.has_objective():
-            self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+        if grb_status == GRB.OPTIMAL:
+            # COP
+            if self.has_objective():
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            # CSP
+            else:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         elif grb_status == GRB.INFEASIBLE:
             self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
         elif grb_status == GRB.TIME_LIMIT:
@@ -477,6 +480,7 @@ class CPM_gurobi(SolverInterface):
 
             Returns: number of solutions found
         """
+        from gurobipy import GRB
 
         if time_limit is not None:
             self.grb_model.setParam("TimeLimit", time_limit)
@@ -537,4 +541,15 @@ class CPM_gurobi(SolverInterface):
         # Reset pool search mode to default
         self.grb_model.setParam("PoolSearchMode", 0)
 
+        if opt_sol_count:
+            if opt_sol_count == solution_limit:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE 
+            else:
+                grb_status = self.grb_model.Status
+                if grb_status == GRB.TIME_LIMIT: # reached time limit
+                    self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+                else: # found all solutions   
+                    self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+        # if unsat or timout with no solution, .solve() will have already set the state accordingly (so nothing to update)
+
         return opt_sol_count
diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py
index f7e8de48..5dd42c62 100644
--- a/cpmpy/solvers/minizinc.py
+++ b/cpmpy/solvers/minizinc.py
@@ -305,7 +305,7 @@ class CPM_minizinc(SolverInterface):
 
         return has_sol
 
-    def _post_solve(self, mzn_result):
+    def _post_solve(self, mzn_result, solve_all:bool=False):
         """ shared by solve() and solveAll() """
         import minizinc
 
@@ -328,7 +328,10 @@ class CPM_minizinc(SolverInterface):
         if mzn_status == minizinc.result.Status.SATISFIED:
             self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         elif mzn_status == minizinc.result.Status.ALL_SOLUTIONS:
-            self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            if solve_all:
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            else:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         elif mzn_status == minizinc.result.Status.OPTIMAL_SOLUTION:
             self.cpm_status.exitstatus = ExitStatus.OPTIMAL
         elif mzn_status == minizinc.result.Status.UNSATISFIABLE:
@@ -402,7 +405,14 @@ class CPM_minizinc(SolverInterface):
                 var._value = None
 
         # status handling
-        self._post_solve(mzn_result)
+        self._post_solve(mzn_result, solve_all=True)
+
+        if solution_count: # found at least one solution
+            if solution_count == solution_limit: # matched solution limit
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            # elif mzn_result.solution is None: <- is implicit since nothing needs to update
+                # last iteration didn't find a solution
+                # nothing needs to update since _post_solve already set state correctly (state from the second-last iteration)
 
         return solution_count
 
diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py
index 764c15f2..66e9f91c 100644
--- a/cpmpy/solvers/ortools.py
+++ b/cpmpy/solvers/ortools.py
@@ -214,7 +214,17 @@ class CPM_ortools(SolverInterface):
         if self.ort_status == ort.FEASIBLE:
             self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         elif self.ort_status == ort.OPTIMAL:
-            self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            # COP
+            if self.has_objective():
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            # CSP
+            else:
+                # for .solveAll(), if all solutions found status is OPTIMAL
+                if kwargs.get("enumerate_all_solutions", False):
+                    self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+                # regular .solve()
+                else:
+                    self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         elif self.ort_status == ort.INFEASIBLE:
             self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
         elif self.ort_status == ort.MODEL_INVALID:
diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py
index e7f6557f..39224a39 100644
--- a/cpmpy/solvers/pysat.py
+++ b/cpmpy/solvers/pysat.py
@@ -220,7 +220,12 @@ class CPM_pysat(SolverInterface):
 
         # translate exit status
         if my_status is True:
-            self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            # COP
+            if self.has_objective():
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            # CSP
+            else:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         elif my_status is False:
             self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
         elif my_status is None:
diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py
index d5c1e1a4..7cf40251 100644
--- a/cpmpy/solvers/pysdd.py
+++ b/cpmpy/solvers/pysdd.py
@@ -135,6 +135,7 @@ class CPM_pysdd(SolverInterface):
 
         # translate exit status
         if has_sol:
+            # Only CSP (does not support COP)
             self.cpm_status.exitstatus = ExitStatus.FEASIBLE
         else:
             self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
@@ -197,27 +198,32 @@ class CPM_pysdd(SolverInterface):
                 projected_sols.add(tuple(projectedsol))
         else:
             projected_sols = set(sddmodels)
-        if display is None:
-            # the desired, fast computation
-            return len(projected_sols)
 
+        if projected_sols:
+            if projected_sols == solution_limit:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            else:
+                # time limit not (yet) supported -> always all solutions found
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
         else:
+            self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+
+        # display if needed
+        if display is not None:
             # manually walking over the tree, much slower...
-            solution_count = 0
             for sol in projected_sols:
-                solution_count += 1
                 # fill in variable values
                 for i, cpm_var in enumerate(self.user_vars):
                     cpm_var._value = sol[i]
 
-                # display is not None:
                 if isinstance(display, Expression):
                     print(argval(display))
                 elif isinstance(display, list):
                     print(argvals(display))
                 else:
                     display()  # callback
-            return solution_count
+        
+        return len(projected_sols)
 
     def solver_var(self, cpm_var):
         """
diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py
index 80e291c4..37205f4e 100644
--- a/cpmpy/solvers/solver_interface.py
+++ b/cpmpy/solvers/solver_interface.py
@@ -251,9 +251,12 @@ class SolverInterface(object):
         if not call_from_model:
             warnings.warn("Adding constraints to solver object to find all solutions, "
                           "solver state will be invalid after this call!")
+            
+        self.cpm_status = SolverStatus(self.name)
 
         solution_count = 0
-        while self.solve(time_limit=time_limit, **kwargs):
+        start = time.time()
+        while ((time_limit is None) or (time_limit > 0)) and self.solve(time_limit=time_limit, **kwargs):
             # display if needed
             if display is not None:
                 if isinstance(display, Expression):
@@ -271,6 +274,25 @@ class SolverInterface(object):
             # add nogood on the user variables
             self += any([v != v.value() for v in self.user_vars if v.value() is not None])
 
+            if time_limit is not None: # update remaining time
+                time_limit -= self.status().runtime
+        end = time.time()
+
+        # update solver status
+        self.cpm_status.runtime = end - start
+        if solution_count:
+            if solution_count == solution_limit:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+            elif self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE:
+                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            else:
+                self.cpm_status.exitstatus = ExitStatus.FEASIBLE
+        # else: <- is implicit since nothing needs to update
+        #     if self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE:
+        #         self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
+        #     elif self.cpm_status.exitstatus == ExitStatus.UNKNOWN:
+        #         self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+
         return solution_count
 
     def solution_hint(self, cpm_vars, vals):
diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py
index 156a9c63..3dd9ed25 100644
--- a/cpmpy/solvers/z3.py
+++ b/cpmpy/solvers/z3.py
@@ -113,6 +113,9 @@ class CPM_z3(SolverInterface):
         if "opt" in subsolver:
             self.z3_solver = z3.Optimize()
 
+        # handle of objective (as returned by solver)
+        self.obj_handle = None
+
         # initialise everything else and post the constraints/objective
         super().__init__(name="z3", cpm_model=cpm_model)
 
@@ -189,14 +192,30 @@ class CPM_z3(SolverInterface):
 
         # translate exit status
         if my_status == "sat":
-            self.cpm_status.exitstatus = ExitStatus.FEASIBLE
-            if isinstance(self.z3_solver, z3.Optimize):
-                self.cpm_status.exitstatus = ExitStatus.OPTIMAL
+            if self.has_objective(): # COP
+                # check if optimal solution found and proven, i.e. bounds are equal
+                lower_bound = self.z3_solver.lower(self.obj_handle)
+                upper_bound = self.z3_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.z3_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...
-            self.cpm_status.exitstatus = ExitStatus.UNKNOWN
+            except z3.Z3Exception 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
 
@@ -286,9 +305,9 @@ class CPM_z3(SolverInterface):
 
         obj = self._z3_expr(expr)
         if minimize:
-            self.z3_solver.minimize(obj)
+            self.obj_handle = self.z3_solver.minimize(obj)
         else:
-            self.z3_solver.maximize(obj)
+            self.obj_handle = self.z3_solver.maximize(obj)
 
 
     def transform(self, cpm_expr):
diff --git a/docs/modeling.md b/docs/modeling.md
index 626d5ab2..68aada79 100644
--- a/docs/modeling.md
+++ b/docs/modeling.md
@@ -436,7 +436,12 @@ if hassol:
 else:
     print("No solution found.")
 ```
-
+The status of solve-call can be the following:
+1. `ExitStatus.OPTIMAL`: The solver found a solution to an optimisation problem and proved its optimality.
+2. `ExitStatus.FEASIBLE`: The solver found a solution to a satisfaction problem, or a feasible solution to an optimization problem but did not prove optimality
+3. `ExitStatus.UNSATIFIABLE`: The solver proved the input problem is unsatisfiable.
+4. `ExitStatus.UNKNOWN`: The solver did not find a feasible solution, nor proved the problem is unsatisfiable. Can happen when a time-limit is reached.
+5. `ExitStatus.NOT_RUN`: The solver is not run yet (default when initializing a solver)
 
 ## Finding all solutions
 
@@ -451,6 +456,13 @@ n = m.solveAll()
 print("Nr of solutions:", n)  # Nr of solutions: 6
 ```
 
+The status of solveAll-call can be the following:
+1. `ExitStatus.OPTIMAL`: The solver found all possible solutions to a problem and proved there to be none remaining.
+2. `ExitStatus.FEASIBLE`: The solver found a subset of all solutions, or found all solutions but did not prove there to be none remaining.
+3. `ExitStatus.UNSATIFIABLE`: The solver proved the input problem is unsatisfiable.
+4. `ExitStatus.UNKNOWN`: The solver did not find a feasible solution, nor proved the problem is unsatisfiable. Can happen when a time-limit is reached.
+5. `ExitStatus.NOT_RUN`: The solver is not run yet (default when initializing a solver)
+
 When using `solveAll()`, a solver will use an optimized native implementation behind the scenes when that exists. Otherwise it will be emulated with an iterative approach, resulting in a performance impact.
 
 It has a `display=...` argument that can be used to display expressions (provide a list of expressions to be evaluated) or as a more generic callback (provide a function), both to be evaluated for each found solution.


Test patch:
diff --git a/tests/test_solvers.py b/tests/test_solvers.py
index ef49a405..5b8d3d50 100644
--- a/tests/test_solvers.py
+++ b/tests/test_solvers.py
@@ -8,6 +8,7 @@ from cpmpy.expressions.core import Operator
 from cpmpy.expressions.utils import argvals
 
 from cpmpy.solvers.pysat import CPM_pysat
+from cpmpy.solvers.solver_interface import ExitStatus
 from cpmpy.solvers.z3 import CPM_z3
 from cpmpy.solvers.minizinc import CPM_minizinc
 from cpmpy.solvers.gurobi import CPM_gurobi
@@ -849,6 +850,85 @@ class TestSupportedSolvers:
             assert (Operator('div', [xv, yv])).value() == dv
             assert (Operator('mod', [xv, yv])).value() == rv
 
+
+    def test_status(self, solver):
+
+        bv = cp.boolvar(shape=3, name="bv")
+        m = cp.Model(cp.any(bv))
+
+        assert m.status().exitstatus == ExitStatus.NOT_RUN
+        assert m.solve(solver=solver)
+        assert m.status().exitstatus == ExitStatus.FEASIBLE
+
+        try: # now try optimization, not supported for all solvers
+            m.maximize(cp.sum(bv))
+            assert m.solve(solver=solver)
+            assert m.status().exitstatus == ExitStatus.OPTIMAL
+        except NotSupportedError:
+            return
+
+        # now making a tricky problem to solve
+        np.random.seed(0)
+        start = cp.intvar(0,100, shape=50)
+        dur = np.random.randint(1,5, size=50)
+        end = cp.intvar(0,100, shape=50)
+        demand  = np.random.randint(10,15, size=50)
+
+        m += cp.Cumulative(start, dur, end,demand, 30)
+        m.minimize(cp.max(end))
+        m.solve(solver=solver, time_limit=1)
+        # normally, should not be able to solve within 1s...
+        assert m.status().exitstatus == ExitStatus.FEASIBLE or m.status().exitstatus == ExitStatus.UNKNOWN
+
+        # now trivally unsat
+        m += cp.sum(bv) <= 0
+        m.solve(solver=solver)
+        assert m.status().exitstatus == ExitStatus.UNSATISFIABLE
+
+
+
+    def test_status_solveall(self, solver):
+
+        bv = cp.boolvar(shape=3, name="bv")
+        m = cp.Model(cp.any(bv))
+
+        limit = None
+        if solver == "gurobi": limit = 100000
+
+        num_sols = m.solveAll(solver=solver, solution_limit=limit)
+        assert num_sols == 7
+        assert m.status().exitstatus == ExitStatus.OPTIMAL  # optimal
+
+
+
+        # adding a bunch of variables to increase nb of sols
+        try:
+            x = cp.boolvar(shape=32, name="x")
+            m = cp.Model(cp.any(x))
+            num_sols = m.solveAll(solver=solver, time_limit=1, solution_limit=limit)
+            assert m.status().exitstatus == ExitStatus.FEASIBLE
+
+            num_sols = m.solveAll(solver=solver, solution_limit=10)
+            assert num_sols == 10
+            assert m.status().exitstatus == ExitStatus.FEASIBLE
+
+            # edge-case: nb of solutions is exactly the sol limit
+            m = cp.Model(cp.any(bv))
+            num_sols = m.solveAll(solver=solver, solution_limit=7)
+            assert num_sols ==  7
+            assert m.status().exitstatus in (ExitStatus.OPTIMAL, ExitStatus.FEASIBLE) # which of the two?
+
+        except NotImplementedError:
+            pass # not all solvers support time/solution limits
+
+        # making the problem unsat
+        if solver != "pysdd": # constraint not supported by pysdd
+            m  = cp.Model([cp.sum(bv) <= 0, cp.any(bv)])
+            num_sols = m.solveAll(solver=solver, solution_limit=limit)
+            assert num_sols == 0
+            assert m.status().exitstatus == ExitStatus.UNSATISFIABLE
+
+
     def test_hidden_user_vars(self, solver):
         """
         Tests whether decision variables which are part of a constraint that never gets posted to the underlying solver
diff --git a/tests/test_tool_dimacs.py b/tests/test_tool_dimacs.py
index d7c29e0d..57e43f58 100644
--- a/tests/test_tool_dimacs.py
+++ b/tests/test_tool_dimacs.py
@@ -33,7 +33,7 @@ class CNFTool(unittest.TestCase):
     def test_empty_formula(self):
         model = self.dimacs_to_model("p cnf 0 0")
         self.assertTrue(model.solve())
-        self.assertEqual(model.status().exitstatus, ExitStatus.OPTIMAL)
+        self.assertEqual(model.status().exitstatus, ExitStatus.FEASIBLE)
 
     def test_empty_clauses(self):
         model = self.dimacs_to_model("p cnf 0 2\n0\n0")