From 49729af01472ddcb39cd052d3b5d6ea5f0a9d9c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 7 Feb 2025 13:41:14 -0800
Subject: [PATCH 1/3] Parser.AST: exposing decl_to_string

---
 src/parser/FStarC.Parser.AST.fsti | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/parser/FStarC.Parser.AST.fsti b/src/parser/FStarC.Parser.AST.fsti
index 6b9083771a5..7dc12ba2178 100644
--- a/src/parser/FStarC.Parser.AST.fsti
+++ b/src/parser/FStarC.Parser.AST.fsti
@@ -354,6 +354,7 @@ val string_of_pragma : pragma -> string
 val pat_to_string : pattern -> string
 val binder_to_string : binder -> string
 val modul_to_string : modul -> string
+val decl_to_string : decl -> string
 
 val decl_is_val : ident -> decl -> bool
 

From 99c8e19577606c9ab2da0fed83e2feada497bed3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 7 Feb 2025 13:41:30 -0800
Subject: [PATCH 2/3] Parser: nits

---
 src/parser/FStarC.Parser.Const.Tuples.fst | 45 ++++++++++++-----------
 1 file changed, 23 insertions(+), 22 deletions(-)

diff --git a/src/parser/FStarC.Parser.Const.Tuples.fst b/src/parser/FStarC.Parser.Const.Tuples.fst
index de1ec8e8a82..c6621186391 100644
--- a/src/parser/FStarC.Parser.Const.Tuples.fst
+++ b/src/parser/FStarC.Parser.Const.Tuples.fst
@@ -19,6 +19,7 @@ open FStarC
 open FStarC.Effect
 open FStarC.Ident
 open FStarC.Range
+open FStarC.Class.Show
 
 // Arity, type constructor, and data constructor for tuples
 private
@@ -38,21 +39,21 @@ let tuple_table : list (int & string & string) = [
   (14,  "FStar.Pervasives.Native.tuple14", "FStar.Pervasives.Native.Mktuple14");
 ]
 
-let mk_tuple_lid n r =
+let lookup_tuple n =
   match List.tryFind (fun (n', _, _) -> n = n') tuple_table with
-  | Some (_, s, _) ->
-    let l = Ident.lid_of_str s in
-    set_lid_range l r
+  | Some r -> r
   | None ->
-    failwith "Tuple too large"
+    failwith ("Tuple too large: " ^ (show n))
+
+let mk_tuple_lid n r =
+  let (_, s, _) = lookup_tuple n in
+  let l = Ident.lid_of_str s in
+  set_lid_range l r
 
 let mk_tuple_data_lid n r =
-  match List.tryFind (fun (n', _, _) -> n = n') tuple_table with
-  | Some (_, _, s) ->
-    let l = Ident.lid_of_str s in
-    set_lid_range l r
-  | None ->
-    failwith "Tuple too large"
+  let (_, _, s) = lookup_tuple n in
+  let l = Ident.lid_of_str s in
+  set_lid_range l r
 
 let get_tuple_datacon_arity (s:string) : option int =
   match List.tryFind (fun (_, _, s') -> s = s') tuple_table with
@@ -84,21 +85,21 @@ let dtuple_table : list (int & string & string) = [
   (5, "FStar.Pervasives.dtuple5", "FStar.Pervasives.Mkdtuple5");
 ]
 
-let mk_dtuple_lid n r =
+let lookup_dtuple n =
   match List.tryFind (fun (n', _, _) -> n = n') dtuple_table with
-  | Some (_, s, _) ->
-    let l = Ident.lid_of_str s in
-    set_lid_range l r
+  | Some r -> r
   | None ->
-    failwith "Dependent Tuple too large"
+    failwith ("DTuple too large: " ^ (show n))
+
+let mk_dtuple_lid n r =
+  let (_, s, _) = lookup_dtuple n in
+  let l = Ident.lid_of_str s in
+  set_lid_range l r
 
 let mk_dtuple_data_lid n r =
-  match List.tryFind (fun (n', _, _) -> n = n') dtuple_table with
-  | Some (_, _, s) ->
-    let l = Ident.lid_of_str s in
-    set_lid_range l r
-  | None ->
-    failwith "Dependent Tuple too large"
+  let (_, _, s) = lookup_dtuple n in
+  let l = Ident.lid_of_str s in
+  set_lid_range l r
 
 let get_dtuple_datacon_arity (s:string) : option int =
   match List.tryFind (fun (_, _, s') -> s = s') dtuple_table with

From 195827e35f86672d4b241b977e2fd2c2446c8784 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 7 Feb 2025 14:46:59 -0800
Subject: [PATCH 3/3] ModifiesGen: work around a Z3 crash (in 4.13.3, works
 fine in Z3 master)

---
 ulib/FStar.ModifiesGen.fst | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/ulib/FStar.ModifiesGen.fst b/ulib/FStar.ModifiesGen.fst
index 45a49be66ae..6f4f459bb53 100644
--- a/ulib/FStar.ModifiesGen.fst
+++ b/ulib/FStar.ModifiesGen.fst
@@ -1504,11 +1504,12 @@ let loc_addresses_unused_in #al c r a h = ()
 let loc_addresses_not_unused_in #al c r a h = ()
 #pop-options
 
-#push-options "--z3rlimit 50"
+// Using spinoff and z3refresh to avoid a crash in Z3 4.13.3
+#push-options "--z3rlimit 50 --z3refresh"
 let loc_unused_in_not_unused_in_disjoint #al c h =
-  assert (Ghost.reveal (Loc?.aux (loc_unused_in c h)) `loc_aux_disjoint` Ghost.reveal (Loc?.aux (loc_not_unused_in c h)));
-  assert_spinoff (loc_disjoint #al #c (loc_unused_in #al c h)
-                                      (loc_not_unused_in #al c h))
+  assert_spinoff (Ghost.reveal (Loc?.aux (loc_unused_in c h)) `loc_aux_disjoint` Ghost.reveal (Loc?.aux (loc_not_unused_in c h)));
+  assert_spinoff (loc_disjoint #al #c (loc_unused_in #al c h) (loc_not_unused_in #al c h));
+  ()
 #pop-options
 
 #push-options "--z3cliopt 'smt.qi.eager_threshold=100'"