2 files changed, 8 insertions, 16 deletions
diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer
index 376d9f3a..d2418bd4 100644
--- a/Test/AbsHoudini/Answer
+++ b/Test/AbsHoudini/Answer
@@ -1,19 +1,11 @@
 
 -------------------- f1.bpl --------------------
-Running Abstract Houdini
-	Post: g == old(g) + 1
-	Post: g == old(g) + 2
-	Post: g == old(g) + 3
-	Pre: old(g) == 0
-Trying summary for foo: (And (== (fooSummaryPred g g@0) false) (== (fooSummaryPred g g@0) false))
-Trying summary for foo: (And (== (fooSummaryPred g g@0) (And (== g@0 (+ g 1)) (Implies (== g 0) (== g@0 (+ g 2))) (Implies (== g 0) (== g@0 (+ g 3))))) (== (fooSummaryPred g g@0) (And (== g@0 (+ g 1)) (Implies (== g 0) (== g@0 (+ g 2))) (Implies (== g 0) (== g@0 (+ g 3))))))
-Trying summary for foo: (And (== (fooSummaryPred g g@0) (== g@0 (+ g 1))) (== (fooSummaryPred g g@0) (== g@0 (+ g 1))))
-Trying summary for main: (And (== (mainSummaryPred g g@3) false) (== (mainSummaryPred g g@3) false))
-Trying summary for main: (And (== (mainSummaryPred g g@3) (And (== g@3 (+ g 1)) (Implies (! (== g 0)) (== g@3 (+ g 2))) (Implies (! (== g 0)) (== g@3 (+ g 3))))) (== (mainSummaryPred g g@3) (And (== g@3 (+ g 1)) (Implies (! (== g 0)) (== g@3 (+ g 2))) (Implies (! (== g 0)) (== g@3 (+ g 3))))))
-Trying summary for main: (And (== (mainSummaryPred g g@3) (Implies (== g 0) (== g@3 (+ g 1)))) (== (mainSummaryPred g g@3) (Implies (== g 0) (== g@3 (+ g 1)))))
-Summary of main:
-(old(g) == 0 ==> g == old(g) + 1)
 Summary of foo:
 g == old(g) + 1
+Summary of main:
+(old(g) == 0 ==> g == old(g) + 1)
+Prover time = 0.0260026
+Number of prover queries = 6
+Witness written to absHoudiniWitness.bpl
 
 Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/AbsHoudini/f1.bpl b/Test/AbsHoudini/f1.bpl
index 5ea6797b..e5ed85ef 100644
--- a/Test/AbsHoudini/f1.bpl
+++ b/Test/AbsHoudini/f1.bpl
@@ -26,7 +26,7 @@ procedure foo()
 }
 
 procedure {:template} summaryTemplate();
-  ensures g == old(g) + 1;
-  ensures g == old(g) + 2;
-  ensures g == old(g) + 3;
+  ensures {:post} g == old(g) + 1;
+  ensures {:post} g == old(g) + 2;
+  ensures {:post} g == old(g) + 3;
   ensures {:pre} old(g) == 0;