Fix issue 1099

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. *)

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.

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)

tests/issues/1099.expected

@@ -0,0 +1,2 @@
+
+unknown