diff --git a/tests/dune.inc b/tests/dune.inc
index 62c46b4bfb..ac01873cfa 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -193318,6 +193318,191 @@
 
 ; Auto-generated part begin
 (subdir models/array
+  (rule
+   (target array1.models_ci_cdcl_no_minimal_bj.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps array1.models_ci_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target array1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 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 array1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 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 array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target array1.models_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 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 array1.models_ci_no_tableaux_cdcl_in_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 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 array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target array1.models_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps array1.models_ci_tableaux_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target array1.models_cdcl.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             %{input})))))))
+  (rule
+   (deps array1.models_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_cdcl.output)))
+  (rule
+   (target array1.models_tableaux_cdcl.output)
+   (deps (:input array1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux-CDCL
+             %{input})))))))
+  (rule
+   (deps array1.models_tableaux_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_tableaux_cdcl.output)))
   (rule
    (target array1.models_tableaux.output)
    (deps (:input array1.models.smt2))
@@ -193335,10 +193520,32 @@
              --sat-solver Tableaux
              %{input})))))))
   (rule
-   (alias runtest-quick)
-    (package alt-ergo)
-     (action
-      (diff array1.models.expected array1.models_tableaux.output))))
+   (deps array1.models_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff array1.models.expected array1.models_tableaux.output)))
+  (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 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