Merge

59 files changed, 597 insertions, 4 deletions

diff --git a/Test/AbsHoudini/fail1.bpl b/Test/AbsHoudini/fail1.bpl
index abbd015b..5e15340c 100644
--- a/Test/AbsHoudini/fail1.bpl
+++ b/Test/AbsHoudini/fail1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x: bool) : bool;

 

 var myVar: int;

diff --git a/Test/AbsHoudini/fail1.bpl.expect b/Test/AbsHoudini/fail1.bpl.expect
new file mode 100644
index 00000000..e987f773
--- /dev/null
+++ b/Test/AbsHoudini/fail1.bpl.expect
@@ -0,0 +1,11 @@
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  false
+}
+fail1.bpl(16,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    fail1.bpl(11,3): anon0
+    fail1.bpl(12,11): anon4_Then
+    fail1.bpl(16,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl
index fc3d5713..0a8ebeb3 100644
--- a/Test/AbsHoudini/houd1.bpl
+++ b/Test/AbsHoudini/houd1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x: bool) : bool;

 

 var myVar: int;

diff --git a/Test/AbsHoudini/houd1.bpl.expect b/Test/AbsHoudini/houd1.bpl.expect
new file mode 100644
index 00000000..0b023466
--- /dev/null
+++ b/Test/AbsHoudini/houd1.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl
index bb0c65e7..6ee73b9a 100644
--- a/Test/AbsHoudini/houd10.bpl
+++ b/Test/AbsHoudini/houd10.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1():bool;

 function {:existential true} b2():bool;

 function {:existential true} b3():bool;

diff --git a/Test/AbsHoudini/houd10.bpl.expect b/Test/AbsHoudini/houd10.bpl.expect
new file mode 100644
index 00000000..d427a9f2
--- /dev/null
+++ b/Test/AbsHoudini/houd10.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  false
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl
index 78087744..dbde4f37 100644
--- a/Test/AbsHoudini/houd11.bpl
+++ b/Test/AbsHoudini/houd11.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert() : bool;

 

 var fooVar: int;

diff --git a/Test/AbsHoudini/houd11.bpl.expect b/Test/AbsHoudini/houd11.bpl.expect
new file mode 100644
index 00000000..13aff08c
--- /dev/null
+++ b/Test/AbsHoudini/houd11.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl
index b3a1a6db..ac46ef62 100644
--- a/Test/AbsHoudini/houd12.bpl
+++ b/Test/AbsHoudini/houd12.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 // Example to test candidate annotations on loops

 

 function {:existential true} Assert(): bool;

diff --git a/Test/AbsHoudini/houd12.bpl.expect b/Test/AbsHoudini/houd12.bpl.expect
new file mode 100644
index 00000000..aefaac93
--- /dev/null
+++ b/Test/AbsHoudini/houd12.bpl.expect
@@ -0,0 +1,34 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  false
+}
+function {:existential true} {:inline} b3() : bool
+{
+  false
+}
+function {:existential true} {:inline} b4() : bool
+{
+  false
+}
+function {:existential true} {:inline} b5() : bool
+{
+  false
+}
+function {:existential true} {:inline} b6() : bool
+{
+  true
+}
+function {:existential true} {:inline} b7() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl
index fd2611e2..c4d8e4e0 100644
--- a/Test/AbsHoudini/houd2.bpl
+++ b/Test/AbsHoudini/houd2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert(x:bool) : bool;

 function {:existential true} b1 (x:bool):bool;

 function {:existential true} b2 (x:bool):bool;

diff --git a/Test/AbsHoudini/houd2.bpl.expect b/Test/AbsHoudini/houd2.bpl.expect
new file mode 100644
index 00000000..6fe401ad
--- /dev/null
+++ b/Test/AbsHoudini/houd2.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} Assert(x: bool) : bool
+{
+  true
+}
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  true
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl
index 81f11018..a37b5874 100644
--- a/Test/AbsHoudini/houd3.bpl
+++ b/Test/AbsHoudini/houd3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert(x: bool) : bool;

 function {:existential true} b1(x: bool) : bool;

 function {:existential true} b2(x: bool) : bool;

