[K-Bug] Incorrect `#Exists` instantiation

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v5.5.19-0-gb0c703a959

Operating System

MacOS (Apple Silicon/AMD)

K Definitions (If Possible)

exists-issue.k

module EXISTS-ISSUE-SYNTAX
  imports INT-SYNTAX

  syntax Int ::= F1(Int) [function, no-evaluators]
  syntax Int ::= F2(Int) [function, no-evaluators]

  syntax Int ::= FX(Int) [function]
endmodule

module EXISTS-ISSUE
     imports BOOL
     imports INT
     imports EXISTS-ISSUE-SYNTAX

     rule FX(I) => F1(I) +Int F2(I +Int 2)

     rule #Ceil(F1(I:Int))  => #Exists X:Int. { I #Equals 2 *Int X } [simplification]
     rule #Ceil(F2(I:Int))  => #Exists X:Int. { I #Equals 2 *Int X } [simplification]

     rule #Ceil(FX(I)) => #Ceil(F1(I)) #And #Ceil(F2(I)) [simplification]
endmodule

exists-example.k

requires "exists-issue.k"
requires "domains.md"

module EXISTS-EXAMPLE-SYNTAX
    imports EXISTS-ISSUE-SYNTAX

endmodule

module VERIFICATION
  imports EXISTS-EXAMPLE-SYNTAX
  imports EXISTS-ISSUE
endmodule

module EXISTS-EXAMPLE
  imports VERIFICATION

  claim
    <k>
      FX(I:Int) => I ...
    </k>
endmodule

Steps to Reproduce

kompile exists-issue.k --backend haskell
kprove exists-example.k

The claim is (wrongly) vacuously proven:

Claim proven during initialization: [REDACTED]/exists-example.k:18:5-20:9
    The left-hand side of the claim may be undefined.
#Top

because (I believe) the existentially quantified X is considered to be the same X when instantiated, instead of having two separate Xs, say X0 and X1. If one renames X in any of the #Ceil simplifications, one gets the expected result.

Expected Results

A failing proof, as the claim does not hold.

Start by running kompile exists-issue.k --backend haskell and kprove exists-example.k using the definitions included in the issue. Compare this with the renamed-variable variant, then trace existential instantiation in the Haskell backend. Done means the supplied claim is no longer vacuously proven and instead fails as expected.