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

17 files changed, 18 insertions, 18 deletions

diff --git a/src/Translate.ml b/src/Translate.ml
index 857f0f69..740670f9 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -573,8 +573,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports;
   (* Add the custom includes *)
   List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes;
-  (* Z3 options *)
-  Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 0 --ifuel 1\"\n";
+  (* Z3 options - note that we use fuel 1 because it its useful for the decrease clauses *)
+  Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 1 --ifuel 1\"\n";
 
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst
index e0279259..eb26276c 100644
--- a/tests/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/betree/BetreeMain.Clauses.Template.fst
@@ -4,7 +4,7 @@ module BetreeMain.Clauses.Template
 open Primitives
 open BetreeMain.Types
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [betree_main::betree::List::{1}::len]: decreases clause *)
 unfold
diff --git a/tests/betree/BetreeMain.Opaque.fsti b/tests/betree/BetreeMain.Opaque.fsti
index 7f0c04de..dc49601a 100644
--- a/tests/betree/BetreeMain.Opaque.fsti
+++ b/tests/betree/BetreeMain.Opaque.fsti
@@ -4,7 +4,7 @@ module BetreeMain.Opaque
 open Primitives
 include BetreeMain.Types
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [betree_main::betree_utils::load_internal_node] *)
 val betree_utils_load_internal_node_fwd
diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti
index 5edb4526..a937c726 100644
--- a/tests/betree/BetreeMain.Types.fsti
+++ b/tests/betree/BetreeMain.Types.fsti
@@ -3,7 +3,7 @@
 module BetreeMain.Types
 open Primitives
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [betree_main::betree::List] *)
 type betree_list_t (t : Type0) =
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) =
diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreeNll.fst
index 14c1d2ba..b548a18b 100644
--- a/tests/misc/BetreeNll.fst
+++ b/tests/misc/BetreeNll.fst
@@ -3,7 +3,7 @@
 module BetreeNll
 open Primitives
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [betree_nll::List] *)
 type list_t (t : Type0) =
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index c85ebf64..aafc0cf6 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -5,7 +5,7 @@ open Primitives
 include External.Types
 include External.Opaque
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [external::swap] *)
 let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
diff --git a/tests/misc/External.Opaque.fsti b/tests/misc/External.Opaque.fsti
index b8240cc3..7c241c7c 100644
--- a/tests/misc/External.Opaque.fsti
+++ b/tests/misc/External.Opaque.fsti
@@ -4,7 +4,7 @@ module External.Opaque
 open Primitives
 include External.Types
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::mem::swap] *)
 val core_mem_swap_fwd (t : Type0) : t -> t -> state -> result (state & unit)
diff --git a/tests/misc/External.Types.fsti b/tests/misc/External.Types.fsti
index b8adf9bb..4a13a744 100644
--- a/tests/misc/External.Types.fsti
+++ b/tests/misc/External.Types.fsti
@@ -3,7 +3,7 @@
 module External.Types
 open Primitives
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::num::nonzero::NonZeroU32] *)
 val core_num_nonzero_non_zero_u32_t : Type0
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 2a06fd76..ef4a9f82 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -3,7 +3,7 @@
 module NoNestedBorrows
 open Primitives
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [no_nested_borrows::Pair] *)
 type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index 205227be..d162519a 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -3,7 +3,7 @@
 module Paper
 open Primitives
 
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [paper::ref_incr] *)
 let ref_incr_fwd_back (x : i32) : result i32 =