Merge

14 files changed, 519 insertions, 43 deletions

diff --git a/Chalice/scripts/create_release/create_release.bat b/Chalice/scripts/create_release/create_release.bat
index a0d67fd9..5aadd36e 100644
--- a/Chalice/scripts/create_release/create_release.bat
+++ b/Chalice/scripts/create_release/create_release.bat
@@ -6,7 +6,7 @@ set BASE_DIR=%~dp0\..\..
 set RELEASE_DIR_SRC=%~dp0\files

 set RELEASE_DIR_DST=%~dp0\release

 

-set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.8.1.final\chalice_2.8.1-1.0.jar

+set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.9.2\chalice_2.9.2-1.0.jar

 set CHALICE_JAR_DST=%RELEASE_DIR_DST%\chalice.jar

 

 pushd %BASE_DIR%

diff --git a/Chalice/tests/predicates/LinkedList-various.chalice b/Chalice/tests/predicates/LinkedList-various.chalice
new file mode 100644
index 00000000..a888b647
--- /dev/null
+++ b/Chalice/tests/predicates/LinkedList-various.chalice
@@ -0,0 +1,176 @@
+class Node

+{

+  var v:int;

+  var n:Node;

+  

+  predicate inv

+  { acc(v) && acc(n) && (n!=null ==> n.inv) }

+  

+  function len():int

+    requires inv;

+    ensures result>0;

+  {

+    unfolding inv in (n==null) ? 1 : 1+n.len()

+  }

+  

+  function get(i:int):int

+    requires inv && 0<=i && i<len();

+  {

+    unfolding inv in (i==0) ? v : n.get(i-1)

+  }

+  

+  method addLast(x:int)

+    requires inv;

+	ensures inv;

+	ensures len()==old(len())+1 && get(old(len()))==x;

+	ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));

+  {

+    unfold inv;

+    if(n==null)

+    {

+      n:=new Node;

+      n.v:=x; n.n:=null;

+      fold n.inv;

+    }

+    else

+    {

+      call n.addLast(x);

+    }

+    fold inv;

+  }

+  

+   method append(p:List)

+    requires inv && p!=null && p.inv;

+	ensures inv;

+	ensures len()==old(len()+p.len());

+	ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));

+	ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));

+  {

+    unfold inv;

+    if(n==null)

+    {

+      unfold p.inv;

+      n:=p.c;

+    }

+    else

+    {

+      call n.append(p);

+    }

+    fold inv;

+  }

+    

+  method remove(i:int)

+    requires inv && i>=0 && i<len()-1;

+	ensures inv;

+	ensures len()==old(len())-1;

+	ensures (forall j in [0..i+1] :: get(j)==old(get(j)));

+	ensures (forall j in [i+1..len()] :: get(j)==old(get(j+1)));

+  {

+    unfold inv;

+    if(i==0)

+    {

+      unfold n.inv;

+      n:=n.n;

+    }

+    else

+    {

+      call n.remove(i-1);

+    }

+    fold inv;

+  }

+}

+

+class List

+{

+  var c:Node;

+

+  predicate inv { acc(c) && (c!=null ==> c.inv) }

+  

+  function len():int

+    requires inv;

+    ensures result>=0;

+  {

+    unfolding inv in (c==null) ? 0 : c.len()

+  }

+  

+  function get(i:int):int

+    requires inv && 0<=i && i<len();

+  {

+    unfolding inv in c.get(i)

+  }

+    

+  method addFirst(x:int)

+    requires inv;

+	ensures inv;

+	ensures len()==old(len())+1 && get(0)==x;

+	ensures (forall i:int :: 1<=i && i<len() ==> get(i)==old(get(i-1)));

+  {

+    var p:Node;

+	

+    unfold inv;

+    p:=new Node; p.v:=x; p.n:=c; c:=p;

+	fold c.inv;

+	assert c.len()==old(len())+1

+	fold inv;

+  }

+  

+  method addLast(x:int)

+    requires inv;

+	ensures inv;

+	ensures len()==old(len())+1 && get(old(len()))==x;

+	ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));

