diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 516e99f48..fe1fff77c 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -1472,8 +1472,14 @@ let rec mk_expr
         ) body binders
 
       | Binder ((Forall (tyvl, tvl) | Exists (tyvl, tvl)) as e, body) ->
-        if tvl == []
-        then (Cache.store_tyvl tyvl; aux_mk_expr ~toplevel body)
+        if not toplevel && tyvl != [] then
+          Fmt.failwith "Non-prenex polymorphism in the term %a"
+            DE.Term.print term
+        else if tvl == []
+        then begin
+          Cache.store_tyvl tyvl;
+          aux_mk_expr ~toplevel:true body
+        end
         else
           let name =
             if !name_tag = 0 then name_base
@@ -1518,7 +1524,7 @@ let rec mk_expr
             end
           in
           let in_theory = decl_kind == E.Dtheory in
-          let f = aux_mk_expr ~toplevel body in
+          let f = aux_mk_expr ~toplevel:false body in
           let qbody = E.purify_form f in
           (*  All the triggers that are encoutered at this level are assumed
               to be user-defined. *)
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index c9b6e1d60..4922692f9 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -72,7 +72,24 @@ and quantified = private {
   (** The underlying formula. *)
 
   toplevel : bool;
-  (** Determine if the quantified formula is at the top level.
+  (** Determine if the quantified formula is at the top level of an asserted
+      formula.
+
+      An {e asserted formula} is a formula introduced by [(assert ...)] or
+      generated by a function definition with [(define-fun ...)].
+
+      By {e top level}, we mean that the quantified formula is not
+      a subformula of another quantified formula.
+
+      For instance, the subformula ∀y:int. ¬G(y) of the asserted formula
+      ¬(∀y:int. ¬G(y)) is also considered at the top level.
+
+      Notice that quantifiers of the same kind are packed as much as possible.
+      For instance, if we assert the formula:
+        ∀α. ∀x:list α. ∃y:α. F(x, y)
+      Then the two universal quantifiers are packed in a same top level formula
+      but the subformula ∃y:α. F(x, y) is not at the top level.
+
       This flag is important for the prenex polymorphism.
       - If this flag is [true], all the free type variables of [main]
         are implicitely considered as quantified.
diff --git a/tests/dune.inc b/tests/dune.inc
index 88dec1477..e40934009 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -180084,7 +180084,277 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff 1111.expected 1111_fpa.output))))
+       (diff 1111.expected 1111_fpa.output)))
+  (rule
+   (target 1099_ci_cdcl_no_minimal_bj.output)
+   (deps (:input 1099.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 1099_ci_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 1099_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 1099.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 1099_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 1099.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 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 1099_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input 1099.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 1099_ci_no_tableaux_cdcl_in_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input 1099.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 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target 1099_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input 1099.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 1099_ci_tableaux_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 1099_cdcl.output)
+   (deps (:input 1099.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 1099_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_cdcl.output)))
+  (rule
+   (target 1099_tableaux_cdcl.output)
+   (deps (:input 1099.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 1099_tableaux_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_tableaux_cdcl.output)))
+  (rule
+   (target 1099_tableaux.output)
+   (deps (:input 1099.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 1099_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_tableaux.output)))
+  (rule
+   (target 1099_legacy.output)
+   (deps (:input 1099.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 1099_legacy.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_legacy.output)))
+  (rule
+   (target 1099_dolmen.output)
+   (deps (:input 1099.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 1099_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_dolmen.output)))
+  (rule
+   (target 1099_fpa.output)
+   (deps (:input 1099.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 1099_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_fpa.output))))
 ; Auto-generated part end
 ; File auto-generated by gentests
 
diff --git a/tests/issues/1099.ae b/tests/issues/1099.ae
new file mode 100644
index 000000000..f68308d02
--- /dev/null
+++ b/tests/issues/1099.ae
@@ -0,0 +1,8 @@
+type 'a t
+logic p : 'a t, unit -> prop
+logic f : 'a t -> prop
+logic r : unit t
+
+axiom a : forall s:'a t. exists n:unit. p(s, n)
+
+goal g : f(r)
diff --git a/tests/issues/1099.expected b/tests/issues/1099.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/issues/1099.expected
@@ -0,0 +1,2 @@
+
+unknown