From 230306ddfc3ccb9e4f995ac6d1e6ea64b053cd17 Mon Sep 17 00:00:00 2001 From: Manuel Carrasco Date: Sun, 28 May 2023 20:04:36 +0100 Subject: [PATCH] Add solver::interrupt to Python's API. (#6739) --- src/api/python/z3/z3.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 6b79dd1fe..001776ec7 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7136,6 +7136,13 @@ class Solver(Z3PPObject): """Import model converter from other into the current solver""" Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver) + def interrupt(self): + """Interrupt the execution of the solver object. + Remarks: This ensures that the interrupt applies only + to the given solver object and it applies only if it is running. + """ + Z3_solver_interrupt(self.ctx.ref(), self.solver) + def unsat_core(self): """Return a subset (as an AST vector) of the assumptions provided to the last check().