Rewording assertion

src/bin/common/solving_loop.ml

@@ -1053,6 +1053,7 @@ let main () =
      the hook on D_state_option.Mode. *)
   let handle_query st id loc attrs contents =
     let module Api = (val (DO.SatSolverModule.get st)) in
+    let st = internal_pop st in
     (* Pushing the environment once. This allows to keep a trace of the old
        environment in case we want to assert afterwards.
        The `pop` instruction is handled by the hook on the mode: when we assert
@@ -1071,19 +1072,10 @@ let main () =
     let solve_res =
       match Api.env.res with
       | `Unsat -> Unsat Api.env.expl
-      | `Sat ->
-        begin
-          let mdl = Model ((module Api.SAT), Api.env.sat_env) in
-          let () =
-            if Options.(get_interpretation () && get_dump_models ()) then
-              Api.FE.print_model
-                (Options.Output.get_fmt_models ())
-                Api.env.sat_env
-          in
-          Sat mdl
-        end
+      | `Sat
       | `Unknown ->
-        (* The environment did not conclude yet. *)
+        (* The environment did not conclude yet, or concluded with SAT. We
+           add additional constraints which may change this result. *)
         begin
           (* Preprocessing query. *)
           let goal_sort =

src/lib/reasoners/satml.ml

@@ -80,6 +80,7 @@ module type SAT_ML = sig
   val empty : unit -> t
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
+  val push_level : t -> int
   val decision_level : t -> int
   val cancel_until : t -> int -> unit
 
@@ -416,6 +417,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       env.clause_inc <- env.clause_inc *. 1e-20
     end
 
+  let push_level env = Vec.size env.increm_guards
+
   let decision_level env = Vec.size env.trail_lim
 
   let nb_assigns env = Vec.size env.trail

src/lib/reasoners/satml.mli

@@ -76,6 +76,9 @@ module type SAT_ML = sig
   val empty : unit -> t
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
+  (** Returns the push/pop depth of the current analysis
+      (i.e., #push - #pop) *)
+  val push_level : t -> int
   val decision_level : t -> int
   val cancel_until : t -> int -> unit
 

src/lib/reasoners/satml_frontend.ml

@@ -446,6 +446,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   let pred_def env f name dep _loc =
     (* dep currently not used. No unsat-cores in satML yet *)
     Debug.pred_def f;
+    assert (SAT.decision_level env.satml <= SAT.push_level env.satml);
     let guard = env.guards.current_guard in
     env.inst <- Inst.add_predicate env.inst ~guard ~name (mk_gf f) dep
 
@@ -1307,7 +1308,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let assume env gf _dep =
     (* dep currently not used. No unsat-cores in satML yet *)
-
+    assert (SAT.decision_level env.satml <= SAT.push_level env.satml);
     try
       let _ : bool =
         assume_aux