Initial set of files.

30 files changed, 545 insertions, 0 deletions

diff --git a/Binaries/..svnbridge/FSharp.Core.dll b/Binaries/..svnbridge/FSharp.Core.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/FSharp.Core.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/FSharp.PowerPack.dll b/Binaries/..svnbridge/FSharp.PowerPack.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/FSharp.PowerPack.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/Microsoft.SpecSharp.pdb b/Binaries/..svnbridge/Microsoft.SpecSharp.pdb
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/Microsoft.SpecSharp.pdb
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/Mscorlib.Contracts.dll b/Binaries/..svnbridge/Mscorlib.Contracts.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/Mscorlib.Contracts.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/System.Compiler.Contracts.dll b/Binaries/..svnbridge/System.Compiler.Contracts.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/System.Compiler.Contracts.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/System.Compiler.Framework.Contracts.dll b/Binaries/..svnbridge/System.Compiler.Framework.Contracts.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/System.Compiler.Framework.Contracts.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/System.Compiler.Framework.dll b/Binaries/..svnbridge/System.Compiler.Framework.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/System.Compiler.Framework.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/System.Compiler.Framework.pdb b/Binaries/..svnbridge/System.Compiler.Framework.pdb
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/System.Compiler.Framework.pdb
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/System.Compiler.dll b/Binaries/..svnbridge/System.Compiler.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/System.Compiler.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/System.Compiler.pdb b/Binaries/..svnbridge/System.Compiler.pdb
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/System.Compiler.pdb
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/System.Contracts.dll b/Binaries/..svnbridge/System.Contracts.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/System.Contracts.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/System.Xml.Contracts.dll b/Binaries/..svnbridge/System.Xml.Contracts.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/System.Xml.Contracts.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/..svnbridge/microsoft.specsharp.dll b/Binaries/..svnbridge/microsoft.specsharp.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/microsoft.specsharp.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
new file mode 100644
index 00000000..7ff940b5
--- /dev/null
+++ b/Binaries/DafnyPrelude.bpl
@@ -0,0 +1,185 @@
+// Dafny prelude

+// Created 9 February 2008 by Rustan Leino.

+// Converted to Boogie 2 on 28 June 2008.

+// Copyright (c) 2008, Microsoft.

+

+type ref;

+const null: ref;

+

+// ---------------------------------------------------------------

+// -- Axiomatization of sets -------------------------------------

+// ---------------------------------------------------------------

+

+type Set T = [T]bool;

+

+function Set#Empty<T>() returns (Set T);

+axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);

+

+function Set#Singleton<T>(T) returns (Set T);

+axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);

+axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);

+

+function Set#UnionOne<T>(Set T, T) returns (Set T);

+axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }

+  Set#UnionOne(a,x)[o] <==> o == x || a[o]);

+

+function Set#Union<T>(Set T, Set T) returns (Set T);

+axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }

+  Set#Union(a,b)[o] <==> a[o] || b[o]);

+

+function Set#Intersection<T>(Set T, Set T) returns (Set T);

+axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }

+  Set#Intersection(a,b)[o] <==> a[o] && b[o]);

+

+function Set#Difference<T>(Set T, Set T) returns (Set T);

+axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }

+  Set#Difference(a,b)[o] <==> a[o] && !b[o]);

+

+function Set#Subset<T>(Set T, Set T) returns (bool);

+axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }

+  Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));

+

+function Set#Equal<T>(Set T, Set T) returns (bool);

+axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }

+  Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o]));

+axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }  // extensionality axiom for sets

+  Set#Equal(a,b) ==> a == b);

+

+function Set#Disjoint<T>(Set T, Set T) returns (bool);

+axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }

+  Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));

+

+// ---------------------------------------------------------------

+// -- Axiomatization of sequences --------------------------------

+// ---------------------------------------------------------------

+

+type Seq T;

+

+function Seq#Length<T>(Seq T) returns (int);

+axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));

+

+function Seq#Empty<T>() returns (Seq T);

+axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);

+axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());

+

+function Seq#Singleton<T>(T) returns (Seq T);

+axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);

+

+function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);

+axiom (forall<T> s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) }

