1 files changed, 32 insertions, 0 deletions
diff --git a/Test/AbsHoudini/f1.bpl b/Test/AbsHoudini/f1.bpl
new file mode 100644
index 00000000..5ea6797b
--- /dev/null
+++ b/Test/AbsHoudini/f1.bpl
@@ -0,0 +1,32 @@
+var g: int;
+
+procedure {:entrypoint} main()
+  modifies g;
+{
+   var x: int;
+   var c: bool;
+
+   g := 1;
+  
+   if(c) {
+     g := g + 1;
+   } else {
+     g := 3;
+   }
+
+   call foo();
+
+   if(old(g) == 0) { g := 1; }
+}
+
+procedure foo() 
+  modifies g;
+{
+  g := g + 1;
+}
+
+procedure {:template} summaryTemplate();
+  ensures g == old(g) + 1;
+  ensures g == old(g) + 2;
+  ensures g == old(g) + 3;
+  ensures {:pre} old(g) == 0;