From d7dd2464cb438c32b11b2f16923999da1fb89d5b Mon Sep 17 00:00:00 2001
From: Peter Collingbourne <peter@pcc.me.uk>
Date: Mon, 11 Jun 2012 16:42:45 +0100
Subject: GPUVerify: factor out CreateCandidateInvariant from
 AddCandidateInvariant

This allows us to build candidate invariants in situations where we
don't have a Region, such as the block predicator.
---
 Source/GPUVerify/GPUVerifier.cs | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index d43bda9a..fbf27669 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -2155,15 +2155,20 @@ namespace GPUVerify
         }
 
         internal void AddCandidateInvariant(IRegion region, Expr e, string tag)
+        {
+            region.AddInvariant(CreateCandidateInvariant(e, tag));
+        }
+
+        internal PredicateCmd CreateCandidateInvariant(Expr e, string tag)
         {
             Constant ExistentialBooleanConstant = MakeExistentialBoolean(Token.NoToken);
             IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);
             PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));
             invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List<object>(new object[] { tag }), null);
-            region.AddInvariant(invariant);
             Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
+            return invariant;
         }
-
+            
         internal Implementation GetImplementation(string procedureName)
         {
             foreach (Declaration D in Program.TopLevelDeclarations)
-- 
cgit v1.2.3