diff options
Diffstat (limited to 'tests/misc')
| -rw-r--r-- | tests/misc/BetreeNll.fst | 2 | ||||
| -rw-r--r-- | tests/misc/External.Funs.fst | 2 | ||||
| -rw-r--r-- | tests/misc/External.Opaque.fsti | 2 | ||||
| -rw-r--r-- | tests/misc/External.Types.fsti | 2 | ||||
| -rw-r--r-- | tests/misc/NoNestedBorrows.fst | 2 | ||||
| -rw-r--r-- | tests/misc/Paper.fst | 2 |
6 files changed, 6 insertions, 6 deletions
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 = |