Lem: Be more careful about nexps occurring in the function signature

Don't ask Z3 to simplify them, as flow typing might lead to different
results in different if-branches, for example, leading to type errors in
Lem.

1 files changed, 8 insertions, 8 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 5c67f93a..c0af581a 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -349,14 +349,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
        let mk_typ nexp =
          Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
-       match Type_check.solve env size with
-       | Some n -> mk_typ (nconstant n)
-       | None ->
-          let is_equal nexp =
-            prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
-          in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
-          | nexp -> mk_typ nexp
-          | exception Not_found -> None
+       let is_equal nexp =
+         prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+       in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
+       | nexp -> mk_typ nexp
+       | exception Not_found ->
+          match Type_check.solve env size with
+          | Some n -> mk_typ (nconstant n)
+          | None -> None
      end
   | _ -> None