diff --git a/Test/AbsHoudini/houd3.bpl.expect b/Test/AbsHoudini/houd3.bpl.expect
new file mode 100644
index 00000000..780edc91
--- /dev/null
+++ b/Test/AbsHoudini/houd3.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} Assert(x: bool) : bool
+{
+  x
+}
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  true
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl
index 01ee6707..2fc339d9 100644
--- a/Test/AbsHoudini/houd4.bpl
+++ b/Test/AbsHoudini/houd4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert() : bool;

 function {:existential true} b1():bool;

 function {:existential true} b2(x:bool):bool;

diff --git a/Test/AbsHoudini/houd4.bpl.expect b/Test/AbsHoudini/houd4.bpl.expect
new file mode 100644
index 00000000..a6756239
--- /dev/null
+++ b/Test/AbsHoudini/houd4.bpl.expect
@@ -0,0 +1,22 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+function {:existential true} {:inline} b1() : bool
+{
+  false
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+  false
+}
+function {:existential true} {:inline} b3(x: bool) : bool
+{
+  false
+}
+function {:existential true} {:inline} b4(x: bool) : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl
index afbaa81c..8a08b5cf 100644
--- a/Test/AbsHoudini/houd5.bpl
+++ b/Test/AbsHoudini/houd5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x:bool):bool;

 function {:existential true} b2(x:bool):bool;

 function {:existential true} b3(x:bool):bool;

