MLCFG error when deconstructing a tuple which also is used in a {pre, post}condition

[sarsko]

This is a regression, meaning that the following pattern previously worked in CreuSAT, but now gives an MLCFG error.

The following code:

use creusot_contracts::*;

#[logic]
#[open(self)] // Opacity doesn't seem to matter
fn deconstruct(f2: (bool, Int)) {}

#[logic]
#[open(self)]
#[requires(just_true(f))] // can also be `ensures`
pub fn entry(
    f: (bool, Int)
) {
    deconstruct((f.0, f.1));
}

#[predicate]
#[open(self)]
fn just_true(f: (bool, Int)) -> bool {
    true
}

Gives:

File "../vt2024-rlib.mlcfg", line 17, characters 64-70: This term has type (int, int), but is expected to have type (bool, int)

Produced MLCFG:

module Vt2024_Entry_Impl
  use prelude.Int
  function deconstruct0 [#"../../../src/lib.rs" 5 0 5 31] (f2 : (bool, int)) : () =
    [#"../../../src/lib.rs" 3 0 3 8] ()
  val deconstruct0 [#"../../../src/lib.rs" 5 0 5 31] (f2 : (bool, int)) : ()
    ensures { result = deconstruct0 f2 }
    
  predicate just_true0 [#"../../../src/lib.rs" 18 0 18 36] (f : (bool, int)) =
    [#"../../../src/lib.rs" 19 4 19 8] true
  val just_true0 [#"../../../src/lib.rs" 18 0 18 36] (f : (bool, int)) : bool
    ensures { result = just_true0 f }
    
  constant f  : (bool, int)
  function entry [#"../../../src/lib.rs" 10 0 12 1] (f : (bool, int)) : ()
  goal vc_entry : ([#"../../../src/lib.rs" 9 11 9 23] just_true0 f)
   -> (let (a, _) = f in let (_, a) = f in let _ = deconstruct0 (a, a) in true)
end

Some notes:

1. Requires deconstructing both fields of the tuple.
2. Tuple type does not matter
3. Opacity does not seem to matter
4. The requires(just_true(f)) can also be an ensures.
5. Moving requires(just_true(f)) to be a just_true(f); call in the body does not run into issues.

[xldenis]

Ahhh this seems to be an issue with name hygiene in places, no?

[Lysxia]

The switch to coma seems to have fixed it. I just ran creusot and why3 on the example and it passed.