+  {

+    unfold inv;

+    if(c==null)

+    {

+      c:=new Node;

+      c.v:=x; c.n:=null;

+      fold c.inv;

+    }

+    else

+    {

+      call c.addLast(x);

+    }

+    fold inv;

+  }

+  

+  method append(p:List)

+    requires inv && p!=null && p.inv;

+	ensures inv;

+	ensures len()==old(len()+p.len());

+	ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));

+	ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));

+  {

+    unfold inv;

+    if(c==null)

+    {

+      unfold p.inv;

+      c:=p.c;

+    }

+    else

+    {

+      call c.append(p);

+    }

+    fold inv;

+  }

+  

+  method remove(i:int)

+    requires inv && i>=0 && i<len();

+	ensures inv;

+	ensures len()==old(len())-1;

+	ensures (forall j in [0..i] :: get(j)==old(get(j)));

+	ensures (forall j in [i..len()] :: get(j)==old(get(j+1)));

+  {

+    unfold inv;

+    if(i==0)

+    {

+      unfold c.inv;

+      c:=c.n;

+    }

+    else

+    {

+      call c.remove(i-1);

+    }

+    fold inv;

+  }

+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10189.chalice b/Chalice/tests/regressions/workitem-10189.chalice
new file mode 100644
index 00000000..b37b83f2
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10189.chalice
@@ -0,0 +1,23 @@
+class Node { 
+	var v: int 
+	var next: Node 
+	 
+	predicate V { 
+			 acc(v) 
+		&& acc(next) 
+		&& (next != null ==> next.V) 
+	} 
+
+	unlimited function length(): int 
+		requires rd(V) 
+	{ 1 + unfolding rd(V) in next == null ? 0 : next.length() } 
+	 
+	unlimited function at(i: int): int
+		requires rd(V) 
+		requires i >= 0 
+		requires i < length() // XXXX
+	{
+		unfolding rd(V) in i == 0 ? v : next.at(i - 1)
+		// Precondition at XXX might not hold
+	} 
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10189.output.txt b/Chalice/tests/regressions/workitem-10189.output.txt
new file mode 100644
index 00000000..96f05468
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10189.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10189.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings

diff --git a/Chalice/tests/regressions/workitem-10208.chalice b/Chalice/tests/regressions/workitem-10208.chalice
new file mode 100644
index 00000000..ae1a7d89
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10208.chalice
@@ -0,0 +1,41 @@
+class Test {

+  var f1: int;

+  var f2: int;

+

+  predicate valid {

+    acc(f1) && acc(f2) && f1 == f2

+  }

+  

+  method test()

+    requires valid

+  {

+    unfold valid

+    f1 := 2

+    f2 := 2

+    fold valid

+    

+    /* --- not strictly necessary */

+    unfold valid

+    assert f1 == 2

+    fold valid

+    /* --- */

+    

+    call test2()

+    

+    unfold valid

+    assert f1 == 2 // BUG: this should not verify (1)

+    assert false // BUG: this should not verify (2)

+  }

+  

+  method test2()

+    requires valid

+    ensures valid

+    ensures unfolding valid in f1 == 1 // line (1) above verifies also without this postcondition

+  {

+    unfold valid

+    f1 := 1

+    f2 := 1

+    fold valid

+  }

+  

+}

diff --git a/Chalice/tests/regressions/workitem-10208.output.txt b/Chalice/tests/regressions/workitem-10208.output.txt
new file mode 100644
index 00000000..0666393a
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10208.output.txt
@@ -0,0 +1,8 @@
+Verification of workitem-10208.chalice using parameters="" 

+

+  26.5: Assertion might not hold. The expression at 26.12 might not evaluate to true.
+
+The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
+  9.3: The end of method test is unreachable.
+
+Boogie program verifier finished with 1 errors and 1 smoke test warnings

diff --git a/Chalice/tests/regressions/workitem-10221.chalice b/Chalice/tests/regressions/workitem-10221.chalice
new file mode 100644
index 00000000..2a8ae723
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10221.chalice
@@ -0,0 +1,158 @@
+// In this example, additional unfold/fold pairs make the verification of the last three methods fail.

+

+class Node {

+  var next : Node;

+  var val : int;

+

+  predicate list {

+    acc(next) && acc(val) && (next!=null ==> next.list)

+  }

+  

+  function vals() : seq<int>

+    requires list

+  {

+    unfolding list in (next == null ? [val] : [val] ++ next.vals())

+  }

+

+  function reverse_vals() : seq<int>

+    requires list

+  {

+    unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])

+  }

