diff --git a/.github/workflows/test_installs.yml b/.github/workflows/test_installs.yml
index f7dc327e9..9f5bc725f 100644
--- a/.github/workflows/test_installs.yml
+++ b/.github/workflows/test_installs.yml
@@ -22,7 +22,7 @@ jobs:
           - ubuntu-latest
           - ubuntu-20.04
           - macos-latest
-          - macos-12
+          - macos-13
     runs-on: ${{ matrix.os }}
     steps:
     - uses: actions/checkout@v3
diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs
index 35fe0fa76..f4c2ff72b 100644
--- a/hax-lib/macros/src/utils.rs
+++ b/hax-lib/macros/src/utils.rs
@@ -218,8 +218,6 @@ pub fn make_fn_decoration(
     mut generics: Option<Generics>,
     self_type: Option<Type>,
 ) -> (TokenStream, AttrPayload) {
-    let uid = ItemUid::fresh();
-    let mut_ref_inputs = unmut_references_in_inputs(&mut signature);
     let self_ident: Ident = syn::parse_quote! {self_};
     let error = {
         let mut rewriter = RewriteSelf::new(self_ident, self_type);
@@ -230,6 +228,8 @@ pub fn make_fn_decoration(
         }
         rewriter.get_error()
     };
+    let uid = ItemUid::fresh();
+    let mut_ref_inputs = unmut_references_in_inputs(&mut signature);
     let decoration = {
         let decoration_sig = {
             let mut sig = signature.clone();
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 03baa5eff..16d6a4594 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -114,6 +114,18 @@ unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
 
 unfold let add x y = x + y
 '''
+"Attributes.Issue_1266_.fst" = '''
+module Attributes.Issue_1266_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_T (v_Self: Type0) = {
+  f_v_pre:v_Self -> Type0;
+  f_v_post:x: v_Self -> x_future: v_Self -> pred: Type0{pred ==> true};
+  f_v:x0: v_Self -> Prims.Pure v_Self (f_v_pre x0) (fun result -> f_v_post x0 result)
+}
+'''
 "Attributes.Nested_refinement_elim.fst" = '''
 module Attributes.Nested_refinement_elim
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index 1a2c1f3b8..6a5d037af 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -320,7 +320,7 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
 
 [[package]]
 name = "hax-lib"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "hax-lib-macros",
  "num-bigint",
@@ -329,7 +329,7 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "hax-lib-macros-types",
  "paste",
@@ -341,7 +341,7 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros-types"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -352,14 +352,14 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-protocol"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "libcrux",
 ]
 
 [[package]]
 name = "hax-lib-protocol-macros"
-version = "0.1.0-rc.1"
+version = "0.1.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index c0deae940..eb520f6a7 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -381,3 +381,11 @@ mod requires_mut {
         }
     }
 }
+
+mod issue_1266 {
+    #[hax_lib::attributes]
+    trait T {
+        #[hax_lib::ensures(|_|true)]
+        fn v(x: &mut Self);
+    }
+}