fixed few tests

Author: shazqadeer

Test/civl/regression-tests/Pure2.bpl

@@ -0,0 +1,20 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:layer 1,1} g:int;
+
+pure action P(x:int)
+{
+  assert x >= 0;
+}
+
+yield procedure {:layer 1} X(x:int)
+{
+  call {:layer 1} P(x);
+}
+
+yield procedure {:layer 1} Y(x:int)
+{
+  assert {:layer 1} x == 0;
+  call {:layer 1} P(x);
+}

Test/civl/regression-tests/Pure2.bpl.expect

@@ -0,0 +1,8 @@
+Pure2.bpl(8,3): Error: this gate of P could not be proved
+Execution trace:
+    Pure2.bpl(13,3): anon0
+Pure2.bpl(18,3): Error: this assertion could not be proved
+Execution trace:
+    Pure2.bpl(18,3): anon0
+
+Boogie program verifier finished with 2 verified, 2 errors

Test/civl/regression-tests/chris5.bpl

@@ -1,5 +1,9 @@
-// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %parallel-boogie /trustRefinement "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
+
+// flag /trustRefinement avoids duplicate error messages since the inlined assert in P
+// is checked during both invariant checking and refinement checking at layer 1
+
 var {:layer 1,1} g:int;
 
 pure procedure {:inline 1} P(x:int)

Test/civl/regression-tests/permissions-fail.bpl

@@ -1,6 +1,9 @@
-// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %parallel-boogie /trustRefinement "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
+// flag /trustRefinement avoids duplicate error messages since the precondition of Lemma
+// is checked during both invariant checking and refinement checking at layer 1
+
 var {:linear} {:layer 0,1} A : Set int;
 
 pure procedure Lemma (set: Set int, i: One int);