+

+  method reverse_in_place() returns (r:Node)

+    requires list;

+    ensures true;

+  {

+    var l : Node := this;

+    r := null;

+

+    var rev : seq<int> := this.reverse_vals();

+    

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+//      if (r != null) {

+//        unfold r.list; fold r.list;

+//      }

+      unfold l.list;

+//      if (l.next != null) {

+//        unfold l.next.list; fold l.next.list;

+//      }

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+    assert r.vals() == rev; // should be the post-condition

+  }

+  

+

+   method reverse_in_place_01() returns (r:Node)

+    requires list;

+    ensures true;

+  {

+    var l : Node := this;

+    r := null;

+

+    var rev : seq<int> := this.reverse_vals();

+    

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+//      if (r != null) {

+//        unfold r.list; fold r.list;

+//      }

+      unfold l.list;

+      if (l.next != null) {

+        unfold l.next.list; fold l.next.list;

+      }

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+    assert r.vals() == rev; // should be the post-condition

+  }

+  

+   

+

+   method reverse_in_place_10() returns (r:Node)

+    requires list;

+    ensures true;

+  {

+    var l : Node := this;

+    r := null;

+

+    var rev : seq<int> := this.reverse_vals();

+    

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+      if (r != null) {

+        unfold r.list; fold r.list;

+      }

+      unfold l.list;

+//      if (l.next != null) {

+//        unfold l.next.list; fold l.next.list;

+//      }

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+    assert r.vals() == rev; // should be the post-condition

+  }

+  

+   

+

+

+   method reverse_in_place_11() returns (r:Node)

+    requires list;

+    ensures true;

+  {

+    var l : Node := this;

+    r := null;

+

+    var rev : seq<int> := this.reverse_vals();

+    

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+      if (r != null) {

+        unfold r.list; fold r.list;

+      }

+      unfold l.list;

+      if (l.next != null) {

+        unfold l.next.list; fold l.next.list;

+      }

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+    assert r.vals() == rev; // should be the post-condition

+  }

+  

+   

+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10221.output.txt b/Chalice/tests/regressions/workitem-10221.output.txt
new file mode 100644
index 00000000..e209c3c1
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10221.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10221.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings

diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs
index d7841f0e..649d76d7 100644
--- a/Source/GPUVerify/ArrayControlFlowAnalyser.cs
+++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs
@@ -172,7 +172,9 @@ namespace GPUVerify
                 {

                     CallCmd callCmd = c as CallCmd;

 

-                    if (callCmd.callee != verifier.BarrierProcedure.Name)

+                    if (callCmd.callee != verifier.BarrierProcedure.Name &&

+                        callCmd.callee != verifier.BarrierInvariantProcedure.Name &&

+                        callCmd.callee != verifier.BarrierInvariantInstantiationProcedure.Name)

                     {

 

                         Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 868bcaa1..85821da2 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -18,7 +18,9 @@ namespace GPUVerify
 
         public Procedure KernelProcedure;
         public Implementation KernelImplementation;
-        public Procedure BarrierProcedure;
+        public Procedure BarrierProcedure;

+        public Procedure BarrierInvariantProcedure;

+        public Procedure BarrierInvariantInstantiationProcedure;
 
         public IKernelArrayInfo KernelArrayInfo = new KernelArrayInfoLists();
 
@@ -128,6 +130,42 @@ namespace GPUVerify
                 ResContext.AddProcedure(p);
             }
             return p;
+        }

+

+        private Procedure FindOrCreateBarrierInvariantProcedure() {

+          var p = CheckSingleInstanceOfAttributedProcedure("barrier_invariant");

+          if (p == null) {

+            p = new Procedure(Token.NoToken, "barrier_invariant", new TypeVariableSeq(),

+                              new VariableSeq(new Variable[] { 
+                                    new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__cond", 
+                                      Microsoft.Boogie.Type.Bool), true)
+                              }),

+                              new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(),

+                              new EnsuresSeq(),

+                              new QKeyValue(Token.NoToken, "barrier_invariant", new List<object>(), null));

