diff --git a/Makefile b/Makefile
index 50677c92f..15f5f59f5 100644
--- a/Makefile
+++ b/Makefile
@@ -128,7 +128,7 @@ runtest: gentest bin
 
 # Run non-regression tests for the CI.
 runtest-ci: gentest bin
-	dune build @runtest @runtest-quick @runtest-ci
+	dune build @runtest @runtest-quick @runtest-ci @check-models
 
 # Promote new outputs of the tests.
 promote:
diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam
index 89b163266..c6002edf3 100644
--- a/alt-ergo-lib.opam
+++ b/alt-ergo-lib.opam
@@ -20,6 +20,7 @@ depends: [
   "dolmen" {>= "0.9"}
   "dolmen_type" {>= "0.9"}
   "dolmen_loop" {>= "0.9"}
+  "dolmen_bin" {with-test}
   "ocplib-simplex" {>= "0.5"}
   "zarith" {>= "1.11"}
   "seq"
diff --git a/dune-project b/dune-project
index 2b6de3b71..d661f6221 100644
--- a/dune-project
+++ b/dune-project
@@ -80,6 +80,7 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (dolmen (>= 0.9))
   (dolmen_type (>= 0.9))
   (dolmen_loop (>= 0.9))
+  (dolmen_bin :with-test)
   (ocplib-simplex (>= 0.5))
   (zarith (>= 1.11))
   seq
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index c7545a8ee..259c737ab 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -53,6 +53,12 @@ module HT = Hashtbl.Make(
     let hash = Fun.id
   end)
 
+module DeclSet = Set.Make
+    (struct
+      type t = Id.typed
+      let compare = Id.compare_typed
+    end)
+
 (** Helper function: returns the basename of a dolmen path, since in AE
     the problems are contained in one-file (for now at least), the path is
     irrelevant and only the basename matters *)
@@ -701,8 +707,15 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
     end
   in
   Cache.store_sy tcst sy;
+  Cache.store_ty_vars id_ty;
   (* Adding polymorphic types to the cache. *)
-  Cache.store_ty_vars id_ty
+  let arg_tys, ret_ty =
+    match DT.view id_ty with
+    | `Arrow (arg_tys, ret_ty) ->
+      List.map dty_to_ty arg_tys, dty_to_ty ret_ty
+    | _ -> [], dty_to_ty id_ty
+  in
+  (Hstring.make name, arg_tys, ret_ty)
 
 (** Handles the definitions of a list of mutually recursive types.
     - If one of the types is an ADT, the ADTs that have only one case are
@@ -2087,14 +2100,24 @@ let make dloc_file acc stmt =
             assert false
         ) defs
 
-    | {contents = `Decls [td]; _ } ->
-      begin match td with
-        | `Type_decl (td, _def) -> mk_ty_decl td
-        | `Term_decl td -> mk_term_decl td
-      end;
-      acc
+    | {contents = `Decls [td]; loc; _ } ->
+      let decl = match td with
+        | `Type_decl (td, _def) ->
+          mk_ty_decl td;
+          None
+
+        | `Term_decl td ->
+          Some (mk_term_decl td)
+      in
+      begin match decl with
+        | Some d ->
+          let st_loc = dl_to_ael dloc_file loc in
+          C.{ st_decl = Decl d; st_loc } :: acc
+        | None ->
+          acc
+      end
 
-    | {contents = `Decls dcl; _ } ->
+    | {contents = `Decls dcl; loc; _ } ->
       let rec aux acc tdl =
         (* for now, when acc has more than one element it is assumed that the
            types are mutually recursive. Which is not necessarily the case.
@@ -2107,21 +2130,24 @@ let make dloc_file acc stmt =
             | [otd] -> mk_ty_decl otd
             | _ -> mk_mr_ty_decls (List.rev acc)
           end;
-          mk_term_decl td;
-          aux [] tl
+          let st_loc = dl_to_ael dloc_file loc in
+          C.{ st_decl = Decl (mk_term_decl td); st_loc } :: aux [] tl
 
         | `Type_decl (td, _def) :: tl ->
           aux (td :: acc) tl
 
         | [] ->
-          begin match acc with
-            | [] -> ()
-            | [otd] -> mk_ty_decl otd
-            | _ ->  mk_mr_ty_decls (List.rev acc)
+          begin
+            let () =
+              match acc with
+              | [] -> ()
+              | [otd] -> mk_ty_decl otd
+              | _ ->  mk_mr_ty_decls (List.rev acc)
+            in
+            []
           end
       in
-      aux [] dcl;
-      acc
+      aux [] dcl @ acc
 
     | { contents = `Set_logic _ | `Set_info _ | `Get_info _ ; _ } -> acc
 
diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
index 10808c3cf..bf5738549 100644
--- a/src/lib/frontend/frontend.ml
+++ b/src/lib/frontend/frontend.ml
@@ -302,6 +302,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
     else Ex.empty
 
+  let internal_decl ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit =
+    ignore loc;
+    match env.res with
+    | `Sat | `Unknown ->
+      SAT.declare env.sat_env id
+    | `Unsat -> ()
+
   let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;
     Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
@@ -443,6 +450,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
   let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
     try
       match d.st_decl with
+      | Decl id -> check_if_over (internal_decl ~loc:d.st_loc id) env
       | Push n -> check_if_over (internal_push ~loc:d.st_loc n) env
       | Pop n -> check_if_over (internal_pop ~loc:d.st_loc n) env
       | Assume (n, f, mf) ->
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index 457475278..eefc11ce7 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -43,7 +43,7 @@ type t = {
 
 let empty = {
   propositional = Expr.Set.empty;
-  model = ModelMap.empty ~suspicious:false;
+  model = ModelMap.empty ~suspicious:false [];
   term_values = Expr.Map.empty;
 }
 
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index b52c4327c..9eebb0527 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -86,7 +86,10 @@ module type S = sig
     Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
     t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances
 
-  val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
+  val extract_concrete_model :
+    prop_model:Expr.Set.t ->
+    declared_ids:Id.typed list ->
+    t -> Models.t
 
 end
 
@@ -748,6 +751,6 @@ module Main : S = struct
     in
     Uf.term_repr env.uf t
 
-  let extract_concrete_model ~prop_model env =
-    Uf.extract_concrete_model ~prop_model env.uf
+  let extract_concrete_model ~prop_model ~declared_ids env =
+    Uf.extract_concrete_model ~prop_model ~declared_ids env.uf
 end
diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli
index 6d6894a17..e8844ac96 100644
--- a/src/lib/reasoners/ccx.mli
+++ b/src/lib/reasoners/ccx.mli
@@ -77,7 +77,10 @@ module type S = sig
     Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
     t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances
 
-  val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
+  val extract_concrete_model :
+    prop_model:Expr.Set.t ->
+    declared_ids:Id.typed list ->
+    t -> Models.t
 
 end
 
diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
index 879645be9..1f65f6e1d 100644
--- a/src/lib/reasoners/fun_sat.ml
+++ b/src/lib/reasoners/fun_sat.ml
@@ -177,6 +177,8 @@ module Make (Th : Theory.S) = struct
     unit_facts_cache : (E.gformula * Ex.t) ME.t ref;
     last_saved_model : Models.t Lazy.t option ref;
     unknown_reason : Sat_solver_sig.unknown_reason option;
+    declare_ids : Id.typed Vec.t;
+    declare_lim : int Vec.t;
   }
 
   let reset_refs () =
@@ -1123,7 +1125,8 @@ module Make (Th : Theory.S) = struct
     else begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
-        let model, _ = Th.compute_concrete_model env.tbox in
+        let declared_ids = Vec.to_list env.declare_ids in
+        let model, _ = Th.compute_concrete_model ~declared_ids env.tbox in
         env.last_saved_model := Some model;
         env
       with Ex.Inconsistent (expl, classes) ->
@@ -1611,6 +1614,10 @@ module Make (Th : Theory.S) = struct
           "solved with backward!";
       raise e
 
+  let declare env id =
+    Vec.push env.declare_ids id;
+    env
+
   let push env to_push =
     if Options.get_tableaux_cdcl () then
       Errors.run_error
@@ -1626,6 +1633,7 @@ module Make (Th : Theory.S) = struct
           let guards = ME.add new_guard
               (mk_gf new_guard "" true true,Ex.empty)
               acc.guards.guards in
+          Vec.push env.declare_lim (Vec.size env.declare_ids);
           {acc with guards =
                       { acc.guards with
                         current_guard = new_guard;
@@ -1656,6 +1664,8 @@ module Make (Th : Theory.S) = struct
           in
           acc.model_gen_phase := false;
           env.last_saved_model := None;
+          let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
+          Vec.shrink env.declare_ids lim;
           {acc with inst;
                     guards =
                       { acc.guards with
@@ -1837,6 +1847,8 @@ module Make (Th : Theory.S) = struct
       add_inst = (fun _ -> true);
       last_saved_model = ref None;
       unknown_reason = None;
+      declare_ids = Vec.make 17 ~dummy:Id.dummy_typed;
+      declare_lim = Vec.make 17 ~dummy:(-1);
     }
     in
     assume env gf_true Ex.empty
diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli
index ca5382fe6..fc5eee731 100644
--- a/src/lib/reasoners/fun_sat.mli
+++ b/src/lib/reasoners/fun_sat.mli
@@ -40,6 +40,8 @@ module Make (Th : Theory.S) : sig
 
   val empty_with_inst : (Expr.t -> bool) -> t
 
+  val declare : t -> Id.typed -> t
+
   val push : t -> int -> t
 
   val pop : t -> int -> t
diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml
index bad7812b0..b359df929 100644
--- a/src/lib/reasoners/fun_sat_frontend.ml
+++ b/src/lib/reasoners/fun_sat_frontend.ml
@@ -47,6 +47,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | FS.Unsat expl -> raise (Unsat expl)
     | FS.I_dont_know e -> env := e; raise I_dont_know
 
+  let declare t id =
+    t := FS.declare !t id
+
   let push t i = exn_handler (fun env -> t := FS.push env i) t
 
   let pop t i = exn_handler (fun env -> t := FS.pop env i) t
diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml
index 24c2f1f3b..f01169de0 100644
--- a/src/lib/reasoners/sat_solver_sig.ml
+++ b/src/lib/reasoners/sat_solver_sig.ml
@@ -76,6 +76,8 @@ module type S = sig
   val empty : unit -> t
   val empty_with_inst : (Expr.t -> bool) -> t
 
+  val declare : t -> Id.typed -> unit
+
   (** [push env n] add n new assertion levels.
       A guard g is added for every expression e assumed at the current
       assertion level.
diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli
index 72b361905..40e66c05b 100644
--- a/src/lib/reasoners/sat_solver_sig.mli
+++ b/src/lib/reasoners/sat_solver_sig.mli
@@ -56,6 +56,8 @@ module type S = sig
   val empty : unit -> t
   val empty_with_inst : (Expr.t -> bool) -> t
 
+  val declare : t -> Id.typed -> unit
+
   (** [push env n] add n new assertion levels.
       A guard g is added for every expression e assumed at the current
       assertion level.
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 678d855e1..802f8029b 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -67,6 +67,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     mutable unknown_reason : Sat_solver_sig.unknown_reason option;
     (** The reason why satml raised [I_dont_know] if it does; [None] by
         default. *)
+    declare_ids : Id.typed Vec.t;
+    declare_lim : int Vec.t;
   }
 
   let empty_guards () = {
@@ -97,6 +99,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       last_saved_model = None;
       last_saved_objectives = None;
       unknown_reason = None;
+      declare_ids = Vec.make 17 ~dummy:Id.dummy_typed;
+      declare_lim = Vec.make 17 ~dummy:(-1);
     }
 
   let empty_with_inst add_inst =
@@ -968,8 +972,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     if compute then begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
+        let declared_ids = Vec.to_list env.declare_ids in
         let model, objectives =
-          Th.compute_concrete_model (SAT.current_tbox env.satml)
+          Th.compute_concrete_model ~declared_ids (SAT.current_tbox env.satml)
         in
         env.last_saved_model <- Some model;
         env.last_saved_objectives <- Some objectives;
@@ -1207,6 +1212,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       expr_guard, atom_guard
     | _ -> assert false
 
+  let declare env id = Vec.push env.declare_ids id
+
   let push env to_push =
     Util.loop ~f:(fun _n () () ->
         try
@@ -1214,7 +1221,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           SAT.push env.satml atom_guard;
           Stack.push expr_guard env.guards.stack_guard;
           Steps.push_steps ();
-          env.guards.current_guard <- expr_guard
+          env.guards.current_guard <- expr_guard;
+          Vec.push env.declare_lim (Vec.size env.declare_ids)
         with
         | Util.Step_limit_reached _ ->
           (* This function should be called without step limit
@@ -1237,7 +1245,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           env.last_saved_model <- None;
           env.last_saved_objectives <- None;
           env.inst <- inst;
-          env.guards.current_guard <- b
+          env.guards.current_guard <- b;
+          let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
+          Vec.shrink env.declare_ids lim
         )
       ~max:to_pop
       ~elt:()
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 4c5a76ff6..1d721a77f 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -61,7 +61,10 @@ module type S = sig
   val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t
 
   val add_term : t -> Expr.t -> add_in_cs:bool -> t
-  val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t
+  val compute_concrete_model :
+    t ->
+    declared_ids:Id.typed list ->
+    Models.t Lazy.t * Objective.Model.t
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
   val theories_instances :
@@ -879,13 +882,14 @@ module Main_Default : S = struct
   let get_real_env t = t.gamma
   let get_case_split_env t = t.gamma_finite
 
-  let compute_concrete_model env =
+  let compute_concrete_model env ~declared_ids =
     let { gamma_finite; assumed_set; objectives; _ }, _ =
       do_case_split_aux env ~for_model:true
     in
     lazy (
       CC_X.extract_concrete_model
         ~prop_model:assumed_set
+        ~declared_ids
         gamma_finite
     ), objectives
 
@@ -940,7 +944,8 @@ module Main_Empty : S = struct
   let get_case_split_env _ = CC_X.empty
   let do_case_split env _ = env, E.Set.empty
   let add_term env _ ~add_in_cs:_ = env
-  let compute_concrete_model _env = lazy Models.empty, Objective.Model.empty
+  let compute_concrete_model _env ~declared_ids:_ =
+    lazy Models.empty, Objective.Model.empty
 
   let assume_th_elt e _ _ = e
   let theories_instances ~do_syntactic_matching:_ _ e _ _ _ = e, []
diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli
index c7e8f71eb..c0f916c74 100644
--- a/src/lib/reasoners/theory.mli
+++ b/src/lib/reasoners/theory.mli
@@ -54,7 +54,10 @@ module type S = sig
 
   val add_term : t -> Expr.t -> add_in_cs:bool -> t
 
-  val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t
+  val compute_concrete_model :
+    t ->
+    declared_ids:Id.typed list ->
+    Models.t Lazy.t * Objective.Model.t
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
   val theories_instances :
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index c22bcff25..d0f106108 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1167,11 +1167,11 @@ let compute_concrete_model_of_val cache =
 let extract_concrete_model cache =
   let compute_concrete_model_of_val = compute_concrete_model_of_val cache in
   let get_abstract_for = Cache.get_abstract_for cache.abstracts
-  in fun ~prop_model env ->
+  in fun ~prop_model ~declared_ids env ->
     let terms, suspicious = terms env in
     let model, mrepr =
       MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc)
-        terms (ModelMap.empty ~suspicious, ME.empty)
+        terms (ModelMap.empty ~suspicious declared_ids, ME.empty)
     in
     let model =
       Hashtbl.fold (fun t vals mdl ->
@@ -1212,9 +1212,9 @@ let extract_concrete_model cache =
     in
     { Models.propositional = prop_model; model; term_values = mrepr }
 
-let extract_concrete_model ~prop_model =
+let extract_concrete_model ~prop_model ~declared_ids =
   let cache : cache = {
     array_selects = Hashtbl.create 17;
     abstracts = Hashtbl.create 17;
   }
-  in fun env -> extract_concrete_model cache ~prop_model env
+  in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env
diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli
index 40fd47cd1..9eef6b30c 100644
--- a/src/lib/reasoners/uf.mli
+++ b/src/lib/reasoners/uf.mli
@@ -72,7 +72,11 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t
 (** {2 Counterexample function} *)
 
 (** Compute a counterexample using the Uf environment *)
-val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
+val extract_concrete_model :
+  prop_model:Expr.Set.t ->
+  declared_ids:Id.typed list ->
+  t ->
+  Models.t
 
 (** saves the module's cache *)
 val save_cache : unit -> unit
diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml
index c539128ba..5c26fa59b 100644
--- a/src/lib/structures/commands.ml
+++ b/src/lib/structures/commands.ml
@@ -31,6 +31,7 @@
 (* Sat entry *)
 
 type sat_decl_aux =
+  | Decl of Id.typed
   | Assume of string * Expr.t * bool
   | PredDef of Expr.t * string (*name of the predicate*)
   | RwtDef of (Expr.t Typed.rwt_rule) list
@@ -46,6 +47,12 @@ type sat_tdecl = {
 }
 
 let print_aux fmt = function
+  | Decl (id, arg_tys, ret_ty) ->
+    Fmt.pf fmt "declare %a with type (%a) -> %a"
+      Id.pp id
+      Fmt.(list ~sep:comma Ty.print) arg_tys
+      Ty.print ret_ty
+
   | Assume (name, e, b) ->
     Format.fprintf fmt "assume %s(%b): @[<hov>%a@]" name b Expr.print e
   | PredDef (e, name) ->
diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli
index 320da889c..800c58f10 100644
--- a/src/lib/structures/commands.mli
+++ b/src/lib/structures/commands.mli
@@ -31,6 +31,7 @@
 (* Sat entry *)
 
 type sat_decl_aux =
+  | Decl of Id.typed
   | Assume of string * Expr.t * bool
   | PredDef of Expr.t * string (*name of the predicate*)
   | RwtDef of (Expr.t Typed.rwt_rule) list
diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml
index e34de223f..62624c385 100644
--- a/src/lib/structures/id.ml
+++ b/src/lib/structures/id.ml
@@ -30,6 +30,8 @@
 
 type t = Hstring.t [@@deriving ord]
 
+type typed = t * Ty.t list * Ty.t [@@deriving ord]
+
 let equal = Hstring.equal
 
 let pp ppf id =
@@ -79,3 +81,7 @@ module Namespace = struct
     Skolem.reset_fresh_cpt ();
     Abstract.reset_fresh_cpt ()
 end
+
+let dummy_typed =
+  let id = Namespace.Internal.fresh () |> Hstring.make in
+  (id, [], Ty.Tunit)
diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli
index 0b2434918..a48fc43c8 100644
--- a/src/lib/structures/id.mli
+++ b/src/lib/structures/id.mli
@@ -30,6 +30,15 @@
 
 type t = Hstring.t [@@deriving ord]
 
+type typed = t * Ty.t list * Ty.t
+(** Typed identifier of function. In order:
+    - The identifier.
+    - Types of its arguments.
+    - The returned type. *)
+
+val dummy_typed : typed
+
+val compare_typed : typed -> typed -> int
 val equal : t -> t -> bool
 val show : t -> string
 val pp : t Fmt.t
diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml
index 2b7fb096f..8a0e68928 100644
--- a/src/lib/structures/modelMap.ml
+++ b/src/lib/structures/modelMap.ml
@@ -31,8 +31,6 @@
 module X = Shostak.Combine
 module Sy = Symbols
 
-type sy = Id.t * Ty.t list * Ty.t [@@deriving ord]
-
 module Graph = struct
   module M = Map.Make
       (struct
@@ -44,6 +42,8 @@ module Graph = struct
   let empty = M.empty
   let add = M.add
   let map = M.map
+  let cardinal = M.cardinal
+  let choose = M.choose
 
   (* A fiber of the function [f] over a value [v] is the set of all the values
      in the domain of [f] whose the image by [f] is [v].
@@ -113,9 +113,9 @@ end
 
 module P = Map.Make
     (struct
-      type t = sy
+      type t = Id.typed
 
-      let compare = compare_sy
+      let compare = Id.compare_typed
     end)
 
 type t = {
@@ -127,12 +127,45 @@ let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } =
   if List.compare_lengths arg_tys arg_vals <> 0 then
     Fmt.invalid_arg "The arity of the symbol %a doesn't agree the number of \
                      arguments" Id.pp id;
-
-  let graph = try P.find sy values with Not_found -> Graph.empty in
+  let graph =
+    try
+      let graph = P.find sy values in
+      (* If the graph associated with [sy] contains only an abstract value,
+         it means there is no constraint on this graph. We replace it by
+         the graph with the only constraint given by [arg_vals] and
+         [ret_val]. *)
+      if Graph.cardinal graph == 1 then
+        let _, value = Graph.choose graph in
+        let Expr.{ f; _ } = Expr.term_view value in
+        match f with
+        | Sy.Name { hs; _ }
+          when Id.Namespace.Abstract.is_id (Hstring.view hs) ->
+          Graph.empty
+        | _ -> graph
+      else
+        graph
+    with Not_found -> Graph.empty in
   let values = P.add sy (Graph.add arg_vals ret_val graph) values in
   { values; suspicious }
 
-let empty ~suspicious = { values = P.empty; suspicious }
+module DeclSets = Set.Make
+    (struct
+      type t = Id.typed
+      let compare = Id.compare_typed
+    end)
+
+let empty ~suspicious declared_ids =
+  let values =
+    List.fold_left
+      (fun values ((_, arg_tys, ret_ty) as sy) ->
+         let arg_vals = List.map Expr.mk_abstract arg_tys in
+         let ret_val = Expr.mk_abstract ret_ty in
+         let graph = Graph.add arg_vals ret_val Graph.empty in
+         P.add sy graph values
+      )
+      P.empty declared_ids
+  in
+  { values; suspicious }
 
 let rec subst_in_term id e c =
   let Expr.{ f; xs; ty = ty'; _ } = Expr.term_view c in
diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli
index 9d8e9f0ec..b2d03124c 100644
--- a/src/lib/structures/modelMap.mli
+++ b/src/lib/structures/modelMap.mli
@@ -28,20 +28,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type sy = Id.t * Ty.t list * Ty.t
-(** Typed symbol of function defined in the model. In order:
-    - The identifier of the symbol.
-    - The types of its arguments.
-    - The returned type. *)
-
 type t
 (** Type of model. *)
 
-val add : sy -> Expr.t list -> Expr.t -> t -> t
+val add : Id.typed -> Expr.t list -> Expr.t -> t -> t
 (** [add sy args ret mdl] adds the binding [args -> ret] to the partial graph
     associated with the symbol [sy]. *)
 
-val empty : suspicious:bool -> t
+val empty : suspicious:bool -> Id.typed list -> t
 (** An empty model. The [suspicious] flag is used to remember that this
     model may be wrong as it involves symbols from theories for which the
     model generation is known to be incomplete. *)
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index 1aa6dc1e5..6e3bf96b8 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -12,7 +12,8 @@ appropriate here.
   (
     (define-fun x () Int 0)
     (define-fun y () Int 0)
-    (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+    (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
+    (define-fun a2 () (Array Int Int) (as @a3 (Array Int Int)))
   )
 
 Now we will test some semantic triggers.
diff --git a/tests/dune.inc b/tests/dune.inc
index 26d82ad68..20455b3d9 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -191478,2328 +191478,41 @@
       (action
        (diff test_float2.models.expected test_float2.models_dolmen.output)))
   (rule
-   (target test_float1.dolmen_dolmen.output)
-   (deps (:input test_float1.dolmen.smt2))
+   (alias check-models)
+   (deps (:input test_float2.models_dolmen.output) (:test test_float2.models.smt2))
    (package alt-ergo)
    (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps test_float1.dolmen_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff test_float1.dolmen.expected test_float1.dolmen_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
-; Auto-generated part begin
-(subdir issues
-  (rule
-   (target 926.models_dolmen.output)
-   (deps (:input 926.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 926.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 926.models.expected 926.models_dolmen.output)))
-  (rule
-   (target 889_optimize.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps 889_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_optimize.output)))
-  (rule
-   (target 889_ci_cdcl_no_minimal_bj.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 889_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 889_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 889_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (deps 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target 889_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 889_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 889_cdcl.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (deps 889_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_cdcl.output)))
-  (rule
-   (target 889_tableaux_cdcl.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (deps 889_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_tableaux_cdcl.output)))
-  (rule
-   (target 889_tableaux.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (deps 889_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_tableaux.output)))
-  (rule
-   (target 889_dolmen.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 889_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_dolmen.output)))
-  (rule
-   (target 889_fpa.output)
-   (deps (:input 889.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (deps 889_fpa.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 889.expected 889_fpa.output)))
-  (rule
-   (target 883.dolmen_dolmen.output)
-   (deps (:input 883.dolmen.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 883.dolmen_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 883.dolmen.expected 883.dolmen_dolmen.output)))
-  (rule
-   (target 777.models_dolmen.output)
-   (deps (:input 777.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 777.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 777.models.expected 777.models_dolmen.output)))
-  (rule
-   (target 696_optimize.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps 696_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_optimize.output)))
-  (rule
-   (target 696_ci_cdcl_no_minimal_bj.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 696_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 696_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 696_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (deps 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target 696_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 696_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 696_cdcl.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (deps 696_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_cdcl.output)))
-  (rule
-   (target 696_tableaux_cdcl.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (deps 696_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_tableaux_cdcl.output)))
-  (rule
-   (target 696_tableaux.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (deps 696_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_tableaux.output)))
-  (rule
-   (target 696_legacy.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend legacy
-             %{input})))))))
-  (rule
-   (deps 696_legacy.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_legacy.output)))
-  (rule
-   (target 696_dolmen.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 696_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_dolmen.output)))
-  (rule
-   (target 696_fpa.output)
-   (deps (:input 696.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (deps 696_fpa.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 696.expected 696_fpa.output)))
-  (rule
-   (target 695_optimize.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps 695_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_optimize.output)))
-  (rule
-   (target 695_ci_cdcl_no_minimal_bj.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 695_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 695_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 695_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (deps 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target 695_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 695_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 695_cdcl.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (deps 695_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_cdcl.output)))
-  (rule
-   (target 695_tableaux_cdcl.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (deps 695_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_tableaux_cdcl.output)))
-  (rule
-   (target 695_tableaux.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (deps 695_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_tableaux.output)))
-  (rule
-   (target 695_dolmen.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 695_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_dolmen.output)))
-  (rule
-   (target 695_fpa.output)
-   (deps (:input 695.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (deps 695_fpa.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 695.expected 695_fpa.output)))
-  (rule
-   (target 645_optimize.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps 645_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_optimize.output)))
-  (rule
-   (target 645_ci_cdcl_no_minimal_bj.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 645_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 645_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 645_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (deps 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target 645_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 645_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 645_cdcl.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (deps 645_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_cdcl.output)))
-  (rule
-   (target 645_tableaux_cdcl.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (deps 645_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_tableaux_cdcl.output)))
-  (rule
-   (target 645_tableaux.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (deps 645_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_tableaux.output)))
-  (rule
-   (target 645_legacy.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend legacy
-             %{input})))))))
-  (rule
-   (deps 645_legacy.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_legacy.output)))
-  (rule
-   (target 645_dolmen.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 645_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_dolmen.output)))
-  (rule
-   (target 645_fpa.output)
-   (deps (:input 645.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (deps 645_fpa.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 645.expected 645_fpa.output)))
-  (rule
-   (target 555.models_dolmen.output)
-   (deps (:input 555.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 555.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 555.models.expected 555.models_dolmen.output)))
-  (rule
-   (target 479_optimize.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps 479_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_optimize.output)))
-  (rule
-   (target 479_ci_cdcl_no_minimal_bj.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 479_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 479_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 479_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target 479_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 479_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 479_cdcl.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (deps 479_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_cdcl.output)))
-  (rule
-   (target 479_tableaux_cdcl.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (deps 479_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_tableaux_cdcl.output)))
-  (rule
-   (target 479_tableaux.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (deps 479_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_tableaux.output)))
-  (rule
-   (target 479_dolmen.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 479_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_dolmen.output)))
-  (rule
-   (target 479_fpa.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (deps 479_fpa.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 479.expected 479_fpa.output)))
-  (rule
-   (target 460_optimize.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps 460_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_optimize.output)))
-  (rule
-   (target 460_ci_cdcl_no_minimal_bj.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 460_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 460_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 460_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (deps 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target 460_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 460_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 460_cdcl.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (deps 460_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_cdcl.output)))
-  (rule
-   (target 460_tableaux_cdcl.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (deps 460_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_tableaux_cdcl.output)))
-  (rule
-   (target 460_tableaux.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (deps 460_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_tableaux.output)))
-  (rule
-   (target 460_legacy.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend legacy
-             %{input})))))))
-  (rule
-   (deps 460_legacy.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_legacy.output)))
-  (rule
-   (target 460_dolmen.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 460_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_dolmen.output)))
-  (rule
-   (target 460_fpa.output)
-   (deps (:input 460.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (deps 460_fpa.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 460.expected 460_fpa.output)))
-  (rule
-   (target 350_optimize.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps 350_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_optimize.output)))
-  (rule
-   (target 350_ci_cdcl_no_minimal_bj.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 350_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 350_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 350_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (deps 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target 350_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 350_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 350_cdcl.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (deps 350_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_cdcl.output)))
-  (rule
-   (target 350_tableaux_cdcl.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (deps 350_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_tableaux_cdcl.output)))
-  (rule
-   (target 350_tableaux.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (deps 350_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_tableaux.output)))
-  (rule
-   (target 350_legacy.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend legacy
-             %{input})))))))
-  (rule
-   (deps 350_legacy.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_legacy.output)))
-  (rule
-   (target 350_dolmen.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 350_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_dolmen.output)))
-  (rule
-   (target 350_fpa.output)
-   (deps (:input 350.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (deps 350_fpa.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 350.expected 350_fpa.output)))
-  (rule
-   (target 340_optimize.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps 340_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_optimize.output)))
-  (rule
-   (target 340_ci_cdcl_no_minimal_bj.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 340_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target 340_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (deps 340_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (deps 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target 340_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (deps 340_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target 340_cdcl.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (deps 340_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_cdcl.output)))
-  (rule
-   (target 340_tableaux_cdcl.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (deps 340_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_tableaux_cdcl.output)))
-  (rule
-   (target 340_tableaux.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (deps 340_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_tableaux.output)))
+    (with-accepted-exit-codes 0
+     (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target test_float1.dolmen_dolmen.output)
+ (deps (:input test_float1.dolmen.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps test_float1.dolmen_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff test_float1.dolmen.expected test_float1.dolmen_dolmen.output))))
+; Auto-generated part end ; File auto-generated by gentests 
+; Auto-generated part begin
+(subdir issues
   (rule
-   (target 340_dolmen.output)
-   (deps (:input 340.smt2))
+   (target 926.models_dolmen.output)
+   (deps (:input 926.models.smt2))
    (package alt-ergo)
    (action
     (chdir %{workspace_root}
@@ -193813,36 +191526,2351 @@
              --frontend dolmen
              %{input})))))))
   (rule
-   (deps 340_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 340.expected 340_dolmen.output)))
-  (rule
-   (target 340_fpa.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (deps 340_fpa.output)
+   (deps 926.models_dolmen.output)
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff 340.expected 340_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+       (diff 926.models.expected 926.models_dolmen.output)))(rule
+                                                             (alias check-models)
+                                                             (deps (:input 926.models_dolmen.output) (:test 926.models.smt2))
+                                                             (package alt-ergo)
+                                                             (action
+                                                              (with-accepted-exit-codes 0
+                                                               (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
-; Auto-generated part begin
+
+(rule
+ (target 889_optimize.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps 889_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_optimize.output)))
+(rule
+ (target 889_ci_cdcl_no_minimal_bj.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 889_ci_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_ci_cdcl_no_minimal_bj.output)))
+(rule
+ (target 889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 889_ci_no_tableaux_cdcl_in_instantiation.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 889_ci_no_tableaux_cdcl_in_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_ci_no_tableaux_cdcl_in_instantiation.output)))
+(rule
+ (target 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (deps 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+(rule
+ (target 889_ci_tableaux_cdcl_no_minimal_bj.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 889_ci_tableaux_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_ci_tableaux_cdcl_no_minimal_bj.output)))
+(rule
+ (target 889_cdcl.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (deps 889_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_cdcl.output)))
+(rule
+ (target 889_tableaux_cdcl.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (deps 889_tableaux_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_tableaux_cdcl.output)))
+(rule
+ (target 889_tableaux.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (deps 889_tableaux.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_tableaux.output)))
+(rule
+ (target 889_dolmen.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 889_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_dolmen.output)))
+(rule
+ (target 889_fpa.output)
+ (deps (:input 889.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (deps 889_fpa.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 889.expected 889_fpa.output)))
+(rule
+ (target 883.dolmen_dolmen.output)
+ (deps (:input 883.dolmen.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 883.dolmen_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 883.dolmen.expected 883.dolmen_dolmen.output)))
+(rule
+ (target 777.models_dolmen.output)
+ (deps (:input 777.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 777.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 777.models.expected 777.models_dolmen.output)))(rule
+                                                           (alias check-models)
+                                                           (deps (:input 777.models_dolmen.output) (:test 777.models.smt2))
+                                                           (package alt-ergo)
+                                                           (action
+                                                            (with-accepted-exit-codes 0
+                                                             (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target 696_optimize.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps 696_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_optimize.output)))
+(rule
+ (target 696_ci_cdcl_no_minimal_bj.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 696_ci_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_ci_cdcl_no_minimal_bj.output)))
+(rule
+ (target 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 696_ci_no_tableaux_cdcl_in_instantiation.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 696_ci_no_tableaux_cdcl_in_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_ci_no_tableaux_cdcl_in_instantiation.output)))
+(rule
+ (target 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (deps 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+(rule
+ (target 696_ci_tableaux_cdcl_no_minimal_bj.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 696_ci_tableaux_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_ci_tableaux_cdcl_no_minimal_bj.output)))
+(rule
+ (target 696_cdcl.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (deps 696_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_cdcl.output)))
+(rule
+ (target 696_tableaux_cdcl.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (deps 696_tableaux_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_tableaux_cdcl.output)))
+(rule
+ (target 696_tableaux.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (deps 696_tableaux.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_tableaux.output)))
+(rule
+ (target 696_legacy.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend legacy
+           %{input})))))))
+(rule
+ (deps 696_legacy.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_legacy.output)))
+(rule
+ (target 696_dolmen.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 696_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_dolmen.output)))
+(rule
+ (target 696_fpa.output)
+ (deps (:input 696.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (deps 696_fpa.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 696.expected 696_fpa.output)))
+(rule
+ (target 695_optimize.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps 695_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_optimize.output)))
+(rule
+ (target 695_ci_cdcl_no_minimal_bj.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 695_ci_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_ci_cdcl_no_minimal_bj.output)))
+(rule
+ (target 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 695_ci_no_tableaux_cdcl_in_instantiation.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 695_ci_no_tableaux_cdcl_in_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_ci_no_tableaux_cdcl_in_instantiation.output)))
+(rule
+ (target 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (deps 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+(rule
+ (target 695_ci_tableaux_cdcl_no_minimal_bj.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 695_ci_tableaux_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_ci_tableaux_cdcl_no_minimal_bj.output)))
+(rule
+ (target 695_cdcl.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (deps 695_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_cdcl.output)))
+(rule
+ (target 695_tableaux_cdcl.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (deps 695_tableaux_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_tableaux_cdcl.output)))
+(rule
+ (target 695_tableaux.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (deps 695_tableaux.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_tableaux.output)))
+(rule
+ (target 695_dolmen.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 695_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_dolmen.output)))
+(rule
+ (target 695_fpa.output)
+ (deps (:input 695.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (deps 695_fpa.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 695.expected 695_fpa.output)))
+(rule
+ (target 645_optimize.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps 645_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_optimize.output)))
+(rule
+ (target 645_ci_cdcl_no_minimal_bj.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 645_ci_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_ci_cdcl_no_minimal_bj.output)))
+(rule
+ (target 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 645_ci_no_tableaux_cdcl_in_instantiation.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 645_ci_no_tableaux_cdcl_in_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_ci_no_tableaux_cdcl_in_instantiation.output)))
+(rule
+ (target 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (deps 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+(rule
+ (target 645_ci_tableaux_cdcl_no_minimal_bj.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 645_ci_tableaux_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_ci_tableaux_cdcl_no_minimal_bj.output)))
+(rule
+ (target 645_cdcl.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (deps 645_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_cdcl.output)))
+(rule
+ (target 645_tableaux_cdcl.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (deps 645_tableaux_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_tableaux_cdcl.output)))
+(rule
+ (target 645_tableaux.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (deps 645_tableaux.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_tableaux.output)))
+(rule
+ (target 645_legacy.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend legacy
+           %{input})))))))
+(rule
+ (deps 645_legacy.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_legacy.output)))
+(rule
+ (target 645_dolmen.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 645_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_dolmen.output)))
+(rule
+ (target 645_fpa.output)
+ (deps (:input 645.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (deps 645_fpa.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 645.expected 645_fpa.output)))
+(rule
+ (target 555.models_dolmen.output)
+ (deps (:input 555.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 555.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 555.models.expected 555.models_dolmen.output)))(rule
+                                                           (alias check-models)
+                                                           (deps (:input 555.models_dolmen.output) (:test 555.models.smt2))
+                                                           (package alt-ergo)
+                                                           (action
+                                                            (with-accepted-exit-codes 0
+                                                             (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target 479_optimize.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps 479_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_optimize.output)))
+(rule
+ (target 479_ci_cdcl_no_minimal_bj.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 479_ci_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_ci_cdcl_no_minimal_bj.output)))
+(rule
+ (target 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 479_ci_no_tableaux_cdcl_in_instantiation.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 479_ci_no_tableaux_cdcl_in_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_ci_no_tableaux_cdcl_in_instantiation.output)))
+(rule
+ (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+(rule
+ (target 479_ci_tableaux_cdcl_no_minimal_bj.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 479_ci_tableaux_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_ci_tableaux_cdcl_no_minimal_bj.output)))
+(rule
+ (target 479_cdcl.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (deps 479_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_cdcl.output)))
+(rule
+ (target 479_tableaux_cdcl.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (deps 479_tableaux_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_tableaux_cdcl.output)))
+(rule
+ (target 479_tableaux.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (deps 479_tableaux.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_tableaux.output)))
+(rule
+ (target 479_dolmen.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 479_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_dolmen.output)))
+(rule
+ (target 479_fpa.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (deps 479_fpa.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 479.expected 479_fpa.output)))
+(rule
+ (target 460_optimize.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps 460_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_optimize.output)))
+(rule
+ (target 460_ci_cdcl_no_minimal_bj.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 460_ci_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_ci_cdcl_no_minimal_bj.output)))
+(rule
+ (target 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 460_ci_no_tableaux_cdcl_in_instantiation.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 460_ci_no_tableaux_cdcl_in_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_ci_no_tableaux_cdcl_in_instantiation.output)))
+(rule
+ (target 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (deps 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+(rule
+ (target 460_ci_tableaux_cdcl_no_minimal_bj.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 460_ci_tableaux_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_ci_tableaux_cdcl_no_minimal_bj.output)))
+(rule
+ (target 460_cdcl.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (deps 460_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_cdcl.output)))
+(rule
+ (target 460_tableaux_cdcl.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (deps 460_tableaux_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_tableaux_cdcl.output)))
+(rule
+ (target 460_tableaux.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (deps 460_tableaux.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_tableaux.output)))
+(rule
+ (target 460_legacy.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend legacy
+           %{input})))))))
+(rule
+ (deps 460_legacy.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_legacy.output)))
+(rule
+ (target 460_dolmen.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 460_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_dolmen.output)))
+(rule
+ (target 460_fpa.output)
+ (deps (:input 460.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (deps 460_fpa.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 460.expected 460_fpa.output)))
+(rule
+ (target 350_optimize.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps 350_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_optimize.output)))
+(rule
+ (target 350_ci_cdcl_no_minimal_bj.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 350_ci_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_ci_cdcl_no_minimal_bj.output)))
+(rule
+ (target 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 350_ci_no_tableaux_cdcl_in_instantiation.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 350_ci_no_tableaux_cdcl_in_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_ci_no_tableaux_cdcl_in_instantiation.output)))
+(rule
+ (target 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (deps 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+(rule
+ (target 350_ci_tableaux_cdcl_no_minimal_bj.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 350_ci_tableaux_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_ci_tableaux_cdcl_no_minimal_bj.output)))
+(rule
+ (target 350_cdcl.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (deps 350_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_cdcl.output)))
+(rule
+ (target 350_tableaux_cdcl.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (deps 350_tableaux_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_tableaux_cdcl.output)))
+(rule
+ (target 350_tableaux.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (deps 350_tableaux.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_tableaux.output)))
+(rule
+ (target 350_legacy.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend legacy
+           %{input})))))))
+(rule
+ (deps 350_legacy.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_legacy.output)))
+(rule
+ (target 350_dolmen.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 350_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_dolmen.output)))
+(rule
+ (target 350_fpa.output)
+ (deps (:input 350.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (deps 350_fpa.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 350.expected 350_fpa.output)))
+(rule
+ (target 340_optimize.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps 340_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_optimize.output)))
+(rule
+ (target 340_ci_cdcl_no_minimal_bj.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 340_ci_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_ci_cdcl_no_minimal_bj.output)))
+(rule
+ (target 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+(rule
+ (target 340_ci_no_tableaux_cdcl_in_instantiation.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (deps 340_ci_no_tableaux_cdcl_in_instantiation.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_ci_no_tableaux_cdcl_in_instantiation.output)))
+(rule
+ (target 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (deps 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+(rule
+ (target 340_ci_tableaux_cdcl_no_minimal_bj.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (deps 340_ci_tableaux_cdcl_no_minimal_bj.output)
+  (alias runtest-ci)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_ci_tableaux_cdcl_no_minimal_bj.output)))
+(rule
+ (target 340_cdcl.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (deps 340_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_cdcl.output)))
+(rule
+ (target 340_tableaux_cdcl.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (deps 340_tableaux_cdcl.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_tableaux_cdcl.output)))
+(rule
+ (target 340_tableaux.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (deps 340_tableaux.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_tableaux.output)))
+(rule
+ (target 340_dolmen.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 340_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_dolmen.output)))
+(rule
+ (target 340_fpa.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (deps 340_fpa.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 340.expected 340_fpa.output)))) ; Auto-generated part end
+; File auto-generated by gentests  ; Auto-generated part begin
 (subdir issues/649
   (rule
    (target 649.dolmen_dolmen.output)
@@ -194156,11 +194184,8 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff 649.expected 649_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
-; Auto-generated part begin
+       (diff 649.expected 649_fpa.output)))) ; Auto-generated part end
+; File auto-generated by gentests  ; Auto-generated part begin
 (subdir issues/664
   (rule
    (target 664.dolmen_dolmen.output)
@@ -194474,11 +194499,8 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff 664.expected 664_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
-; Auto-generated part begin
+       (diff 664.expected 664_fpa.output)))) ; Auto-generated part end
+; File auto-generated by gentests  ; Auto-generated part begin
 (subdir issues/854
   (rule
    (target twice_eq.models_dolmen.output)
@@ -194502,50 +194524,72 @@
       (action
        (diff twice_eq.models.expected twice_eq.models_dolmen.output)))
   (rule
-   (target original.models_dolmen.output)
-   (deps (:input original.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps original.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff original.models.expected original.models_dolmen.output)))
-  (rule
-   (target function.models_dolmen.output)
-   (deps (:input function.models.smt2))
+   (alias check-models)
+   (deps (:input twice_eq.models_dolmen.output) (:test twice_eq.models.smt2))
    (package alt-ergo)
    (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps function.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff function.models.expected function.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+    (with-accepted-exit-codes 0
+     (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target original.models_dolmen.output)
+ (deps (:input original.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps original.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff original.models.expected original.models_dolmen.output)))(rule
+                                                                    (alias check-models)
+                                                                    (deps (:input original.models_dolmen.output) (:test original.models.smt2))
+                                                                    (package alt-ergo)
+                                                                    (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+
+(rule
+ (target function.models_dolmen.output)
+ (deps (:input function.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps function.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff function.models.expected function.models_dolmen.output)))(rule
+                                                                    (alias check-models)
+                                                                    (deps (:input function.models_dolmen.output) (:test function.models.smt2))
+                                                                    (package alt-ergo)
+                                                                    (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir ite
   (rule
@@ -197175,11 +197219,8 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff ite-1.expected ite-1_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
-; Auto-generated part begin
+       (diff ite-1.expected ite-1_fpa.output)))) ; Auto-generated part end
+; File auto-generated by gentests  ; Auto-generated part begin
 (subdir let
   (rule
    (target testfile-let016_optimize.output)
@@ -209153,9 +209194,7 @@
      (package alt-ergo)
       (action
        (diff let--invalid-1.expected let--invalid-1_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
+; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir misc
   (rule
@@ -209721,14 +209760,12 @@
      (package alt-ergo)
       (action
        (diff unzip.ae.expected unzip.ae_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
+; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models
   (rule
-   (target check_sat.models_dolmen.output)
-   (deps (:input check_sat.models.ae))
+   (target complete_models.models_dolmen.output)
+   (deps (:input complete_models.models.smt2))
    (package alt-ergo)
    (action
     (chdir %{workspace_root}
@@ -209742,14 +209779,50 @@
              --frontend dolmen
              %{input})))))))
   (rule
-   (deps check_sat.models_dolmen.output)
+   (deps complete_models.models_dolmen.output)
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff check_sat.models.expected check_sat.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+       (diff complete_models.models.expected complete_models.models_dolmen.output)))
+  (rule
+   (alias check-models)
+   (deps (:input complete_models.models_dolmen.output) (:test complete_models.models.smt2))
+   (package alt-ergo)
+   (action
+    (with-accepted-exit-codes 0
+     (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
 
+(rule
+ (target check_sat.models_dolmen.output)
+ (deps (:input check_sat.models.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps check_sat.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff check_sat.models.expected check_sat.models_dolmen.output)))
+(rule
+ (alias check-models)
+ (deps (:input check_sat.models_dolmen.output) (:test check_sat.models.ae))
+ (package alt-ergo)
+ (action
+  (with-accepted-exit-codes 0
+   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models/arith
   (rule
@@ -209926,97 +209999,110 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff arith2.models.expected arith2.models_dolmen.output)))
-  (rule
-   (target arith12.optimize_optimize.output)
-   (deps (:input arith12.optimize.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps arith12.optimize_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff arith12.optimize.expected arith12.optimize_optimize.output)))
-  (rule
-   (target arith11.optimize_optimize.output)
-   (deps (:input arith11.optimize.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps arith11.optimize_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff arith11.optimize.expected arith11.optimize_optimize.output)))
-  (rule
-   (target arith10.optimize_optimize.output)
-   (deps (:input arith10.optimize.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             --optimize
-             %{input})))))))
-  (rule
-   (deps arith10.optimize_optimize.output)
-    (alias runtest)
-     (package alt-ergo)
-      (action
-       (diff arith10.optimize.expected arith10.optimize_optimize.output)))
-  (rule
-   (target arith1.models_dolmen.output)
-   (deps (:input arith1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps arith1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff arith1.models.expected arith1.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+       (diff arith2.models.expected arith2.models_dolmen.output)))(rule
+                                                                   (alias check-models)
+                                                                   (deps (:input arith2.models_dolmen.output) (:test arith2.models.smt2))
+                                                                   (package alt-ergo)
+                                                                   (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+
+(rule
+ (target arith12.optimize_optimize.output)
+ (deps (:input arith12.optimize.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps arith12.optimize_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff arith12.optimize.expected arith12.optimize_optimize.output)))
+(rule
+ (target arith11.optimize_optimize.output)
+ (deps (:input arith11.optimize.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps arith11.optimize_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff arith11.optimize.expected arith11.optimize_optimize.output)))
+(rule
+ (target arith10.optimize_optimize.output)
+ (deps (:input arith10.optimize.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           --optimize
+           %{input})))))))
+(rule
+ (deps arith10.optimize_optimize.output)
+  (alias runtest)
+   (package alt-ergo)
+    (action
+     (diff arith10.optimize.expected arith10.optimize_optimize.output)))
+(rule
+ (target arith1.models_dolmen.output)
+ (deps (:input arith1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps arith1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff arith1.models.expected arith1.models_dolmen.output)))(rule
+                                                                 (alias check-models)
+                                                                 (deps (:input arith1.models_dolmen.output) (:test arith1.models.smt2))
+                                                                 (package alt-ergo)
+                                                                 (action
+                                                                  (with-accepted-exit-codes 0
+                                                                   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models/array
   (rule
@@ -210041,29 +210127,43 @@
       (action
        (diff embedded-array.models.expected embedded-array.models_dolmen.output)))
   (rule
-   (target array1.models_dolmen.output)
-   (deps (:input array1.models.smt2))
+   (alias check-models)
+   (deps (:input embedded-array.models_dolmen.output) (:test embedded-array.models.smt2))
    (package alt-ergo)
    (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps array1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff array1.models.expected array1.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+    (with-accepted-exit-codes 0
+     (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target array1.models_dolmen.output)
+ (deps (:input array1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps array1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff array1.models.expected array1.models_dolmen.output)))(rule
+                                                                 (alias check-models)
+                                                                 (deps (:input array1.models_dolmen.output) (:test array1.models.smt2))
+                                                                 (package alt-ergo)
+                                                                 (action
+                                                                  (with-accepted-exit-codes 0
+                                                                   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models/bitv
   (rule
@@ -210088,239 +210188,335 @@
       (action
        (diff specified.models.expected specified.models_dolmen.output)))
   (rule
-   (target not.models_dolmen.output)
-   (deps (:input not.models.smt2))
+   (alias check-models)
+   (deps (:input specified.models_dolmen.output) (:test specified.models.smt2))
    (package alt-ergo)
    (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps not.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff not.models.expected not.models_dolmen.output)))
-  (rule
-   (target manyslice.models_dolmen.output)
-   (deps (:input manyslice.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps manyslice.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff manyslice.models.expected manyslice.models_dolmen.output)))
-  (rule
-   (target extract.models_dolmen.output)
-   (deps (:input extract.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps extract.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff extract.models.expected extract.models_dolmen.output)))
-  (rule
-   (target cs-soundness.models_dolmen.output)
-   (deps (:input cs-soundness.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps cs-soundness.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff cs-soundness.models.expected cs-soundness.models_dolmen.output)))
-  (rule
-   (target cardinal.models_dolmen.output)
-   (deps (:input cardinal.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps cardinal.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff cardinal.models.expected cardinal.models_dolmen.output)))
-  (rule
-   (target bvxor-2.models_dolmen.output)
-   (deps (:input bvxor-2.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps bvxor-2.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff bvxor-2.models.expected bvxor-2.models_dolmen.output)))
-  (rule
-   (target bvxor-1.models_dolmen.output)
-   (deps (:input bvxor-1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps bvxor-1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff bvxor-1.models.expected bvxor-1.models_dolmen.output)))
-  (rule
-   (target bvor-2.models_dolmen.output)
-   (deps (:input bvor-2.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps bvor-2.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff bvor-2.models.expected bvor-2.models_dolmen.output)))
-  (rule
-   (target bvor-1.models_dolmen.output)
-   (deps (:input bvor-1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps bvor-1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff bvor-1.models.expected bvor-1.models_dolmen.output)))
-  (rule
-   (target bvand-2.models_dolmen.output)
-   (deps (:input bvand-2.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps bvand-2.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff bvand-2.models.expected bvand-2.models_dolmen.output)))
-  (rule
-   (target bvand-1.models_dolmen.output)
-   (deps (:input bvand-1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps bvand-1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff bvand-1.models.expected bvand-1.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+    (with-accepted-exit-codes 0
+     (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target not.models_dolmen.output)
+ (deps (:input not.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps not.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff not.models.expected not.models_dolmen.output)))(rule
+                                                           (alias check-models)
+                                                           (deps (:input not.models_dolmen.output) (:test not.models.smt2))
+                                                           (package alt-ergo)
+                                                           (action
+                                                            (with-accepted-exit-codes 0
+                                                             (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target manyslice.models_dolmen.output)
+ (deps (:input manyslice.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps manyslice.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff manyslice.models.expected manyslice.models_dolmen.output)))
+(rule
+ (alias check-models)
+ (deps (:input manyslice.models_dolmen.output) (:test manyslice.models.smt2))
+ (package alt-ergo)
+ (action
+  (with-accepted-exit-codes 0
+   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target extract.models_dolmen.output)
+ (deps (:input extract.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps extract.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff extract.models.expected extract.models_dolmen.output)))(rule
+                                                                   (alias check-models)
+                                                                   (deps (:input extract.models_dolmen.output) (:test extract.models.smt2))
+                                                                   (package alt-ergo)
+                                                                   (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target cs-soundness.models_dolmen.output)
+ (deps (:input cs-soundness.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps cs-soundness.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff cs-soundness.models.expected cs-soundness.models_dolmen.output)))
+(rule
+ (alias check-models)
+ (deps (:input cs-soundness.models_dolmen.output) (:test cs-soundness.models.smt2))
+ (package alt-ergo)
+ (action
+  (with-accepted-exit-codes 0
+   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+
+(rule
+ (target cardinal.models_dolmen.output)
+ (deps (:input cardinal.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps cardinal.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff cardinal.models.expected cardinal.models_dolmen.output)))(rule
+                                                                    (alias check-models)
+                                                                    (deps (:input cardinal.models_dolmen.output) (:test cardinal.models.smt2))
+                                                                    (package alt-ergo)
+                                                                    (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target bvxor-2.models_dolmen.output)
+ (deps (:input bvxor-2.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps bvxor-2.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff bvxor-2.models.expected bvxor-2.models_dolmen.output)))(rule
+                                                                   (alias check-models)
+                                                                   (deps (:input bvxor-2.models_dolmen.output) (:test bvxor-2.models.smt2))
+                                                                   (package alt-ergo)
+                                                                   (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target bvxor-1.models_dolmen.output)
+ (deps (:input bvxor-1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps bvxor-1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff bvxor-1.models.expected bvxor-1.models_dolmen.output)))(rule
+                                                                   (alias check-models)
+                                                                   (deps (:input bvxor-1.models_dolmen.output) (:test bvxor-1.models.smt2))
+                                                                   (package alt-ergo)
+                                                                   (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target bvor-2.models_dolmen.output)
+ (deps (:input bvor-2.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps bvor-2.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff bvor-2.models.expected bvor-2.models_dolmen.output)))(rule
+                                                                 (alias check-models)
+                                                                 (deps (:input bvor-2.models_dolmen.output) (:test bvor-2.models.smt2))
+                                                                 (package alt-ergo)
+                                                                 (action
+                                                                  (with-accepted-exit-codes 0
+                                                                   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target bvor-1.models_dolmen.output)
+ (deps (:input bvor-1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps bvor-1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff bvor-1.models.expected bvor-1.models_dolmen.output)))(rule
+                                                                 (alias check-models)
+                                                                 (deps (:input bvor-1.models_dolmen.output) (:test bvor-1.models.smt2))
+                                                                 (package alt-ergo)
+                                                                 (action
+                                                                  (with-accepted-exit-codes 0
+                                                                   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target bvand-2.models_dolmen.output)
+ (deps (:input bvand-2.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps bvand-2.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff bvand-2.models.expected bvand-2.models_dolmen.output)))(rule
+                                                                   (alias check-models)
+                                                                   (deps (:input bvand-2.models_dolmen.output) (:test bvand-2.models.smt2))
+                                                                   (package alt-ergo)
+                                                                   (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target bvand-1.models_dolmen.output)
+ (deps (:input bvand-1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps bvand-1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff bvand-1.models.expected bvand-1.models_dolmen.output)))(rule
+                                                                   (alias check-models)
+                                                                   (deps (:input bvand-1.models_dolmen.output) (:test bvand-1.models.smt2))
+                                                                   (package alt-ergo)
+                                                                   (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models/bool
   (rule
@@ -210343,52 +210539,73 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff bool3.models.expected bool3.models_dolmen.output)))
-  (rule
-   (target bool2.models_dolmen.output)
-   (deps (:input bool2.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps bool2.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff bool2.models.expected bool2.models_dolmen.output)))
-  (rule
-   (target bool1.models_dolmen.output)
-   (deps (:input bool1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps bool1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff bool1.models.expected bool1.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+       (diff bool3.models.expected bool3.models_dolmen.output)))(rule
+                                                                 (alias check-models)
+                                                                 (deps (:input bool3.models_dolmen.output) (:test bool3.models.smt2))
+                                                                 (package alt-ergo)
+                                                                 (action
+                                                                  (with-accepted-exit-codes 0
+                                                                   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target bool2.models_dolmen.output)
+ (deps (:input bool2.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps bool2.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff bool2.models.expected bool2.models_dolmen.output)))(rule
+                                                               (alias check-models)
+                                                               (deps (:input bool2.models_dolmen.output) (:test bool2.models.smt2))
+                                                               (package alt-ergo)
+                                                               (action
+                                                                (with-accepted-exit-codes 0
+                                                                 (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target bool1.models_dolmen.output)
+ (deps (:input bool1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps bool1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff bool1.models.expected bool1.models_dolmen.output)))(rule
+                                                               (alias check-models)
+                                                               (deps (:input bool1.models_dolmen.output) (:test bool1.models.smt2))
+                                                               (package alt-ergo)
+                                                               (action
+                                                                (with-accepted-exit-codes 0
+                                                                 (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models/issues
   (rule
@@ -210411,10 +210628,15 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff 719.models.err.expected 719.models.err_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+       (diff 719.models.err.expected 719.models.err_dolmen.output)))(rule
+                                                                    (alias check-models)
+                                                                    (deps (:input 719.models.err_dolmen.output) (:test 719.models.err.smt2))
+                                                                    (package alt-ergo)
+                                                                    (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models/issues/715
   (rule
@@ -210437,31 +210659,44 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff 715_2.models.expected 715_2.models_dolmen.output)))
-  (rule
-   (target 715_1.models_dolmen.output)
-   (deps (:input 715_1.models.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps 715_1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff 715_1.models.expected 715_1.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+       (diff 715_2.models.expected 715_2.models_dolmen.output)))(rule
+                                                                 (alias check-models)
+                                                                 (deps (:input 715_2.models_dolmen.output) (:test 715_2.models.smt2))
+                                                                 (package alt-ergo)
+                                                                 (action
+                                                                  (with-accepted-exit-codes 0
+                                                                   (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+
+(rule
+ (target 715_1.models_dolmen.output)
+ (deps (:input 715_1.models.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps 715_1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff 715_1.models.expected 715_1.models_dolmen.output)))(rule
+                                                               (alias check-models)
+                                                               (deps (:input 715_1.models_dolmen.output) (:test 715_1.models.ae))
+                                                               (package alt-ergo)
+                                                               (action
+                                                                (with-accepted-exit-codes 0
+                                                                 (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models/records
   (rule
@@ -210484,52 +210719,73 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff record3.models.expected record3.models_dolmen.output)))
-  (rule
-   (target record2.models_dolmen.output)
-   (deps (:input record2.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps record2.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff record2.models.expected record2.models_dolmen.output)))
-  (rule
-   (target record1.models_dolmen.output)
-   (deps (:input record1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps record1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff record1.models.expected record1.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+       (diff record3.models.expected record3.models_dolmen.output)))(rule
+                                                                    (alias check-models)
+                                                                    (deps (:input record3.models_dolmen.output) (:test record3.models.smt2))
+                                                                    (package alt-ergo)
+                                                                    (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+
+(rule
+ (target record2.models_dolmen.output)
+ (deps (:input record2.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps record2.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff record2.models.expected record2.models_dolmen.output)))(rule
+                                                                   (alias check-models)
+                                                                   (deps (:input record2.models_dolmen.output) (:test record2.models.smt2))
+                                                                   (package alt-ergo)
+                                                                   (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target record1.models_dolmen.output)
+ (deps (:input record1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps record1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff record1.models.expected record1.models_dolmen.output)))(rule
+                                                                   (alias check-models)
+                                                                   (deps (:input record1.models_dolmen.output) (:test record1.models.smt2))
+                                                                   (package alt-ergo)
+                                                                   (action
+                                                                    (with-accepted-exit-codes 0
+                                                                    (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir models/uf
   (rule
@@ -210552,31 +210808,44 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff uf2.models.expected uf2.models_dolmen.output)))
-  (rule
-   (target uf1.models_dolmen.output)
-   (deps (:input uf1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes (or 0)
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps uf1.models_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff uf1.models.expected uf1.models_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+       (diff uf2.models.expected uf2.models_dolmen.output)))(rule
+                                                             (alias check-models)
+                                                             (deps (:input uf2.models_dolmen.output) (:test uf2.models.smt2))
+                                                             (package alt-ergo)
+                                                             (action
+                                                              (with-accepted-exit-codes 0
+                                                               (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
+
+
+(rule
+ (target uf1.models_dolmen.output)
+ (deps (:input uf1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes (or 0)
+      (run %{bin:alt-ergo}
+           --timelimit=2
+           --enable-assertions
+           --output=smtlib2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (deps uf1.models_dolmen.output)
+  (alias runtest-quick)
+   (package alt-ergo)
+    (action
+     (diff uf1.models.expected uf1.models_dolmen.output)))(rule
+                                                           (alias check-models)
+                                                           (deps (:input uf1.models_dolmen.output) (:test uf1.models.smt2))
+                                                           (package alt-ergo)
+                                                           (action
+                                                            (with-accepted-exit-codes 0
+                                                             (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}"))))
 
+) ; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir polymorphism
   (rule
@@ -212915,9 +213184,7 @@
      (package alt-ergo)
       (action
        (diff testfile-polymorphism001.expected testfile-polymorphism001_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
+; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir quantifiers
   (rule
@@ -221972,9 +222239,7 @@
      (package alt-ergo)
       (action
        (diff testfile-github001.expected testfile-github001_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
+; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir smtlib
   (rule
@@ -222834,9 +223099,7 @@
      (package alt-ergo)
       (action
        (diff testfile-echo1.dolmen.expected testfile-echo1.dolmen_dolmen.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
+; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir sum
   (rule
@@ -228387,9 +228650,7 @@
      (package alt-ergo)
       (action
        (diff testfile-sum001.expected testfile-sum001_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
+; Auto-generated part end ; File auto-generated by gentests 
 ; Auto-generated part begin
 (subdir typing
   (rule
diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected
index 086ba7ffb..b35225efb 100644
--- a/tests/issues/555.models.expected
+++ b/tests/issues/555.models.expected
@@ -3,6 +3,6 @@ unknown
 (
   (define-fun x () Int 0)
   (define-fun y () Int 0)
-  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
 )
diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected
index bb0b49fe0..88a28c7d8 100644
--- a/tests/issues/854/function.models.expected
+++ b/tests/issues/854/function.models.expected
@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref))
   (define-fun a () Int 0)
   (define-fun f ((_arg_0 Int)) Int 0)
   (define-fun a1 () Int 0)
diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected
index 9198abbbf..8fbfb8105 100644
--- a/tests/issues/854/original.models.expected
+++ b/tests/issues/854/original.models.expected
@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )
diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected
index f18c7f58e..c51afd4a7 100644
--- a/tests/issues/854/twice_eq.models.expected
+++ b/tests/issues/854/twice_eq.models.expected
@@ -1,8 +1,8 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
-  (define-fun another_mk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref))
+  (define-fun another_mk ((_arg_0 Int)) intref (as @a6 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )
diff --git a/tests/models/arith/arith11.optimize.expected b/tests/models/arith/arith11.optimize.expected
index 99f7450f0..722135b53 100644
--- a/tests/models/arith/arith11.optimize.expected
+++ b/tests/models/arith/arith11.optimize.expected
@@ -4,6 +4,7 @@ unknown
   (define-fun p1 () Bool false)
   (define-fun p2 () Bool true)
   (define-fun x () Real 2.0)
+  (define-fun y () Real (as @a3 Real))
 )
 (objectives 
   (x 2.0)
diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected
index 086ba7ffb..b35225efb 100644
--- a/tests/models/array/array1.models.expected
+++ b/tests/models/array/array1.models.expected
@@ -3,6 +3,6 @@ unknown
 (
   (define-fun x () Int 0)
   (define-fun y () Int 0)
-  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
 )
diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected
index dd6a80ae9..057bc1a6c 100644
--- a/tests/models/array/embedded-array.models.expected
+++ b/tests/models/array/embedded-array.models.expected
@@ -1,8 +1,8 @@
 
 unknown
 (
-  (define-fun s () S (as @a0 S))
+  (define-fun s () S (as @a2 S))
   (define-fun x () Pair
-   (pair (store (as @a1 (Array Int S)) 0 s)
-         (store (as @a1 (Array Int S)) 0 s)))
+   (pair (store (as @a3 (Array Int S)) 0 s)
+         (store (as @a3 (Array Int S)) 0 s)))
 )
diff --git a/tests/models/bool/bool2.models.expected b/tests/models/bool/bool2.models.expected
index e0f6879b8..7d4b0eed7 100644
--- a/tests/models/bool/bool2.models.expected
+++ b/tests/models/bool/bool2.models.expected
@@ -2,6 +2,7 @@
 unknown
 (
   (define-fun x () Bool false)
+  (define-fun y () Bool (as @a1 Bool))
 )
 ((notx true))
 
diff --git a/tests/models/complete_models.models.expected b/tests/models/complete_models.models.expected
new file mode 100644
index 000000000..49667d5f1
--- /dev/null
+++ b/tests/models/complete_models.models.expected
@@ -0,0 +1,36 @@
+
+unknown
+(
+  (define-fun x () Int (as @a0 Int))
+)
+
+unknown
+(
+  (define-fun x () Int 5)
+  (define-fun y () Int (as @a2 Int))
+)
+
+unknown
+(
+  (define-fun x () Int 6)
+)
+
+unknown
+(
+  (define-fun x () Int 6)
+  (define-fun z () S (as @a5 S))
+)
+
+unknown
+(
+  (define-fun x () Int 6)
+  (define-fun z () S (as @a7 S))
+  (define-fun f ((_arg_0 Int)) Int (as @a9 Int))
+)
+
+unknown
+(
+  (define-fun x () Int 6)
+  (define-fun z () S (as @a11 S))
+  (define-fun f ((_arg_0 Int)) Int 2)
+)
diff --git a/tests/models/complete_models.models.smt2 b/tests/models/complete_models.models.smt2
new file mode 100644
index 000000000..c65cf1d89
--- /dev/null
+++ b/tests/models/complete_models.models.smt2
@@ -0,0 +1,24 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x Int)
+(check-sat)
+(get-model)
+(push 1)
+(declare-const y Int)
+(assert (= x 5))
+(check-sat)
+(get-model)
+(pop 1)
+(assert (= x 6))
+(check-sat)
+(get-model)
+(declare-sort S 0)
+(declare-const z S)
+(check-sat)
+(get-model)
+(declare-fun f (Int) Int)
+(check-sat)
+(get-model)
+(assert (= (f 5) 2))
+(check-sat)
+(get-model)
diff --git a/tools/gentest.ml b/tools/gentest.ml
index 71300e52b..2767c56ae 100644
--- a/tools/gentest.ml
+++ b/tools/gentest.ml
@@ -118,13 +118,15 @@ module Test : sig
   type t = private {
     cmd: Cmd.t;
     pb_file: string;
-    params: params
+    params: params;
+    check_model: bool;
   }
   (** Type of a test. *)
 
   val base_params : params
 
-  val make: cmd: Cmd.t -> pb_file: string -> params:params -> t
+  val make: cmd: Cmd.t -> pb_file: string -> check_model: bool ->
+    params: params -> t
   (** Set up the test. *)
 
   val pp_expected_output: t printer
@@ -145,6 +147,7 @@ end = struct
     cmd: Cmd.t;
     pb_file: string;
     params: params;
+    check_model: bool;
   }
 
   let base_params = {
@@ -154,7 +157,8 @@ end = struct
     accepted_exit_codes = [0];
   }
 
-  let make ~cmd ~pb_file ~params = {cmd; pb_file; params}
+  let make ~cmd ~pb_file ~check_model ~params =
+    {cmd; pb_file; check_model; params}
 
   let pp_output fmt tst =
     let filename = Filename.chop_extension tst.pb_file in
@@ -206,7 +210,23 @@ end = struct
       Cmd.pp tst.cmd
       pp_output tst
       (Cmd.group tst.cmd)
-      pp_diff_command tst
+      pp_diff_command tst;
+    let () =
+      if tst.check_model then
+        Format.fprintf fmt "\
+@[<v 1>\
+(rule@,\
+(alias check-models)@,\
+(deps (:input %a) (:test %s))@,\
+(package alt-ergo)@,\
+@[<v 1>(action@,\
+@[<v 1>(with-accepted-exit-codes 0@,\
+@[<v 1>(bash \"sed 's/^unknown/sat/' %%{input} | \
+opam exec -- dolmen --check-model true %%{test}\"))))@]@]@]@]\n@."
+          pp_output tst
+          tst.pb_file
+    in
+    ()
 end
 
 module Batch : sig
@@ -277,7 +297,11 @@ end = struct
         in
         List.fold_left (fun acc2 cmd ->
             if filter params cmd then
-              Test.make ~cmd ~pb_file ~params :: acc2
+              let check_model =
+                List.exists (String.equal "models")
+                  (String.split_on_char '.' pb_file)
+              in
+              Test.make ~cmd ~pb_file ~check_model ~params :: acc2
             else
               acc2
           ) acc1 cmds) [] pb_files