Validity of simple existential pattern over map not proven #2875
Description
Z3 version 4.8.7 - 64 bit
K version: 5.1.226
Build date: Tue Oct 12 02:23:45 CEST 2021
kompile --backend haskell assign.k && kprove --def-module VERIFICATION spec.kassign.k
module ASSIGN-SYNTAX
imports INT-SYNTAX
imports ID-SYNTAX
syntax Stmt ::= Id "=" Int
endmodule
module ASSIGN
imports ASSIGN-SYNTAX
imports INT
imports MAP
configuration
<T>
<k>
$PGM:Stmt
</k>
<env>
.Map
</env>
</T>
rule <k> X:Id = V:Int => . ... </k>
<env> M => M [X <- V] </env>
endmodule
spec.k
requires "assign.k"
module SPEC-SYNTAX
imports ASSIGN-SYNTAX
syntax Id ::= "$x" [token]
endmodule
module VERIFICATION
imports SPEC-SYNTAX
imports ASSIGN
endmodule
module SPEC
imports VERIFICATION
claim <k> $x = A:Int => . ... </k>
<env> M => M [ $x <- ?B:Int ] </env>
ensures A <=Int ?B
endmodule
Expected output
#Top
Actual output
#Not ( #Exists ?B . {
M [ $x <- ?B:Int ]
#Equals
M [ $x <- A:Int ]
}
#And
{
true
#Equals
A <=Int ?B
} )
#And
<T>
<k>
_DotVar2
</k>
<env>
M [ $x <- A:Int ]
</env>
</T>
Note: The claim is proven if the property is strengthened to equality, i.e. with ensures A ==Int ?B.