+            Program.TopLevelDeclarations.Add(p);

+            ResContext.AddProcedure(p);

+          }

+          return p;

+        }

+

+        private Procedure FindOrCreateBarrierInvariantInstantiationProcedure() {

+          var p = CheckSingleInstanceOfAttributedProcedure("barrier_invariant_instantiation");

+          if (p == null) {

+            p = new Procedure(Token.NoToken, "barrier_invariant_instantiation", new TypeVariableSeq(),

+                              new VariableSeq(new Variable[] { 
+                                    new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__t1", 
+                                      new BvType(32)), true),
+                                    new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__t2", 
+                                      new BvType(32)), true)
+                              }),

+                              new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(),

+                              new EnsuresSeq(),

+                              new QKeyValue(Token.NoToken, "barrier_invariant_instantiation", new List<object>(), null));

+            Program.TopLevelDeclarations.Add(p);

+            ResContext.AddProcedure(p);

+          }

+          return p;

         }
 
         private Procedure CheckSingleInstanceOfAttributedProcedure(string attribute)
@@ -1376,17 +1414,21 @@ namespace GPUVerify
 
             if(KernelArrayInfo.getGroupSharedArrays().Count > 0) {
 
-                Expr IfGuard1 = Expr.And(P1, LocalFence1);
-                Expr IfGuard2 = Expr.And(P2, LocalFence2);
-
-                bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
-                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),
-                    null));
-                bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
-                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),
-                    null));
-
-                bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()));
+                bigblocks.AddRange(
+                      MakeResetBlocks(Expr.And(P1, LocalFence1), KernelArrayInfo.getGroupSharedArrays()));

+

+                // This could be relaxed to take into account whether the threads are in different

+                // groups, but for now we keep it relatively simple

+

+                Expr AtLeastOneEnabledWithLocalFence =

+                  Expr.Or(Expr.And(P1, LocalFence1), Expr.And(P2, LocalFence2));

+

+                if (SomeArrayModelledNonAdversarially(KernelArrayInfo.getGroupSharedArrays())) {

+                  bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

+                    new IfCmd(Token.NoToken,

+                      AtLeastOneEnabledWithLocalFence,

+                      new StmtList(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), null));

+                }
             }
 
             if (KernelArrayInfo.getGlobalArrays().Count > 0)
@@ -1394,14 +1436,18 @@ namespace GPUVerify
                 Expr IfGuard1 = Expr.And(P1, GlobalFence1);
                 Expr IfGuard2 = Expr.And(P2, GlobalFence2);
 
-                bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
-                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),
-                    null));
-                bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
-                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),
-                    null));
-
-                bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()));
+                bigblocks.AddRange(
+                      MakeResetBlocks(Expr.And(P1, GlobalFence1), KernelArrayInfo.getGlobalArrays()));

+

+                Expr ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence = 

+                  Expr.And(Expr.And(GPUVerifier.ThreadsInSameGroup(), Expr.And(P1, P2)), Expr.Or(GlobalFence1, GlobalFence2));

+

+                if (SomeArrayModelledNonAdversarially(KernelArrayInfo.getGlobalArrays())) {

+                  bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

+                    new IfCmd(Token.NoToken,

+                      ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence,

+                      new StmtList(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), null));

+                }
             }
 
             StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok);
@@ -1432,16 +1478,16 @@ namespace GPUVerify
                                     new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1));
         }
 
-        private List<BigBlock> MakeResetBlocks(int Thread, ICollection<Variable> variables)
+        private List<BigBlock> MakeResetBlocks(Expr ResetCondition, ICollection<Variable> variables)
         {
             Debug.Assert(variables.Count > 0);
-            List<BigBlock> ResetAndHavocBlocks = new List<BigBlock>();
+            List<BigBlock> result = new List<BigBlock>();
             foreach (Variable v in variables)
             {
-                ResetAndHavocBlocks.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, Thread));
+                result.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, ResetCondition));
             }
