Bug: Could not compute value of ClauseBound

[R1kM]

The following code, minimized from the traits.rs test from Aeneas, yields to warnings.

pub trait ToU64 {
    fn to_u64(self) -> u64;
}

pub trait WithConstTy<const LEN: usize> {
    const LEN2: usize = 32;

    type W: ToU64;
}

Charon version: 7f8dbd5

Charon command: (the charon command line you ran)
charon/bin/charon rustc --preset=aeneas -- traits.rs --crate-name=traits --crate-type=rlib --allow=unused --allow=non_snake_case

Charon output:

warning: Could not compute the value of ClauseBound(0, 0)::W (Some(TraitRef(HashConsed(TraitRefContents { kind: Clause(Bound(DeBruijnId { index: 0 }, 0)), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { id: 1, generics: <@TypeBound(1, 0), @ConstGenericBound(1, 0)> } } })))) needed to update generics <@TypeBound(0, 0), @ConstGenericBound(0, 0)> for item traits::WithConstTy.
         Constraints in scope:

 --> tests/src/traits.rs:6:5
  |
9 |     const LEN2: usize = 32;
  |     ^^^^^^^^^^^^^^^^^^^^^^^

warning: Could not compute the value of ClauseBound(0, 0)::W (Some(TraitRef(HashConsed(TraitRefContents { kind: Clause(Bound(DeBruijnId { index: 0 }, 0)), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { id: 1, generics: <@TypeBound(1, 0), @ConstGenericBound(1, 0)> } } })))) needed to update generics <@TypeBound(0, 0), @ConstGenericBound(0, 0)> for item traits::WithConstTy.
         Constraints in scope:

 --> tests/src/traits.rs:6:5
  |
9 |     const LEN2: usize = 32;
  |     ^^^^^^^^^^^^^^^^^^^^^^^

warning: The extraction generated 2 warnings