Address partially review

src/bin/common/parse_command.ml

@@ -946,15 +946,14 @@ let parse_output_opt =
            info ["dump-models-on"] ~docv ~docs:s_models ~doc)
     in
 
-    let mk_interpretation interpretation produce_models dump_models
-        verify_models =
+    let mk_interpretation interpretation produce_models dump_models =
       match interpretation with
-      | INone when produce_models || dump_models || verify_models -> ILast
+      | INone when produce_models || dump_models -> ILast
       | interpretation -> interpretation
     in
     Term.(
       const mk_interpretation $ interpretation $
-      produce_models $ dump_models $ verify_models
+      produce_models $ dump_models
     ),
     dump_models,
     dump_models_on,

src/bin/common/solving_loop.ml

@@ -103,8 +103,16 @@ let cmd_on_modes st modes cmd =
 let verify_model ~get_value () =
   match get_value [Expr.vrai] with
   | Some [e] when Expr.equal e Expr.vrai -> ()
-  | Some [_] | None | exception Sat_solver_util.Wrong_model _ ->
+
+  | Some [_]
+  | exception Sat_solver_util.Wrong_model _
+  | exception Sat_solver_util.No_model ->
     recoverable_error "The model is wrong"
+
+  | None ->
+    (* The model generation is not enabled. *)
+    ()
+
   | Some _ ->
     (* The length of the output list is the same as the length of the
        input list. *)
@@ -841,6 +849,8 @@ let main () =
       recoverable_error "No model produced, cannot execute get-value."
     | exception Sat_solver_util.Wrong_model _ ->
       recoverable_error "The model is wrong, cannot execute get-value."
+    | exception Sat_solver_util.No_model ->
+      recoverable_error "No model produced but it should, cannot execute get-value."
   in
 
   let handle_get_assignment ~get_assignment st =

src/lib/reasoners/sat_solver_util.ml

@@ -82,25 +82,28 @@ let check (type a) (module SAT : S with type t = a) env =
   | I_dont_know | Sat -> ()
 
 exception Wrong_model of Explanation.t
+exception No_model
 
 (* Assert the last computed model in the environment [env].
 
-   @raise Unsat if the solver found a contradiction, which means the model
+   @raise Wrong_model if the solver found a contradiction, which means the model
           is wrong. *)
 let assert_model (type a) (module SAT : S with type t = a) env mdl =
-  ModelMap.iter
-    (fun ({ hs; _ } as name, _, ret_ty) graph ->
-       ModelMap.Graph.iter
-         (fun val_args val_ret ->
-            let e = Expr.mk_app name val_args ret_ty in
-            let iff = match ret_ty with Ty.Tbool -> true | _ -> false in
-            let eq = Expr.mk_eq ~iff e val_ret in
-            internal_assume (module SAT) env (Hstring.view hs) eq
-         )
-         graph
-    )
-    mdl.Models.model;
-  check (module SAT) env
+  try
+    ModelMap.iter
+      (fun ({ hs; _ } as name, _, ret_ty) graph ->
+         ModelMap.Graph.iter
+           (fun val_args val_ret ->
+              let e = Expr.mk_app name val_args ret_ty in
+              let iff = match ret_ty with Ty.Tbool -> true | _ -> false in
+              let eq = Expr.mk_eq ~iff e val_ret in
+              internal_assume (module SAT) env (Hstring.view hs) eq
+           )
+           graph
+      )
+      mdl.Models.model;
+    check (module SAT) env
+  with Unsat ex -> raise_notrace (Wrong_model ex)
 
 (* [get_value_in_boolean_model bmdl e] retrieves the assignment of the boolean
    expression [e] in the boolean model [bmdl].

src/lib/reasoners/sat_solver_util.mli

@@ -37,6 +37,7 @@ type lbool = False | True | Unknown
 val pp_lbool : lbool Fmt.t
 
 exception Wrong_model of Explanation.t
+exception No_model
 
 val get_value : 'a sat_module -> 'a -> Expr.t list -> Expr.t list option
 (** [get_value (module SAT) env l] returns the model values of the expressions
@@ -45,7 +46,9 @@ val get_value : 'a sat_module -> 'a -> Expr.t list -> Expr.t list option
     @return [None] if the model generation is not enabled or the
             environment is already unsatisfiable before calling this function.
     @raise Wrong_model if the solver found a contradiction in the current
-           model. *)
+           model.
+    @raise No_model if the solver didn't produce a model but the model
+           generation is enabled. *)
 
 val get_assignment : 'a sat_module -> 'a -> Expr.t list -> lbool list
 (** [get_assignment (module SAT) env l] returns the status of the literals [l]

src/lib/reasoners/satml_frontend.ml

@@ -1354,10 +1354,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   let optimize env ~is_max obj = SAT.optimize env.satml ~is_max obj
 
   let get_boolean_model env =
-    List.map (fun Atom.{ lit; _ } ->
+    List.filter_map (fun Atom.{ lit; _ } ->
         match Shostak.Literal.view lit with
-        | Literal.LTerm e -> e
-        | LSem _ -> assert false
+        | Literal.LTerm e -> Some e
+        | LSem _ -> None
       ) (SAT.boolean_model env.satml)
 
   let get_model env =