Method only verifies with --useOldAxiomatization
Opened this issue · 0 comments
superaxander commented
The following method only seems to verify if I use --useOldAxiomatization
:
method lemmaUniquenessPrefix(s1: Seq[Bool], s2: Seq[Bool],
prefix: Seq[Bool])
ensures (s1 == s2) == (prefix ++ s1 == prefix ++ s2)
{
var s3: Seq[Bool]
var s4: Seq[Bool]
if (|s1| == |s2|) {
s3 := prefix ++ s1
s4 := prefix ++ s2
inhale (forall y: Int ::
{ s1[y] }
0 <= y && y < |s1| ==>
(s1[y] == s2[y]) == (s3[|prefix| + y] == s4[|prefix| + y]))
}
}