+  Seq#Length(Seq#Build(s,i,v,len)) == len);

+

+function Seq#Append<T>(Seq T, Seq T) returns (Seq T);

+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }

+  Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));

+

+function Seq#Index<T>(Seq T, int) returns (T);

+axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);

+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }

+  (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&

+  (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0))));

+axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Build(s,i,v,len),n) }

+  (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&

+  (i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));

+

+function Seq#Contains<T>(Seq T, T) returns (bool);

+axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }

+  Seq#Contains(s,x) <==>

+    (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));

+axiom (forall x: ref ::

+  { Seq#Contains(Seq#Empty(), x) }

+  !Seq#Contains(Seq#Empty(), x));

+axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::

+  { Seq#Contains(Seq#Append(s0, s1), x) }

+  Seq#Contains(Seq#Append(s0, s1), x) <==>

+    Seq#Contains(s0, x) || Seq#Contains(s1, x));

+axiom (forall<T> s: Seq T, i: int, v: T, len: int, x: T ::

+  { Seq#Contains(Seq#Build(s, i, v, len), x) }

+  Seq#Contains(Seq#Build(s, i, v, len), x) <==>

+    x == v || Seq#Contains(s, x));

+axiom (forall<T> s: Seq T, n: int, x: T ::

+  { Seq#Contains(Seq#Take(s, n), x) }

+  Seq#Contains(Seq#Take(s, n), x) <==>

+    (exists i: int :: { Seq#Index(s, i) }

+      0 <= i && i < n && n <= Seq#Length(s) && Seq#Index(s, i) == x));

+axiom (forall<T> s: Seq T, n: int, x: T ::

+  { Seq#Contains(Seq#Drop(s, n), x) }

+  Seq#Contains(Seq#Drop(s, n), x) <==>

+    (exists i: int :: { Seq#Index(s, i) }

+      0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));

+

+function Seq#Equal<T>(Seq T, Seq T) returns (bool);

+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }

+  Seq#Equal(s0,s1) <==>

+    Seq#Length(s0) == Seq#Length(s1) &&

+    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }

+        0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));

+axiom(forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) }  // extensionality axiom for sequences

+  Seq#Equal(a,b) ==> a == b);

+

+function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);

+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }

+  Seq#SameUntil(s0,s1,n) <==>

+    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }

+        0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));

+

+function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);

+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }

+  0 <= n ==>

+    (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&

+    (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));

+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) }

+  0 <= j && j < n && j < Seq#Length(s) ==>

+    Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));

+

+function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);

+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }

+  0 <= n ==>

+    (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&

+    (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));

+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }

+  0 <= n && 0 <= j && j < Seq#Length(s)-n ==>

+    Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));

+

+// ---------------------------------------------------------------

+// -- Boxing and unboxing ----------------------------------------

+// ---------------------------------------------------------------

+

+function $Box<T>(T) returns (ref);

+function $Unbox<T>(ref) returns (T);

+

+axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

+

+// ---------------------------------------------------------------

+

+type ClassName;

+const unique class.int: ClassName;

+const unique class.bool: ClassName;

+const unique class.object: ClassName;

+const unique class.set: ClassName;

+const unique class.seq: ClassName;

+

+function dtype(ref) returns (ClassName);

+function TypeParams(ref, int) returns (ClassName);

+

+function TypeTuple(a: ClassName, b: ClassName) returns (ClassName);

+function TypeTupleCar(ClassName) returns (ClassName);

+function TypeTupleCdr(ClassName) returns (ClassName);

+// TypeTuple is injective in both arguments:

+axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }

+  TypeTupleCar(TypeTuple(a,b)) == a &&

+  TypeTupleCdr(TypeTuple(a,b)) == b);

+

+// ---------------------------------------------------------------

+

+type Field alpha;

+type HeapType = <alpha>[ref,Field alpha]alpha;

+

+function $IsGoodHeap(HeapType) returns (bool);

+var $Heap: HeapType where $IsGoodHeap($Heap);

+

+const unique alloc: Field bool;

+

+function $HeapSucc(HeapType, HeapType) returns (bool);

+axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }

+  $HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));

