Remove ulevel nat axiom

examples/data_structures/RBTreeIntrinsic.fst

@@ -32,7 +32,7 @@
 module RBTreeIntrinsic
 
 /// Much of the file verifies with fuel=0, max_ifuel=1
-#set-options "--max_fuel 2 --max_ifuel 2 --z3rlimit 80"
+#set-options "--max_fuel 2 --max_ifuel 2 --z3rlimit 80 --z3refresh"
 
 type color =
 | Red

src/smtencoding/FStarC.SMTEncoding.Encode.fst

@@ -1981,7 +1981,9 @@ let encode_env_bindings (env:env_t) (bindings:list S.binding) : ML (decls_t & en
     let encode_binding b (i, decls, env) = match b with
         | S.Binding_univ u ->
           let u_fv, u_tm = EncodeTerm.encode_univ_name u in
-          let decls' = [Term.DeclFun(fv_name u_fv, [], univ_sort, Some "universe local constant")] |> mk_decls_trivial in
+          let decls' = [
+            Term.DeclFun(fv_name u_fv, [], univ_sort, Some "universe local constant");
+            Util.mkAssume (mkApp("univ_ok", [u_tm]), Some ("univ_ok_" ^ fv_name u_fv), "univ_ok_" ^ fv_name u_fv)] |> mk_decls_trivial in
           i+1, decls@decls', env
 
         | S.Binding_var x ->

src/smtencoding/FStarC.SMTEncoding.Term.fst

@@ -980,7 +980,8 @@ and mkPrelude z3options : ML string =
                                 (! (= (U_max u1 u2)\n\
                                       (Univ (imax (ulevel u1) (ulevel u2))))\n\
                                  :pattern ((U_max u1 u2)))))\n\
-                (assert (forall ((u Universe)) (>= (ulevel u) 0)))\n\
+                (define-fun univ_ok ((u Universe)) Bool\n\
+                    (>= (ulevel u) 0))\n\
                 (declare-fun U_unif (Int) Universe)\n\
                 (declare-fun U_unknown () Universe)\n\
                 (declare-fun Term_constr_id (Term) Int)\n\