only do the intersection of read/write vars

src/main/scala/uclid/lang/BlockFlattener.scala

@@ -40,6 +40,8 @@ package uclid
 package lang
 
 import com.typesafe.scalalogging.Logger
+import java.util.jar.Attributes.Name
+
 
 class BlockVariableRenamerPass extends RewritePass {
   def renameVarList (vars : List[(Identifier, Type)], context : Scope) : List[(Identifier, Identifier, Type)] = {
@@ -140,7 +142,6 @@ class BlockFlattenerPass extends RewritePass {
   }
 
   def addConcurrentVars (blkStmt : BlockStmt, context: Scope) : BlockStmt = {
-
     val filteredStmts = blkStmt.stmts.filter(_.isInstanceOf[BlockStmt])
 
     if(filteredStmts.size != blkStmt.stmts.size)
@@ -157,13 +158,21 @@ class BlockFlattenerPass extends RewritePass {
           acc ++ readSet
         }
       }.filter(id => context.map.contains(id) && context.map(id).isInstanceOf[Scope.StateVar] 
-                              && (!id.name.startsWith("__ucld") || id.name.endsWith("_var")))
+                              && (!id.name.startsWith("__ucld")))
+
+      val writes = filteredStmts.foldLeft(Set.empty[Identifier]) {
+        (acc, blk) => {
+          val writeSet = StatementScheduler.writeSets(blk.asInstanceOf[BlockStmt].stmts, context)
+          acc ++ writeSet
+        }
+      }.filter(id => context.map.contains(id) && context.map(id).isInstanceOf[Scope.StateVar])
 
-      // create new vars. We only need new variables for the reads because there should only be
+      // create new vars. We only need new variables for the reads that are also written to 
+      // because there should only be
       // one write to a variable in a concurrent block. Blocks with more than one write will have been
       // caught earlier
       val varPairs: Map[Expr, Expr] =
-        reads.map(
+        reads.intersect(writes).map(
         id => (id.asInstanceOf[Expr] -> NameProvider.get("block_" + id.toString()).asInstanceOf[Expr])).toMap
       logger.debug("New vars: " + varPairs.toString())