Does the behavior of add_tag!() and does_not_have_tag!() be affected by type and clone()?

[AiDaiP]

Issue

For S1, there is no warning at verify!(does_not_have_tag!(self, TraitTag)) in my_clone(). In f2(), clone() is deleted and a warning appears at verify!(does_not_have_tag!(self, TraitTag)). For S2, warnings appear for both my_clone() and f2(). Does the behavior of add_tag!() and does_not_have_tag!() be affected by type and clone()?

Steps to Reproduce

#![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]

#[macro_use]
extern crate mirai_annotations;

#[cfg(mirai)]
use mirai_annotations::{TagPropagation, TagPropagationSet};

#[cfg(mirai)]
struct TaintedKind<const MASK: TagPropagationSet> {}

#[cfg(mirai)]
const TAINTED_MASK: TagPropagationSet = tag_propagation_set!(TagPropagation::SubComponent);

#[cfg(mirai)]
type TraitTag = TaintedKind<TAINTED_MASK>;
#[cfg(not(mirai))]
type TraitTag = ();

pub struct S1(Box<str>);

impl S1 {
    pub fn my_clone(&self) -> Self {
        add_tag!(self, TraitTag);
        verify!(does_not_have_tag!(self, TraitTag));
        Self(self.0.clone())
    }

    pub fn f2(&self){
        add_tag!(self, TraitTag);
        verify!(does_not_have_tag!(self, TraitTag));
    }
}

pub struct S2(Box<u8>);

impl S2 {
    pub fn my_clone(&self) -> Self {
        add_tag!(self, TraitTag);
        verify!(does_not_have_tag!(self, TraitTag));
        Self(self.0.clone())
    }

    pub fn f2(&self){
        add_tag!(self, TraitTag);
        verify!(does_not_have_tag!(self, TraitTag));
    }
}

fn main() {
    println!("helloworld")
}

cargo mirai

Expected Behavior

warning: provably false verification condition warning appears at all does_not_have_tag!()

Actual Results

warning: provably false verification condition
  --> src/main.rs:31:9
   |
31 |         verify!(does_not_have_tag!(self, TraitTag));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: provably false verification condition
  --> src/main.rs:40:9
   |
40 |         verify!(does_not_have_tag!(self, TraitTag));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: provably false verification condition
  --> src/main.rs:46:9
   |
46 |         verify!(does_not_have_tag!(self, TraitTag));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: `helloworld` (bin "helloworld") generated 3 warnings
    Finished dev [unoptimized + debuginfo] target(s) in 13.39s

Environment

rustc 1.69.0-nightly (ef982929c 2023-01-27)

[hermanventer]

This looks like a bug.