diff --git a/Binaries/FSharp.Core.dll b/Binaries/FSharp.Core.dll
new file mode 100644
index 00000000..56f1b6cd
--- /dev/null
+++ b/Binaries/FSharp.Core.dll
diff --git a/Binaries/FSharp.PowerPack.dll b/Binaries/FSharp.PowerPack.dll
new file mode 100644
index 00000000..7e0d3482
--- /dev/null
+++ b/Binaries/FSharp.PowerPack.dll
diff --git a/Binaries/Microsoft.SpecSharp.pdb b/Binaries/Microsoft.SpecSharp.pdb
new file mode 100644
index 00000000..9fa6f932
--- /dev/null
+++ b/Binaries/Microsoft.SpecSharp.pdb
diff --git a/Binaries/Mscorlib.Contracts.dll b/Binaries/Mscorlib.Contracts.dll
new file mode 100644
index 00000000..b0aeeb5f
--- /dev/null
+++ b/Binaries/Mscorlib.Contracts.dll
diff --git a/Binaries/System.Compiler.Contracts.dll b/Binaries/System.Compiler.Contracts.dll
new file mode 100644
index 00000000..6a573ef8
--- /dev/null
+++ b/Binaries/System.Compiler.Contracts.dll
diff --git a/Binaries/System.Compiler.Framework.Contracts.dll b/Binaries/System.Compiler.Framework.Contracts.dll
new file mode 100644
index 00000000..50726f3e
--- /dev/null
+++ b/Binaries/System.Compiler.Framework.Contracts.dll
diff --git a/Binaries/System.Compiler.Framework.dll b/Binaries/System.Compiler.Framework.dll
new file mode 100644
index 00000000..0c891dd0
--- /dev/null
+++ b/Binaries/System.Compiler.Framework.dll
diff --git a/Binaries/System.Compiler.Framework.pdb b/Binaries/System.Compiler.Framework.pdb
new file mode 100644
index 00000000..7e580bd1
--- /dev/null
+++ b/Binaries/System.Compiler.Framework.pdb
diff --git a/Binaries/System.Compiler.dll b/Binaries/System.Compiler.dll
new file mode 100644
index 00000000..645853a1
--- /dev/null
+++ b/Binaries/System.Compiler.dll
diff --git a/Binaries/System.Compiler.pdb b/Binaries/System.Compiler.pdb
new file mode 100644
index 00000000..328e2aa4
--- /dev/null
+++ b/Binaries/System.Compiler.pdb
diff --git a/Binaries/System.Contracts.dll b/Binaries/System.Contracts.dll
new file mode 100644
index 00000000..ed1ae103
--- /dev/null
+++ b/Binaries/System.Contracts.dll
diff --git a/Binaries/System.Xml.Contracts.dll b/Binaries/System.Xml.Contracts.dll
new file mode 100644
index 00000000..1ba5ec57
--- /dev/null
+++ b/Binaries/System.Xml.Contracts.dll
diff --git a/Binaries/TypedUnivBackPred2.sx b/Binaries/TypedUnivBackPred2.sx
new file mode 100644
index 00000000..5ee200f1
--- /dev/null
+++ b/Binaries/TypedUnivBackPred2.sx
@@ -0,0 +1,131 @@
+; -------------------------------------------------------------------------

+; Boogie 2 universal background predicate for Z3 (Simplify notation with types)

+; Copyright (c) 2004-2009, Microsoft Corp.

+

+(DEFTYPE $int :BUILTIN Int)

+(DEFTYPE $bool :BUILTIN bool)

+(DEFTYPE U)

+(DEFTYPE T)

+

+(DEFOP <: U U $bool)         ; used for translation with type premisses

+(DEFOP <:: T U U $bool)      ; used for translation with type arguments

+

+(BG_PUSH (AND

+

+  ; false is not true

+

+  (DISTINCT |@false| |@true|)

+

+  ; we assume type correctness of the operations here

+  ; a-l>=0 ==> (v ++ w:l)[a:b] = v[a-l:b-l]

+  (FORALL (v lv w lw lvw a b)

+    (QID bv:e:c1)

+    (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b))

+    (IMPLIES

+      (>= (- a lw) 0)

+      (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract v lv (- a lw) (- b lw)))))

