From f91e02c43c1cdc2ba4988a50ff28d4a3550a1118 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Thu, 10 Aug 2023 13:56:40 +0200
Subject: [PATCH] Check ground models with Dolmen

---
 Makefile          |    2 +-
 alt-ergo-lib.opam |    1 +
 dune-project      |    1 +
 tests/dune.inc    | 6080 +++++++++++++++++++++++----------------------
 tools/gentest.ml  |   34 +-
 5 files changed, 3192 insertions(+), 2926 deletions(-)

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/tests/dune.inc b/tests/dune.inc
index e5b9775fc..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,9 +209760,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
@@ -209748,29 +209785,44 @@
       (action
        (diff complete_models.models.expected complete_models.models_dolmen.output)))
   (rule
-   (target check_sat.models_dolmen.output)
-   (deps (:input check_sat.models.ae))
+   (alias check-models)
+   (deps (:input complete_models.models_dolmen.output) (:test complete_models.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 check_sat.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
+    (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
@@ -209947,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
@@ -210062,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
@@ -210109,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
@@ -210364,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
@@ -210432,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
@@ -210458,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
@@ -210505,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
@@ -210573,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
@@ -212936,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
@@ -221993,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
@@ -222855,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
@@ -228408,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/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