[Bug] kprove - rejects valid claim

[ttuegel]

K Version: v5.0.0-a507642

kprove rejects this claim:

// spec.k
module VERIFICATION
  import TEST
endmodule

module ISSUE-2138-SPEC
  import VERIFICATION

  claim
    <k> #assert i ( 1 , 0 ) ==Int 0 => . </k>
      requires true #And ( #Forall X. { i ( X, 0 ) #Equals 0 } )

endmodule

// test.k
module TEST
    imports BOOL
    imports INT

    syntax Exp ::= Int | Bool
                 | pair(Int, Int) [klabel(pair), symbol]

    syntax KItem ::= "#assume" Exp [klabel(assume), symbol]
    rule #assume true => .K
    rule #assume false => #Bottom

    syntax KItem ::= "#assert" Exp  [klabel(assert), symbol]
                   | "#fail"
    rule #assert true => .K
    rule #assert false => #fail

// Uninterpreted functions
    syntax Int ::= i(Int, Int)   [function, functional, no-evaluators, smtlib(fi), klabel(i)]
endmodule

with the following error:

[Error] Compiler: Found variable X on right hand side of rule, not bound on
left hand side. Did you mean "?X"?
    Source(/home/jenkins-slave/workspace/haskell-backend_PR-2317/test/issue-2138/././issue-2138-spec.k)
    Location(10,36,10,37)
[Error] Compiler: Had 1 structural errors.

This claim was accepted in version v5.0.0-5701be4.

Expected behavior: claim is accepted by the compiler.

[ehildenb]

this is because of https://github.com/kframework/k/issues/1472

[ttuegel]

You're probably right, but I don't think the check in #1472 should even be relevant because the variable isn't free in the rule, it's bound explicitly by #Forall.

[ehildenb]

Could be that the check also needs to be modified to take binders into account

[radumereuta]

Duplicate of: #1472