diff --git a/Test/AbsHoudini/houd5.bpl.expect b/Test/AbsHoudini/houd5.bpl.expect
new file mode 100644
index 00000000..12144524
--- /dev/null
+++ b/Test/AbsHoudini/houd5.bpl.expect
@@ -0,0 +1,26 @@
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  !x
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+  x
+}
+function {:existential true} {:inline} b3(x: bool) : bool
+{
+  !x
+}
+function {:existential true} {:inline} b4(x: bool) : bool
+{
+  x
+}
+function {:existential true} {:inline} b5() : bool
+{
+  false
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl
index e4927901..209e2f01 100644
--- a/Test/AbsHoudini/houd6.bpl
+++ b/Test/AbsHoudini/houd6.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1():bool;

 function {:existential true} b2():bool;

 function {:existential true} b3():bool;

diff --git a/Test/AbsHoudini/houd6.bpl.expect b/Test/AbsHoudini/houd6.bpl.expect
new file mode 100644
index 00000000..f5c02d70
--- /dev/null
+++ b/Test/AbsHoudini/houd6.bpl.expect
@@ -0,0 +1,38 @@
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+function {:existential true} {:inline} b4() : bool
+{
+  true
+}
+function {:existential true} {:inline} b5() : bool
+{
+  true
+}
+function {:existential true} {:inline} b6() : bool
+{
+  true
+}
+function {:existential true} {:inline} b7() : bool
+{
+  true
+}
+function {:existential true} {:inline} b8() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl
index ef3293db..6df7b428 100644
--- a/Test/AbsHoudini/houd7.bpl
+++ b/Test/AbsHoudini/houd7.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1():bool;

 function {:existential true} b2():bool;

 function {:existential true} b3():bool;

diff --git a/Test/AbsHoudini/houd7.bpl.expect b/Test/AbsHoudini/houd7.bpl.expect
new file mode 100644
index 00000000..ce1675e4
--- /dev/null
+++ b/Test/AbsHoudini/houd7.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b1() : bool
+{
+  false
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl
index 8be7f3db..e5b88466 100644
--- a/Test/AbsHoudini/houd8.bpl
+++ b/Test/AbsHoudini/houd8.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1():bool;

 function {:existential true} b2():bool;

 function {:existential true} b3():bool;

diff --git a/Test/AbsHoudini/houd8.bpl.expect b/Test/AbsHoudini/houd8.bpl.expect
new file mode 100644
index 00000000..605ec988
--- /dev/null
+++ b/Test/AbsHoudini/houd8.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} b1() : bool
+{
+  false
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl
index fc37a15b..0c2d7f10 100644
--- a/Test/AbsHoudini/pred1.bpl
+++ b/Test/AbsHoudini/pred1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b0(x:bool, y:bool): bool;

 function {:existential true} b1(x:bool, y:bool): bool;

 function {:existential true} b2(x:bool, y:bool): bool;

diff --git a/Test/AbsHoudini/pred1.bpl.expect b/Test/AbsHoudini/pred1.bpl.expect
new file mode 100644
index 00000000..0e3d3333
--- /dev/null
+++ b/Test/AbsHoudini/pred1.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} b0(x: bool, y: bool) : bool
+{
+  x && !y
+}
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+  (y || x) && (!x || !y)
+}
+function {:existential true} {:inline} b2(x: bool, y: bool) : bool
+{
+  x && !y
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl
index 3ce948ce..9e93495f 100644
--- a/Test/AbsHoudini/pred2.bpl
+++ b/Test/AbsHoudini/pred2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b0(x:bool): bool;

 

 var g: int;

diff --git a/Test/AbsHoudini/pred2.bpl.expect b/Test/AbsHoudini/pred2.bpl.expect
new file mode 100644
index 00000000..55e46035
--- /dev/null
+++ b/Test/AbsHoudini/pred2.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} b0(x: bool) : bool
+{
+  x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl
index 450efde4..1cb36798 100644
--- a/Test/AbsHoudini/pred3.bpl
+++ b/Test/AbsHoudini/pred3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b0(x:bool, y:bool): bool;

 function {:existential true} b1(x:bool, y:bool): bool;

 function {:existential true} b2(x:bool, y:bool): bool;

diff --git a/Test/AbsHoudini/pred3.bpl.expect b/Test/AbsHoudini/pred3.bpl.expect
new file mode 100644
index 00000000..0e3d3333
--- /dev/null
+++ b/Test/AbsHoudini/pred3.bpl.expect
@@ -0,0 +1,14 @@
+function {:existential true} {:inline} b0(x: bool, y: bool) : bool
+{
+  x && !y
+}
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+  (y || x) && (!x || !y)
+}
+function {:existential true} {:inline} b2(x: bool, y: bool) : bool
+{
+  x && !y
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred4.bpl b/Test/AbsHoudini/pred4.bpl
index d4741720..9c814e3b 100644
--- a/Test/AbsHoudini/pred4.bpl
+++ b/Test/AbsHoudini/pred4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x:bool, y:bool): bool;

 function {:existential true} {:absdomain "Intervals"} b3(x:int): bool;

 

diff --git a/Test/AbsHoudini/pred4.bpl.expect b/Test/AbsHoudini/pred4.bpl.expect
new file mode 100644
index 00000000..ec1d9517
--- /dev/null
+++ b/Test/AbsHoudini/pred4.bpl.expect
@@ -0,0 +1,10 @@
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+  (y || x) && (!x || !y)
+}
+function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : bool
+{
+  x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl
index 6940e820..762a354f 100644
--- a/Test/AbsHoudini/pred5.bpl
+++ b/Test/AbsHoudini/pred5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} b1(x: bool) : bool;

 

 procedure main() 

diff --git a/Test/AbsHoudini/pred5.bpl.expect b/Test/AbsHoudini/pred5.bpl.expect
new file mode 100644
index 00000000..a5e1c73d
--- /dev/null
+++ b/Test/AbsHoudini/pred5.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl
index e12525b6..a5709736 100644
--- a/Test/AbsHoudini/quant1.bpl
+++ b/Test/AbsHoudini/quant1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool;

 

 procedure foo ()

