GPUVerify: the non-uniform loop invariant is not a candidate invariant

Thanks to Ally for pointing this out.

1 files changed, 5 insertions, 6 deletions

diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs
index a006bde6..5e61734d 100644
--- a/Source/GPUVerify/BlockPredicator.cs
+++ b/Source/GPUVerify/BlockPredicator.cs
@@ -186,9 +186,9 @@ class BlockPredicator {
 
         pExpr = Expr.Eq(cur, blockIds[runBlock]);
         CmdSeq newCmdSeq = new CmdSeq();
+        AddNonUniformInvariant(newCmdSeq, runBlock);
         if (CommandLineOptions.Inference && blockGraph.Headers.Contains(runBlock)) {
           AddUniformCandidateInvariant(newCmdSeq, runBlock);
-          AddNonUniformCandidateInvariant(newCmdSeq, runBlock);
         }
         newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));
         foreach (Cmd cmd in runBlock.Cmds)
@@ -215,7 +215,7 @@ class BlockPredicator {
           "uniform loop"));
   }
 
-  private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) {
+  private void AddNonUniformInvariant(CmdSeq cs, Block header) {
     var loopNodes = new HashSet<Block>();
     foreach (var b in blockGraph.BackEdgeNodes(header))
       loopNodes.UnionWith(blockGraph.NaturalLoops(header, b));
@@ -232,10 +232,9 @@ class BlockPredicator {
     }
     var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]),
                                             (e, exit) => Expr.Or(e, Expr.Eq(cur, exit)));
-    cs.Add(verifier.CreateCandidateInvariant(new NAryExpr(Token.NoToken,
-                 new IfThenElse(Token.NoToken),
-                 new ExprSeq(fp, curIsHeaderOrExit, Expr.Eq(cur, returnBlockId))),
-                 "non-uniform loop"));
+    cs.Add(new AssertCmd(Token.NoToken, new NAryExpr(Token.NoToken,
+             new IfThenElse(Token.NoToken),
+             new ExprSeq(fp, curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)))));
   }
 
   public static void Predicate(GPUVerifier v, Program p) {