diff options
Diffstat (limited to 'tests/hashmap')
| -rw-r--r-- | tests/hashmap/Hashmap.Clauses.Template.fst | 2 | ||||
| -rw-r--r-- | tests/hashmap/Hashmap.Funs.fst | 2 | ||||
| -rw-r--r-- | tests/hashmap/Hashmap.Types.fst | 2 |
3 files changed, 3 insertions, 3 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) = |