diff --git a/Test/AbsHoudini/quant1.bpl.expect b/Test/AbsHoudini/quant1.bpl.expect
new file mode 100644
index 00000000..7d06cb21
--- /dev/null
+++ b/Test/AbsHoudini/quant1.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 2
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl
index 5a491877..2f291fca 100644
--- a/Test/AbsHoudini/quant2.bpl
+++ b/Test/AbsHoudini/quant2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

 

 procedure main() 

diff --git a/Test/AbsHoudini/quant2.bpl.expect b/Test/AbsHoudini/quant2.bpl.expect
new file mode 100644
index 00000000..0610db26
--- /dev/null
+++ b/Test/AbsHoudini/quant2.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 1
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl
index cc0ef79e..10fb72c7 100644
--- a/Test/AbsHoudini/quant3.bpl
+++ b/Test/AbsHoudini/quant3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

 

 procedure foo ()

diff --git a/Test/AbsHoudini/quant3.bpl.expect b/Test/AbsHoudini/quant3.bpl.expect
new file mode 100644
index 00000000..d43073ab
--- /dev/null
+++ b/Test/AbsHoudini/quant3.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl
index 55947f1f..99c37572 100644
--- a/Test/AbsHoudini/quant4.bpl
+++ b/Test/AbsHoudini/quant4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool;

 

 procedure foo ()

diff --git a/Test/AbsHoudini/quant4.bpl.expect b/Test/AbsHoudini/quant4.bpl.expect
new file mode 100644
index 00000000..07f98295
--- /dev/null
+++ b/Test/AbsHoudini/quant4.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl
index dfc44e47..83e6e68a 100644
--- a/Test/AbsHoudini/quant5.bpl
+++ b/Test/AbsHoudini/quant5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

 

 procedure foo ()

diff --git a/Test/AbsHoudini/quant5.bpl.expect b/Test/AbsHoudini/quant5.bpl.expect
new file mode 100644
index 00000000..b74f5abc
--- /dev/null
+++ b/Test/AbsHoudini/quant5.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 5 && x <= 5
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl
index 5884cf7b..ba18cf15 100644
--- a/Test/AbsHoudini/test1.bpl
+++ b/Test/AbsHoudini/test1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 var g: bool;

 

 procedure foo() 

diff --git a/Test/AbsHoudini/test1.bpl.expect b/Test/AbsHoudini/test1.bpl.expect
new file mode 100644
index 00000000..ecc2a8fd
--- /dev/null
+++ b/Test/AbsHoudini/test1.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b0() : bool
+{
+  false
+}
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl
index a30c3159..76a02e23 100644
--- a/Test/AbsHoudini/test10.bpl
+++ b/Test/AbsHoudini/test10.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 var sdv_7: int;

 var sdv_21: int;

 function {:existential true} b1(): bool;

diff --git a/Test/AbsHoudini/test10.bpl.expect b/Test/AbsHoudini/test10.bpl.expect
new file mode 100644
index 00000000..c9e99b13
--- /dev/null
+++ b/Test/AbsHoudini/test10.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b1() : bool
+{
+  false
+}
+function {:existential true} {:inline} b2() : bool
+{
+  false
+}
+function {:existential true} {:inline} b3() : bool
+{
+  false
+}
+function {:existential true} {:inline} b4() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl
index bfd78363..8c1717bf 100644
--- a/Test/AbsHoudini/test2.bpl
+++ b/Test/AbsHoudini/test2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 var g: int;

 var h: int;

 

diff --git a/Test/AbsHoudini/test2.bpl.expect b/Test/AbsHoudini/test2.bpl.expect
new file mode 100644
index 00000000..ecc2a8fd
--- /dev/null
+++ b/Test/AbsHoudini/test2.bpl.expect
@@ -0,0 +1,18 @@
+function {:existential true} {:inline} b0() : bool
+{
+  false
+}
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl
index bfe8a32d..d9500308 100644
--- a/Test/AbsHoudini/test7.bpl
+++ b/Test/AbsHoudini/test7.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert() : bool;

 

 var g: int;

