diff --git a/tests/dune.inc b/tests/dune.inc
index ad1bd4a1f..20af14689 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -175753,257 +175753,8 @@
 ; Auto-generated part begin
 (subdir float
   (rule
-   (target test_float3_ci_cdcl_no_minimal_bj.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_ci_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_ci_cdcl_no_minimal_bj.output)))
-  (rule
-   (target test_float3_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
-  (rule
-   (target test_float3_ci_no_tableaux_cdcl_in_instantiation.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_ci_no_tableaux_cdcl_in_instantiation.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_ci_no_tableaux_cdcl_in_instantiation.output)))
-  (rule
-   (target test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
-  (rule
-   (target test_float3_ci_tableaux_cdcl_no_minimal_bj.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_ci_tableaux_cdcl_no_minimal_bj.output)
-    (alias runtest-ci)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_ci_tableaux_cdcl_no_minimal_bj.output)))
-  (rule
-   (target test_float3_cdcl.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_cdcl.output)))
-  (rule
-   (target test_float3_tableaux_cdcl.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_tableaux_cdcl.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_tableaux_cdcl.output)))
-  (rule
-   (target test_float3_tableaux.output)
-   (deps (:input test_float3.ae))
-   (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
-             %{input})))))))
-  (rule
-   (deps test_float3_tableaux.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_tableaux.output)))
-  (rule
-   (target test_float3_legacy.output)
-   (deps (:input test_float3.ae))
-   (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 legacy
-             %{input})))))))
-  (rule
-   (deps test_float3_legacy.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_legacy.output)))
-  (rule
-   (target test_float3_dolmen.output)
-   (deps (:input test_float3.ae))
-   (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 test_float3_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff test_float3.expected test_float3_dolmen.output)))
-  (rule
-   (target test_float3_fpa.output)
-   (deps (:input test_float3.ae))
+   (target test_float3.fpa_fpa.output)
+   (deps (:input test_float3.fpa.ae))
    (package alt-ergo)
    (action
     (chdir %{workspace_root}
@@ -176017,11 +175768,11 @@
              --enable-theories fpa
              %{input})))))))
   (rule
-   (deps test_float3_fpa.output)
+   (deps test_float3.fpa_fpa.output)
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff test_float3.expected test_float3_fpa.output)))
+       (diff test_float3.fpa.expected test_float3.fpa_fpa.output)))
   (rule
    (target test_float2.models_tableaux.output)
    (deps (:input test_float2.models.smt2))
diff --git a/tests/float/test_float3.fpa.ae b/tests/float/test_float3.fpa.ae
new file mode 100644
index 000000000..3067a37b5
--- /dev/null
+++ b/tests/float/test_float3.fpa.ae
@@ -0,0 +1,5 @@
+logic x : real
+
+axiom ax : 1.0 <= x
+
+goal g : float(4, 4, NearestTiesToEven, 1.0) <= float(4, 4, NearestTiesToEven, x)
\ No newline at end of file
diff --git a/tests/float/test_float3.fpa.expected b/tests/float/test_float3.fpa.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/float/test_float3.fpa.expected
@@ -0,0 +1,2 @@
+
+unsat