+

+  ; b<=l ==> (v ++ w:l)[a:b] = w[a:b]

+  (FORALL (v lv w lw lvw a b)

+    (QID bv:e:c2)

+    (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b))

+    (IMPLIES

+      (<= b lw)

+      (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract w lw a b))))

+

+  ; v:l

+  ; a>=x || b<=y ==> (v[x:l] ++ w ++ v[0:y])[a:b] = v[a:b]

+  (FORALL (v lv x lxv w lw lwy y a b)

+    (QID bv:e:c3)

+    (PATS 

+      ($bv_extract 

+        ($bv_concat 

+          ($bv_extract v lv x lv) lxv

+	  ($bv_concat 

+	    w lw

+            ($bv_extract v lv 0 y) y) lwy) lv a b))

+    (IMPLIES

+      (AND

+        (EQ lw (- x y))

+        (EQ lxv (- lv x))

+        (EQ lwy (+ w y))

+        (OR (>= a x) (<= b y)))

+      (EQ

+        ($bv_extract 

+          ($bv_concat 

+            ($bv_extract v lv x lv) lxv

+	    ($bv_concat 

+	      w lw

+              ($bv_extract v lv 0 y) y) lwy) lv a b)

+	($bv_extract v lv a b))))

+

+  ; a>=x ==> (v[x:l] ++ w)[a:b] = v[a:b]

+  (FORALL (v lv x lxv w a b)

+    (QID bv:e:c4)

+    (PATS 

+      ($bv_extract 

+        ($bv_concat 

+          ($bv_extract v lv x lv) lxv 

+	  w x) 

+	lv a b))

+    (IMPLIES

+      (AND

+        (EQ lxv (- lv x))

+        (>= a x))

+      (EQ

+        ($bv_extract 

+          ($bv_concat 

+            ($bv_extract v lv x lv) lxv 

+	    w x) 

+	  lv a b)

+	($bv_extract v lv a b))))

+

+  (FORALL (v l)

+    (QID bv:e:0)

+    (PATS ($bv_extract v l 0 l))

+      (EQ ($bv_extract v l 0 l) v))

+

+  (FORALL (n)

+    (QID bv:pow)

+    (PATS ($pow2 n))

+      (IMPLIES (> n 0) (EQ ($pow2 n) (* 2 ($pow2 (- n 1))))))

+

+  (EQ ($pow2 0) 1)

+

+  ; 0 <= v < 2^Y ==> 0bvX ++ v[0:Y] == v

+  (FORALL (v l a b)

+    (QID bv:e:pow)

+    (PATS ($bv_concat 0 b ($bv_extract v l 0 a) a))

+    (IMPLIES

+      (AND

+        (<= 0 v)

+        (< v ($pow2 a))

+        (EQ l (+ a b)))

+      (EQ ($bv_concat 0 b ($bv_extract v l 0 a) a) v)))

+  

+  ; X > 0 ==> 0bvX ++ v >= 0

+  (FORALL (v a b)

+    (QID bv:e:pos)

+    (PATS ($bv_concat 0 b v a))

+    (IMPLIES

+      (> b 0)

+      (>= ($bv_concat 0 b v a) 0)))

+

+  ;; unsound?

+;  (FORALL (lv w lw)

+;    (QID bv:c:0)

+;    (PATS ($bv_concat 0 lv w lw))

+;    (EQ ($bv_concat 0 lv w lw) w))

+  ;; matching loop

+;  (FORALL (v l1 a b l2 c d)

+;    (QID bv:e:e)

+;    (PATS ($bv_extract ($bv_extract v l1 a b) l2 c d))

+;    (EQ ($bv_extract ($bv_extract v l1 a b) l2 c d) ($bv_extract v l1 (+ c a) (+ d a))))

+  

+

+  ; Reflect plus

+  (FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))

+

+))  ;; AND, BG_PUSH

+; End Boogie universal background predicate

+; -------------------------------------------------------------------------

