summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-05-06 15:53:52 +0200
committerSon Ho2022-05-06 15:53:52 +0200
commit7dce6eaffaa4169fab822d833e32b593ad867588 (patch)
tree08d3f6fe9fcf5e601affc8377a53bdd92c2a98f8
parent38276f00f6aaebb70392775b97577c73a657005a (diff)
Update the extraction to set the fuel to 1 in the Z3 options
Diffstat (limited to '')
-rw-r--r--src/Translate.ml4
-rw-r--r--tests/betree/BetreeMain.Clauses.Template.fst2
-rw-r--r--tests/betree/BetreeMain.Opaque.fsti2
-rw-r--r--tests/betree/BetreeMain.Types.fsti2
-rw-r--r--tests/hashmap/Hashmap.Clauses.Template.fst2
-rw-r--r--tests/hashmap/Hashmap.Funs.fst2
-rw-r--r--tests/hashmap/Hashmap.Types.fst2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Opaque.fsti2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Types.fsti2
-rw-r--r--tests/misc/BetreeNll.fst2
-rw-r--r--tests/misc/External.Funs.fst2
-rw-r--r--tests/misc/External.Opaque.fsti2
-rw-r--r--tests/misc/External.Types.fsti2
-rw-r--r--tests/misc/NoNestedBorrows.fst2
-rw-r--r--tests/misc/Paper.fst2
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 =