Jul 16, 2014 at 7:37 PM
Edited Jul 16, 2014 at 7:39 PM
I recently discovered that Boogie behaves in an inconsistent way when it comes to the extensionality of Maps (extensionality is considering two maps to be equal if they contain the same elements).
Consider the following program
assume (forall x:int :: a[x] == b[x]);
assert a == b;
If I ask Boogie to verify this program using its default flags it claims that assertion might be violated.
However if I use the
command line flag to Boogie it now considers this program correct.
According to the "This is Boogie 2" document Maps in Boogie don't have extensionality however we can see if we use the right flag with Boogie is does seem to think Maps have extensionality.
I believe the underlying issue is
- With the
/useArrayTheory flag. The Array theory is used to represent Maps in the SMTLIBv2 query and in this theory Arrays are considered to have the property of extensionality
- Without this flag maps are encoded as uninterpreted functions in the SMTLIBv2 like so...
(declare-sort |T@[Int]Int| 0)
(declare-fun |Select_[$int]$int| (|T@[Int]Int| Int) Int)
(declare-fun a () |T@[Int]Int|)
(declare-fun b () |T@[Int]Int|)
; The assume ends up in the assertions...
(forall ((x Int) ) (! (= (|Select_[$int]$int| a x) (|Select_[$int]$int| b x))
; Burried somewhere in the assertion is our assertion from the Boogie program
(= a b)
(= a b)
can evaluate to false seeing as it has not been defined what it means for these custom sorts (
) to be equal.
Is this behaviour intentional?