diff --git a/Binaries/UnivBackPred2.smt b/Binaries/UnivBackPred2.smt
new file mode 100644
index 00000000..76c77d60
--- /dev/null
+++ b/Binaries/UnivBackPred2.smt
@@ -0,0 +1,131 @@
+; -------------------------------------------------------------------------

+; Boogie universal background predicate

+; Copyright (c) 2004-2006, Microsoft Corp.

+  :logic AUFLIA

+  :category { industrial }

+

+:extrasorts ( boogieU )

+:extrasorts ( boogieT )

+:extrasorts ( TermBool )

+

+:extrafuns (( boolTrue TermBool ))

+:extrafuns (( boolFalse TermBool ))

+:extrafuns (( boolIff TermBool TermBool TermBool ))

+:extrafuns (( boolImplies TermBool TermBool TermBool ))

+:extrafuns (( boolAnd TermBool TermBool TermBool ))

+:extrafuns (( boolOr TermBool TermBool TermBool ))

+:extrafuns (( boolNot TermBool TermBool ))

+:extrafuns (( UEqual boogieU boogieU TermBool ))

+:extrafuns (( TEqual boogieT boogieT TermBool ))

+:extrafuns (( IntEqual Int Int TermBool ))

+:extrafuns (( intLess Int Int TermBool ))

+:extrafuns (( intAtMost Int Int TermBool ))

+:extrafuns (( intGreater Int Int TermBool ))

+:extrafuns (( intAtLeast Int Int TermBool ))

+:extrafuns (( boogieIntMod Int Int Int ))

+:extrafuns (( boogieIntDiv Int Int Int ))

+

+; used for translation with type premisses

+:extrapreds (( UOrdering2 boogieU boogieU ))

+; used for translation with type arguments

+:extrapreds (( UOrdering3 boogieT boogieU boogieU ))

+

+; used for translation with type premisses

+:extrafuns (( TermUOrdering2 boogieU boogieU TermBool ))

+; used for translation with type arguments

+:extrafuns (( TermUOrdering3 boogieT boogieU boogieU TermBool ))

+

+  ; formula/term axioms

+  :assumption

+  (forall (?x TermBool) (?y TermBool)

+    (iff

+      (= (boolIff ?x ?y) boolTrue)

+      (iff (= ?x boolTrue) (= ?y boolTrue))))

+

+  :assumption

+  (forall (?x TermBool) (?y TermBool)

+    (iff

+      (= (boolImplies ?x ?y) boolTrue)

+      (implies (= ?x boolTrue) (= ?y boolTrue))))

+

+  :assumption

+  (forall (?x TermBool) (?y TermBool)

+    (iff

+      (= (boolAnd ?x ?y) boolTrue)

+      (and (= ?x boolTrue) (= ?y boolTrue))))

+

+  :assumption

+  (forall (?x TermBool) (?y TermBool)

+    (iff

+      (= (boolOr ?x ?y) boolTrue)

+      (or (= ?x boolTrue) (= ?y boolTrue))))

+

+  :assumption

+  (forall (?x TermBool)

+    (iff

+      (= (boolNot ?x) boolTrue)

+      (not (= ?x boolTrue)))

+    :pat { (boolNot ?x) }

+  )

+

+  :assumption

+  (forall (?x boogieU) (?y boogieU)

+    (iff

+      (= (UEqual ?x ?y) boolTrue)

+      (= ?x ?y)))

+

+  :assumption

+  (forall (?x boogieT) (?y boogieT)

+    (iff

+      (= (TEqual ?x ?y) boolTrue)

+      (= ?x ?y)))

+

+  :assumption

+  (forall (?x Int) (?y Int)

+    (iff

+      (= (IntEqual ?x ?y) boolTrue)

+      (= ?x ?y)))

+

+  :assumption

+  (forall (?x Int) (?y Int)

+    (iff

+      (= (intLess ?x ?y) boolTrue)

+      (< ?x ?y)))

+

+  :assumption

+  (forall (?x Int) (?y Int)

+    (iff

+      (= (intAtMost ?x ?y) boolTrue)

+      (<= ?x ?y)))

+

+  :assumption

+  (forall (?x Int) (?y Int)

+    (iff

+      (= (intAtLeast ?x ?y) boolTrue)

+      (>= ?x ?y)))

+