diff --git a/Test/AbsHoudini/test7.bpl.expect b/Test/AbsHoudini/test7.bpl.expect
new file mode 100644
index 00000000..82afc94e
--- /dev/null
+++ b/Test/AbsHoudini/test7.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl
index 6c55016a..0b00bc19 100644
--- a/Test/AbsHoudini/test8.bpl
+++ b/Test/AbsHoudini/test8.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 function {:existential true} Assert(): bool;

 

 var g: int;

diff --git a/Test/AbsHoudini/test8.bpl.expect b/Test/AbsHoudini/test8.bpl.expect
new file mode 100644
index 00000000..82afc94e
--- /dev/null
+++ b/Test/AbsHoudini/test8.bpl.expect
@@ -0,0 +1,6 @@
+function {:existential true} {:inline} Assert() : bool
+{
+  false
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl
index c08edf6b..221234e5 100644
--- a/Test/AbsHoudini/test9.bpl
+++ b/Test/AbsHoudini/test9.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t

+// RUN: %diff %s.expect %t

 var v1: int;

 var v2: int;

 var v3: int;

diff --git a/Test/AbsHoudini/test9.bpl.expect b/Test/AbsHoudini/test9.bpl.expect
new file mode 100644
index 00000000..ae5e9286
--- /dev/null
+++ b/Test/AbsHoudini/test9.bpl.expect
@@ -0,0 +1,66 @@
+function {:existential true} {:inline} b1() : bool
+{
+  true
+}
+function {:existential true} {:inline} b2() : bool
+{
+  true
+}
+function {:existential true} {:inline} b3() : bool
+{
+  true
+}
+function {:existential true} {:inline} b4() : bool
+{
+  false
+}
+function {:existential true} {:inline} b5() : bool
+{
+  true
+}
+function {:existential true} {:inline} b6() : bool
+{
+  false
+}
+function {:existential true} {:inline} b7() : bool
+{
+  true
+}
+function {:existential true} {:inline} b8() : bool
+{
+  true
+}
+function {:existential true} {:inline} b9() : bool
+{
+  true
+}
+function {:existential true} {:inline} b10() : bool
+{
+  false
+}
+function {:existential true} {:inline} b11() : bool
+{
+  true
+}
+function {:existential true} {:inline} b12() : bool
+{
+  false
+}
+function {:existential true} {:inline} b13() : bool
+{
+  true
+}
+function {:existential true} {:inline} b14() : bool
+{
+  true
+}
+function {:existential true} {:inline} b15() : bool
+{
+  true
+}
+function {:existential true} {:inline} b16() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/README.md b/Test/README.md
index 98013581..4446aa4f 100644
--- a/Test/README.md
+++ b/Test/README.md
@@ -110,8 +110,9 @@ The RUN lines may use several substitutions
 - ``%boogie`` expands to the absolute path to the Boogie executable with any set

   options and prefixed by ``mono`` on non Windows platforms

 

-- ``%diff`` expands to the diff tool being used. This is ``diff`` on non Windows

-  platforms and ``fc`` on Windows.

+- ``%diff`` expands to the diff tool being used. This is ``diff`` on non

+  Windows platforms and ``pydiff`` on Windows. Do not use the ``fc`` tool

+  because it is buggy when tests are run concurrently.

 

 - ``%OutputCheck`` expands to the absolute path to the OutputCheck tool

 

diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg
index 9cd85ef6..e103edde 100644
--- a/Test/lit.site.cfg
+++ b/Test/lit.site.cfg
@@ -111,13 +111,16 @@ else:
     lit_config.warning('Skipping solver sanity check on Windows')
 
 # Add diff tool substitution
+commonDiffFlags=' --unified=3 --strip-trailing-cr --ignore-all-space'
 diffExecutable = None
 if os.name == 'posix':
-    diffExecutable = 'diff --unified=3 --strip-trailing-cr --ignore-all-space'
+    diffExecutable = 'diff' + commonDiffFlags
 elif os.name == 'nt':
-    diffExecutable = 'fc /W'
+    pydiff = os.path.join(config.test_source_root, 'pydiff.py')
+    diffExecutable = sys.executable + ' ' + pydiff + commonDiffFlags
 else:
     lit_config.fatal('Unsupported platform')
+lit_config.note("Using diff tool '{}'".format(diffExecutable))
 
 config.substitutions.append( ('%diff', diffExecutable ))
 
diff --git a/Test/pydiff.py b/Test/pydiff.py
new file mode 100644
index 00000000..407fe251
--- /dev/null
+++ b/Test/pydiff.py
@@ -0,0 +1,100 @@
+#!/usr/bin/env python
+"""
+Simple driver around python's difflib that implements a basic ``diff`` like
+tool. This exists to provide a simple ``diff`` like tool that will run on
+Windows where only the ``fc`` tool is available.
+"""
+import argparse
+import difflib
+import os
+import sys
+
+
+def main(args):
+    parser = argparse.ArgumentParser(formatter_class=argparse.RawDescriptionHelpFormatter,
+                                     description=__doc__
+                                    )
+    # Open in binary mode so python doesn't try and do
+    # universal line endings for us.
+    parser.add_argument('from-file',
+                        type=argparse.FileType('rb'),
+                       )
+    parser.add_argument('to-file',
+                        type=argparse.FileType('rb'),
+                       )
+    parser.add_argument('-U','--unified=',
+                        type=int,
+                        default=3,
+                        help='Number of context lines to show. '
+                             'Default %(default)s'
+                       )
+    parser.add_argument('--strip-trailing-cr',
+                        action='store_true',
+                        help='strip trailing carriage return when comparing'
+                       )
+    parser.add_argument('--ignore-all-space','-w',
+                        action='store_true',
+                        help='Ignore all whitespace characters when comparing'
+                       )
+
+    parsedArgs = parser.parse_args(args)
+    fromFile, fromFileName = preProcess(getattr(parsedArgs,'from-file'),
+                                        parsedArgs.strip_trailing_cr,
+                                        parsedArgs.ignore_all_space
+                                       )
+    toFile, toFileName = preProcess(getattr(parsedArgs,'to-file'),
+                                    parsedArgs.strip_trailing_cr,
+                                    parsedArgs.ignore_all_space
+                                   )
+
+    result = difflib.unified_diff(fromFile,
+                                  toFile,
+                                  fromFileName,
+                                  toFileName,
+                                  n=getattr(parsedArgs,'unified='),
+                                 )
+    # Force lazy computation to happen now
+    result = list(result)
+
+    if len(result) == 0:
+        # Files are identical
+        return 0
+    else:
+        for l in result:
+            sys.stdout.write(l)
+        return 1
+
+def preProcess(openFile, stripTrailingCR=False, ignoreAllSpace=False):
+    """
+    Helper function to read lines in a file and do any necessary
+    pre-processing
+    """
+    original = openFile.readlines()
+
+    # Translation table deletes white space characters Note we don't remove
+    # newline characters because this will create a mess when outputting the
+    # diff. Is this the right behaviour?
+    deleteChars=' \t'
+    translationTable = str.maketrans('','', deleteChars)
+
+    copy = [ ]
+    for line in original:
+        newLine = str(line.decode())
+
+        if stripTrailingCR:
+            if newLine[-2:] == '\r\n' or newLine[-2:] == '\n\r':
+                newLine = newLine[:-2] + '\n'
+
+        if ignoreAllSpace:
+            newLine = newLine.translate(translationTable)
+
+        copy.append(newLine)
+
+    return (copy, openFile.name)
+
+def getFileName(openFile):
+    return openFile.name
+
+if __name__ == '__main__':
+    sys.exit(main(sys.argv[1:]))
+