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/betree/BetreeMain.Clauses.Template.fst | 2 +-
 tests/betree/BetreeMain.Opaque.fsti          | 2 +-
 tests/betree/BetreeMain.Types.fsti           | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tests/betree')

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