+  :assumption

+  (forall (?x Int) (?y Int)

+    (iff

+      (= (intGreater ?x ?y) boolTrue)

+      (> ?x ?y)))

+

+  ; false is not true

+  :assumption

+  (distinct boolFalse boolTrue)

+

+  :assumption

+  (forall (?x boogieU) (?y boogieU)

+    (iff

+      (= (TermUOrdering2 ?x ?y) boolTrue)

+      (UOrdering2 ?x ?y)))

+

+  :assumption

+  (forall (?x boogieT) (?y boogieU) (?z boogieU)

+    (iff

+      (= (TermUOrdering3 ?x ?y ?z) boolTrue)

+      (UOrdering3 ?x ?y ?z)))

+

+; End Boogie universal background predicate

+; -------------------------------------------------------------------------

+

diff --git a/Binaries/UnivBackPred2.sx b/Binaries/UnivBackPred2.sx
new file mode 100644
index 00000000..7c3dac8e
--- /dev/null
+++ b/Binaries/UnivBackPred2.sx
@@ -0,0 +1,85 @@
+; -------------------------------------------------------------------------

+; Boogie 2 universal background predicate

+; Copyright (c) 2004-2008, Microsoft Corp.

+(DEFPRED (<: t u))          ; used for translation with type premisses

+(DEFPRED (<:: s t u))       ; used for translation with type arguments

+

+(BG_PUSH (AND

+

+  ; formula/term axioms

+

+  (FORALL (x y)

+    (IFF

+      (EQ (boolIff x y) |@true|)

+      (IFF (EQ x |@true|) (EQ y |@true|))))

+

+  (FORALL (x y)

+    (IFF

+      (EQ (boolImplies x y) |@true|)

+      (IMPLIES (EQ x |@true|) (EQ y |@true|))))

+

+  (FORALL (x y)

+    (IFF

+      (EQ (boolAnd x y) |@true|)

+      (AND (EQ x |@true|) (EQ y |@true|))))

+

+  (FORALL (x y)

+    (IFF

+      (EQ (boolOr x y) |@true|)

+      (OR (EQ x |@true|) (EQ y |@true|))))

+

+  (FORALL (x)

+    (PATS (boolNot x))

+    (IFF

+      (EQ (boolNot x) |@true|)

+      (NEQ x |@true|)))

+

+  (FORALL (x y)

+    (IFF

+      (EQ (anyEqual x y) |@true|)

+      (EQ x y)))

+

+  (FORALL (x y)

+    (PATS (anyNeq x y))

+    (IFF

+      (EQ (anyNeq x y) |@true|)

+      (NEQ x y)))

+

+  (FORALL (x y)

+    (IFF

+      (EQ (intLess x y) |@true|)

+      (< x y)))

+

+  (FORALL (x y)

+    (IFF

+      (EQ (intAtMost x y) |@true|)

+      (<= x y)))

+

+  (FORALL (x y)

+    (IFF

+      (EQ (intAtLeast x y) |@true|)

+      (>= x y)))

+

+  (FORALL (x y)

+    (IFF

+      (EQ (intGreater x y) |@true|)

+      (> x y)))

+

+  ; false is not true

+

+  (DISTINCT |@false| |@true|)

+

+  ;; The following axiom gives a way to typed produce verification conditions,

+  ;; that is, verification conditions where the terms are typable.  To use these,

+  ;; the VCExpressionGenerator.{CastTo,CastFrom} methods must be overridden.

+  ;; Look for USE_SORTED_LOGIC in VCGeneration/VCExpr.ssc.

+  ; (FORALL (val T U)

+  ;   (PATS (TypeConvert (TypeConvert val T U) U T))

+  ;   (EQ (TypeConvert (TypeConvert val T U) U T) val))

+

+  ; Reflect plus

+  (FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))

+

+))  ;; AND, BG_PUSH

+; End Boogie universal background predicate

+; -------------------------------------------------------------------------

diff --git a/Binaries/microsoft.specsharp.dll b/Binaries/microsoft.specsharp.dll
new file mode 100644
index 00000000..b63cc192
--- /dev/null
+++ b/Binaries/microsoft.specsharp.dll