From 7dce6eaffaa4169fab822d833e32b593ad867588 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 May 2022 15:53:52 +0200
Subject: Update the extraction to set the fuel to 1 in the Z3 options

---
 tests/hashmap/Hashmap.Clauses.Template.fst | 2 +-
 tests/hashmap/Hashmap.Funs.fst             | 2 +-
 tests/hashmap/Hashmap.Types.fst            | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tests/hashmap')

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) =
-- 
cgit v1.2.3