Update the extraction to set the fuel to 1 in the Z3 options

7 files changed, 7 insertions, 7 deletions

diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst
index 257cf7a6..c1549e6b 100644
--- a/tests/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/hashmap/Hashmap.Clauses.Template.fst
@@ -4,7 +4,7 @@ module Hashmap.Clauses.Template
 open Primitives
 open Hashmap.Types
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
 unfold
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 4fb9c8e4..a97c52b9 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -5,7 +5,7 @@ open Primitives
 include Hashmap.Types
 include Hashmap.Clauses
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap::hash_key] *)
 let hash_key_fwd (k : usize) : result usize = Return k
diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/hashmap/Hashmap.Types.fst
index 22cdecff..91ee26c6 100644
--- a/tests/hashmap/Hashmap.Types.fst
+++ b/tests/hashmap/Hashmap.Types.fst
@@ -3,7 +3,7 @@
 module Hashmap.Types
 open Primitives
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap::List] *)
 type list_t (t : Type0) =
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index 6179e6b2..3c5ee819 100644
--- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -4,7 +4,7 @@ module HashmapMain.Clauses.Template
 open Primitives
 open HashmapMain.Types
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
 unfold
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index 4177f77d..160df880 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -6,7 +6,7 @@ include HashmapMain.Types
 include HashmapMain.Opaque
 include HashmapMain.Clauses
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap_main::hashmap::hash_key] *)
 let hashmap_hash_key_fwd (k : usize) : result usize = Return k
diff --git a/tests/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/hashmap_on_disk/HashmapMain.Opaque.fsti
index a8ec347f..6e54ea10 100644
--- a/tests/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ b/tests/hashmap_on_disk/HashmapMain.Opaque.fsti
@@ -4,7 +4,7 @@ module HashmapMain.Opaque
 open Primitives
 include HashmapMain.Types
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap_main::hashmap_utils::deserialize] *)
 val hashmap_utils_deserialize_fwd
diff --git a/tests/hashmap_on_disk/HashmapMain.Types.fsti b/tests/hashmap_on_disk/HashmapMain.Types.fsti
index b9798076..e289174b 100644
--- a/tests/hashmap_on_disk/HashmapMain.Types.fsti
+++ b/tests/hashmap_on_disk/HashmapMain.Types.fsti
@@ -3,7 +3,7 @@
 module HashmapMain.Types
 open Primitives
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap_main::hashmap::List] *)
 type hashmap_list_t (t : Type0) =