snap

kkohbrok · Jan 10, 2018 · 0b9a4a6 · 0b9a4a6
1 parent b3ccab9
commit 0b9a4a6
Show file tree

Hide file tree

Showing 22 changed files with 20,149 additions and 19,993 deletions.
diff --git a/src/ocaml-output/FStar_Errors.ml b/src/ocaml-output/FStar_Errors.ml
diff --git a/src/ocaml-output/FStar_Extraction_Kremlin.ml b/src/ocaml-output/FStar_Extraction_Kremlin.ml
diff --git a/src/ocaml-output/FStar_Extraction_ML_Code.ml b/src/ocaml-output/FStar_Extraction_ML_Code.ml
diff --git a/src/ocaml-output/FStar_Extraction_ML_Modul.ml b/src/ocaml-output/FStar_Extraction_ML_Modul.ml
diff --git a/src/ocaml-output/FStar_Extraction_ML_Syntax.ml b/src/ocaml-output/FStar_Extraction_ML_Syntax.ml
diff --git a/src/ocaml-output/FStar_Extraction_ML_Term.ml b/src/ocaml-output/FStar_Extraction_ML_Term.ml
diff --git a/src/ocaml-output/FStar_Options.ml b/src/ocaml-output/FStar_Options.ml
diff --git a/src/ocaml-output/FStar_Parser_Const.ml b/src/ocaml-output/FStar_Parser_Const.ml
@@ -159,6 +159,7 @@ let range_0: FStar_Ident.lident = pconst "range_0"
 let guard_free: FStar_Ident.lident = pconst "guard_free"
 let inversion_lid: FStar_Ident.lident =
   p2l ["FStar"; "Pervasives"; "inversion"]
+let with_type_lid: FStar_Ident.lident = pconst "with_type"
 let normalize: FStar_Ident.lident = pconst "normalize"
 let normalize_term: FStar_Ident.lident = pconst "normalize_term"
 let norm: FStar_Ident.lident = pconst "norm"

diff --git a/src/ocaml-output/FStar_SMTEncoding_Encode.ml b/src/ocaml-output/FStar_SMTEncoding_Encode.ml
diff --git a/src/ocaml-output/FStar_SMTEncoding_Z3.ml b/src/ocaml-output/FStar_SMTEncoding_Z3.ml
@@ -95,8 +95,8 @@ let ini_params: Prims.unit -> Prims.string =
                FStar_Util.string_of_int uu____310 in
              FStar_Util.format1 "smt.random_seed=%s" uu____309 in
            [uu____308] in
-         "-smt2 -in auto_config=false model=true smt.relevancy=2" ::
-           uu____305 in
+         "-smt2 -in auto_config=false model=true smt.relevancy=2 smt.case_split=3"
+           :: uu____305 in
        let uu____311 = FStar_Options.z3_cliopt () in
        FStar_List.append uu____302 uu____311 in
      FStar_String.concat " " uu____299)

diff --git a/src/ocaml-output/FStar_Syntax_Print.ml b/src/ocaml-output/FStar_Syntax_Print.ml
@@ -667,7 +667,7 @@ and lcomp_to_string: FStar_Syntax_Syntax.lcomp -> Prims.string =
     let uu____1782 = FStar_Options.print_effect_args () in
     if uu____1782
     then
-      let uu____1783 = lc.FStar_Syntax_Syntax.comp () in
+      let uu____1783 = FStar_Syntax_Syntax.lcomp_comp lc in
       comp_to_string uu____1783
     else
       (let uu____1785 = sli lc.FStar_Syntax_Syntax.eff_name in
@@ -915,6 +915,8 @@ and cflags_to_string: FStar_Syntax_Syntax.cflags -> Prims.string =
     | FStar_Syntax_Syntax.RETURN  -> "return"
     | FStar_Syntax_Syntax.PARTIAL_RETURN  -> "partial_return"
     | FStar_Syntax_Syntax.SOMETRIVIAL  -> "sometrivial"
+    | FStar_Syntax_Syntax.TRIVIAL_POSTCONDITION  -> "trivial_postcondition"
+    | FStar_Syntax_Syntax.SHOULD_NOT_INLINE  -> "should_not_inline"
     | FStar_Syntax_Syntax.LEMMA  -> "lemma"
     | FStar_Syntax_Syntax.CPS  -> "cps"
     | FStar_Syntax_Syntax.DECREASES uu____2015 -> ""

diff --git a/src/ocaml-output/FStar_Syntax_Resugar.ml b/src/ocaml-output/FStar_Syntax_Resugar.ml
diff --git a/src/ocaml-output/FStar_Syntax_Subst.ml b/src/ocaml-output/FStar_Syntax_Subst.ml
diff --git a/src/ocaml-output/FStar_Syntax_Syntax.ml b/src/ocaml-output/FStar_Syntax_Syntax.ml