Open
Description
This seems to decrease the performance significantly on certain proofs.
To reproduce:
tmp.k
module TMP
imports MAP
imports INT
syntax KItem ::= a(Map) | "b" | "c" | d(Map)
rule b => c
rule d(M:Map) => a(M)
syntax Int ::= count(Map) [function, functional]
rule count(.Map) => 0
rule count(K |-> _ M) => 1 +Int count(M) ensures notBool K in_keys(M)
[simplification]
endmodule
tmp-proof.k
module TMP-PROOF
imports TMP
claim a(_ |-> _ M:Map) => b requires count(M) >Int 5
[trusted]
claim a(_ |-> _ M:Map) => b requires count(M) >Int 3
[trusted]
claim a(M:Map) => b requires count(M) >Int 0
[trusted]
claim d(M:Map) => c requires count(M) >Int 0 andBool count(M) <Int 3
endmodule
command line:
kompile tmp.k --backend haskell && \
kprove tmp-proof.k --haskell-backend-command "kore-repl --smt-timeout 1000 --repl-script kast.kscript"repl:
stepf 5
select 3
konfig
Note that at step 1 -> 2 the REPL tried to apply 3 claims. For two of them, the SMT solver said that the condition is unsat, so the backend didn't try to take those branches. However, when applying the third, the Haskell backend kept the negated conditions from those branches (although they should always be true):
#Not ( #Exists _0 . #Exists _1 . #Exists M0 . {
M
#Equals
M0
_0 |-> _1
}
#And
{
false
#Equals
_0 in_keys ( M0 )
}
#And
{
true
#Equals
count ( M0 ) >Int 3
} )
#And
#Not ( #Exists _0 . #Exists _1 . #Exists M0 . {
M
#Equals
M0
_0 |-> _1
}
#And
{
false
#Equals
_0 in_keys ( M0 )
}
#And
{
true
#Equals
count ( M0 ) >Int 5
} )
#And
<k>
c ~> _DotVar1 ~> .
</k>
#And
{
true
#Equals
count ( M ) <Int 3
}
#And
{
true
#Equals
count ( M ) >Int 0
}