Add a was_interrupted ref that indicates if Solver.interrupt was called on a solver or not

Author: hra687261

src/smtml/altergo_mappings.default.ml

@@ -51,6 +51,8 @@ module M = struct
       let caches_consts = false
 
       let is_available = true
+
+      let was_interrupted = ref false
     end
 
     type handle

src/smtml/bitwuzla_mappings.default.ml

@@ -13,6 +13,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
     let caches_consts = false
 
     let is_available = true
+
+    let was_interrupted = ref false
   end
 
   type ty = Sort.t

src/smtml/colibri2_mappings.default.ml

@@ -29,6 +29,8 @@ module M = struct
       let caches_consts = false
 
       let is_available = true
+
+      let was_interrupted = ref false
     end
 
     type handle

src/smtml/cvc5_mappings.default.ml

@@ -12,6 +12,8 @@ module Fresh_cvc5 () = struct
     let caches_consts = false
 
     let is_available = true
+
+    let was_interrupted = ref false
   end
 
   type ty = Sort.sort

src/smtml/mappings.nop.ml

@@ -10,6 +10,8 @@ module Nop = struct
       let caches_consts = false
 
       let is_available = false
+
+      let was_interrupted = ref false
     end
 
     type ty = [ `Ty ]

src/smtml/mappings_intf.ml

@@ -100,6 +100,9 @@ module type M = sig
 
     (** [caches_consts] indicates whether the solver caches constants. *)
     val caches_consts : bool
+
+    (** [was_interrupted] indicates if the solver was interrupted. *)
+    val was_interrupted : bool ref
   end
 
   (** {2 Type Handling} *)

src/smtml/z3_mappings.default.ml

@@ -14,6 +14,8 @@ module M = struct
       let caches_consts = true
 
       let is_available = true
+
+      let was_interrupted = ref false
     end
 
     type ty = Z3.Sort.sort
@@ -602,7 +604,9 @@ module M = struct
         Z3.Simplifier.and_then ctx simplify solver_eqs then_
         |> Z3.Solver.add_simplifier ctx solver
 
-      let interrupt () = Z3.Tactic.interrupt ctx
+      let interrupt () =
+        Internals.was_interrupted := true;
+        Z3.Tactic.interrupt ctx
 
       let get_statistics solver =
         get_statistics (Z3.Solver.get_statistics solver)