-            Debug.Assert(ResetAndHavocBlocks.Count > 0);
-            return ResetAndHavocBlocks;
+            Debug.Assert(result.Count > 0);
+            return result;
         }
 
         private List<BigBlock> MakeHavocBlocks(ICollection<Variable> variables) {
@@ -1451,8 +1497,19 @@ namespace GPUVerify
             if (!ArrayModelledAdversarially(v)) {
               result.Add(HavocSharedArray(v));
             }
-          }
+          }

+          Debug.Assert(result.Count > 0);
           return result;
+        }

+

+        private bool SomeArrayModelledNonAdversarially(ICollection<Variable> variables) {

+          Debug.Assert(variables.Count > 0);

+          foreach (Variable v in variables) {

+            if (!ArrayModelledAdversarially(v)) {

+              return true;

+            }

+          }

+          return false;

         }
 
         public static bool HasZDimension(Variable v)
@@ -1765,7 +1822,7 @@ namespace GPUVerify
                 }
                 else if (c is AssertCmd)
                 {
-                    result.simpleCmds.Add(new AssertCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssertCmd).Expr, impl)));
+                    // Do not pull non-local accesses out of assert commands
                 }
                 else if (c is AssumeCmd)
                 {
@@ -1982,7 +2039,9 @@ namespace GPUVerify
 
         private int Check()
         {
-            BarrierProcedure = FindOrCreateBarrierProcedure();
+            BarrierProcedure = FindOrCreateBarrierProcedure();

+            BarrierInvariantProcedure = FindOrCreateBarrierInvariantProcedure();

+            BarrierInvariantInstantiationProcedure = FindOrCreateBarrierInvariantInstantiationProcedure();

             KernelProcedure = CheckExactlyOneKernelProcedure();
 
             if (ErrorCount > 0)
@@ -2039,8 +2098,9 @@ namespace GPUVerify
                 {
                     return D as Implementation;
                 }
-            }
-            Debug.Assert(false);
+            }

+            Error(Token.NoToken, "No implementation found for procedure \"" + procedureName + "\"");

+            Environment.Exit(1);
             return null;
         }
 
diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs
index c85989c9..7f14fcd0 100644
--- a/Source/GPUVerify/IRaceInstrumenter.cs
+++ b/Source/GPUVerify/IRaceInstrumenter.cs
@@ -15,7 +15,7 @@ namespace GPUVerify
 
         void AddRaceCheckingDeclarations();
 
-        BigBlock MakeResetReadWriteSetStatements(Variable v, int thread);
+        BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition);
 
         void AddRaceCheckingCandidateRequires(Procedure Proc);
 
diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs
index 6a934899..d1361ff4 100644
--- a/Source/GPUVerify/NonLocalAccessCollector.cs
+++ b/Source/GPUVerify/NonLocalAccessCollector.cs
@@ -70,7 +70,6 @@ namespace GPUVerify
             return collector.Accesses.Count > 0;

         }

 

-

         public override Expr VisitNAryExpr(NAryExpr node)

         {

             if (IsNonLocalAccess(node, NonLocalState))

diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index fae08aa3..6452331f 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -24,7 +24,7 @@ namespace GPUVerify
 
         }
 
-        public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)
+        public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition)
         {
             return new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
         }
diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index c73b9b13..71214cb3 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -473,16 +473,17 @@ namespace GPUVerify {
     }
 
 
-    public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) {
+    public BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition) {
       BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
-      if (Thread == 2) {
-        return result;
-      }
 
-      Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
-          new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));
-      Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
-          new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));
+      Expr ResetReadAssumeGuard = Expr.Imp(ResetCondition, 
+        Expr.Not(new IdentifierExpr(Token.NoToken,
+          new VariableDualiser(1, null, null).VisitVariable(
+            GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")))));
+      Expr ResetWriteAssumeGuard = Expr.Imp(ResetCondition,
+        Expr.Not(new IdentifierExpr(Token.NoToken,
+          new VariableDualiser(1, null, null).VisitVariable(
+            GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")))));
 
       if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v)) {
         ResetReadAssumeGuard = Expr.Imp(GPUVerifier.ThreadsInSameGroup(), ResetReadAssumeGuard);