diff --git a/Makefile b/Makefile
index cd56bd6b88..bde15dd6fc 100644
--- a/Makefile
+++ b/Makefile
@@ -126,7 +126,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 1c1da38843..fe75fe8c7f 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.4"}
   "seq"
diff --git a/dune-project b/dune-project
index ad75c36052..e640f74876 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.4))
   seq
diff --git a/tests/dune.inc b/tests/dune.inc
index a19c2a5084..3d9f716880 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -171682,1019 +171682,1024 @@
    (alias runtest-quick)
     (package alt-ergo)
      (action
-      (diff 555.models.expected 555.models_tableaux.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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 479.expected 479_tableaux.output)))
-  (rule
-   (target 479_legacy.output)
-   (deps (:input 479.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend legacy
-             --timelimit=2
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 479.expected 479_legacy.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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --timelimit=2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --timelimit=2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 479.expected 479_fpa.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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend legacy
-             --timelimit=2
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --timelimit=2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --timelimit=2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 460.expected 460_fpa.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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend legacy
-             --timelimit=2
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --timelimit=2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --timelimit=2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 350.expected 350_fpa.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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-instantiation
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-tableaux-cdcl-in-theories
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL-Tableaux
-             --no-minimal-bj
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver CDCL
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux-CDCL
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 340.expected 340_tableaux.output)))
-  (rule
-   (target 340_legacy.output)
-   (deps (:input 340.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend legacy
-             --timelimit=2
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 340.expected 340_legacy.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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --timelimit=2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (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 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --timelimit=2
-             --enable-theories fpa
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 340.expected 340_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+      (diff 555.models.expected 555.models_tableaux.output)))(rule
+                                                              (alias check-models)
+                                                              (deps (:input 555.models_tableaux.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}"))))
 
-; Auto-generated part begin
+
+(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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff 479.expected 479_tableaux.output)))
+(rule
+ (target 479_legacy.output)
+ (deps (:input 479.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend legacy
+           --timelimit=2
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff 479.expected 479_legacy.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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --timelimit=2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --timelimit=2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff 479.expected 479_fpa.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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend legacy
+           --timelimit=2
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --timelimit=2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --timelimit=2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff 460.expected 460_fpa.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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend legacy
+           --timelimit=2
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --timelimit=2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --timelimit=2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff 350.expected 350_fpa.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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-instantiation
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-tableaux-cdcl-in-theories
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL-Tableaux
+           --no-minimal-bj
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver CDCL
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux-CDCL
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff 340.expected 340_tableaux.output)))
+(rule
+ (target 340_legacy.output)
+ (deps (:input 340.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend legacy
+           --timelimit=2
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff 340.expected 340_legacy.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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --timelimit=2
+           --frontend dolmen
+           %{input})))))))
+(rule
+ (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 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --timelimit=2
+           --enable-theories fpa
+           %{input})))))))
+(rule
+ (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)
@@ -172966,11 +172971,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)
@@ -173242,11 +173244,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 ite
   (rule
    (target testfile-everything012_ci_cdcl_no_minimal_bj.output)
@@ -175555,11 +175554,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_ci_cdcl_no_minimal_bj.output)
@@ -186105,9 +186101,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
@@ -186620,9 +186614,7 @@
     (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
@@ -186644,10 +186636,16 @@
    (alias runtest-quick)
     (package alt-ergo)
      (action
-      (diff check_sat.models.expected check_sat.models_tableaux.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+      (diff check_sat.models.expected check_sat.models_tableaux.output)))
+  (rule
+   (alias check-models)
+   (deps (:input check_sat.models_tableaux.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
@@ -186669,30 +186667,43 @@
    (alias runtest-quick)
     (package alt-ergo)
      (action
-      (diff arith2.models.expected arith2.models_tableaux.output)))
-  (rule
-   (target arith1.models_tableaux.output)
-   (deps (:input arith1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff arith1.models.expected arith1.models_tableaux.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+      (diff arith2.models.expected arith2.models_tableaux.output)))(rule
+                                                                    (alias check-models)
+                                                                    (deps (:input arith2.models_tableaux.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 arith1.models_tableaux.output)
+ (deps (:input arith1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff arith1.models.expected arith1.models_tableaux.output)))(rule
+                                                                  (alias check-models)
+                                                                  (deps (:input arith1.models_tableaux.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/bool
   (rule
@@ -186714,30 +186725,43 @@
    (alias runtest-quick)
     (package alt-ergo)
      (action
-      (diff bool2.models.expected bool2.models_tableaux.output)))
-  (rule
-   (target bool1.models_tableaux.output)
-   (deps (:input bool1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff bool1.models.expected bool1.models_tableaux.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+      (diff bool2.models.expected bool2.models_tableaux.output)))(rule
+                                                                  (alias check-models)
+                                                                  (deps (:input bool2.models_tableaux.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_tableaux.output)
+ (deps (:input bool1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff bool1.models.expected bool1.models_tableaux.output)))(rule
+                                                                (alias check-models)
+                                                                (deps (:input bool1.models_tableaux.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
@@ -186759,10 +186783,15 @@
    (alias runtest-quick)
     (package alt-ergo)
      (action
-      (diff 719.models.expected 719.models_tableaux.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+      (diff 719.models.expected 719.models_tableaux.output)))(rule
+                                                              (alias check-models)
+                                                              (deps (:input 719.models_tableaux.output) (:test 719.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/715
   (rule
@@ -186784,30 +186813,43 @@
    (alias runtest-quick)
     (package alt-ergo)
      (action
-      (diff 715_2.models.expected 715_2.models_tableaux.output)))
-  (rule
-   (target 715_1.models_tableaux.output)
-   (deps (:input 715_1.models.ae))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff 715_1.models.expected 715_1.models_tableaux.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+      (diff 715_2.models.expected 715_2.models_tableaux.output)))(rule
+                                                                  (alias check-models)
+                                                                  (deps (:input 715_2.models_tableaux.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_tableaux.output)
+ (deps (:input 715_1.models.ae))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff 715_1.models.expected 715_1.models_tableaux.output)))(rule
+                                                                (alias check-models)
+                                                                (deps (:input 715_1.models_tableaux.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/uf
   (rule
@@ -186829,30 +186871,43 @@
    (alias runtest-quick)
     (package alt-ergo)
      (action
-      (diff uf2.models.expected uf2.models_tableaux.output)))
-  (rule
-   (target uf1.models_tableaux.output)
-   (deps (:input uf1.models.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes 0
-        (run %{bin:alt-ergo}
-             --output=smtlib2
-             --frontend dolmen
-             --timelimit=2
-             --sat-solver Tableaux
-             %{input})))))))
-  (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff uf1.models.expected uf1.models_tableaux.output))))
-; Auto-generated part end
-; File auto-generated by gentests
+      (diff uf2.models.expected uf2.models_tableaux.output)))(rule
+                                                              (alias check-models)
+                                                              (deps (:input uf2.models_tableaux.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_tableaux.output)
+ (deps (:input uf1.models.smt2))
+ (package alt-ergo)
+ (action
+  (chdir %{workspace_root}
+   (with-stdout-to %{target}
+    (ignore-stderr
+     (with-accepted-exit-codes 0
+      (run %{bin:alt-ergo}
+           --output=smtlib2
+           --frontend dolmen
+           --timelimit=2
+           --sat-solver Tableaux
+           %{input})))))))
+(rule
+ (alias runtest-quick)
+  (package alt-ergo)
+   (action
+    (diff uf1.models.expected uf1.models_tableaux.output)))(rule
+                                                            (alias check-models)
+                                                            (deps (:input uf1.models_tableaux.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
@@ -189014,11 +189069,8 @@
      (action
       (diff
         testfile-polymorphism001.expected
-        testfile-polymorphism001_fpa.output))))
-; Auto-generated part end
-; File auto-generated by gentests
-
-; Auto-generated part begin
+        testfile-polymorphism001_fpa.output)))) ; Auto-generated part end
+; File auto-generated by gentests  ; Auto-generated part begin
 (subdir quantifiers
   (rule
    (target testfile-quant014_ci_cdcl_no_minimal_bj.output)
@@ -197076,9 +197128,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 sum
   (rule
@@ -202007,9 +202057,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/tools/gentest.ml b/tools/gentest.ml
index 9c33cc17a6..6b63ddb9e2 100644
--- a/tools/gentest.ml
+++ b/tools/gentest.ml
@@ -109,11 +109,12 @@ end
 module Test : sig
   type t = private {
     cmd: Cmd.t;
-    pb_file: string
+    pb_file: string;
+    check_model: bool;
   }
   (** Type of a test. *)
 
-  val make: cmd: Cmd.t -> pb_file: string -> t
+  val make: cmd: Cmd.t -> pb_file: string -> check_model: bool -> t
   (** Set up the test. *)
 
   val pp_expected_output: t printer
@@ -124,10 +125,11 @@ module Test : sig
 end = struct
   type t = {
     cmd: Cmd.t;
-    pb_file: string
+    pb_file: string;
+    check_model: bool;
   }
 
-  let make ~cmd ~pb_file = {cmd; pb_file}
+  let make ~cmd ~pb_file ~check_model = {cmd; pb_file; check_model}
 
   let pp_output fmt tst =
     let filename = Filename.chop_extension tst.pb_file in
@@ -160,7 +162,23 @@ end = struct
       Cmd.pp tst.cmd
       (Cmd.group tst.cmd)
       pp_expected_output tst
-      pp_output tst
+      pp_output 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
@@ -210,7 +228,11 @@ end = struct
         in
         List.fold_left (fun acc2 cmd ->
             if filter ~exclude filters cmd then
-              Test.make ~cmd ~pb_file :: acc2
+              let check_model =
+                List.exists (String.equal "models")
+                  (String.split_on_char '.' pb_file)
+              in
+              Test.make ~cmd ~pb_file ~check_model :: acc2
             else
               acc2
           ) acc1 cmds) [] pb_files