Don't create duplicate new vars for uclid created vars

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

@@ -156,7 +156,7 @@ class BlockFlattenerPass extends RewritePass {
           val readSet = StatementScheduler.readSets(blk.asInstanceOf[BlockStmt].stmts, context)
           acc ++ readSet
         }
-      }.filter(id => context.map.contains(id) && context.map(id).isInstanceOf[Scope.StateVar])
+      }.filter(id => context.map.contains(id) && context.map(id).isInstanceOf[Scope.StateVar] && !id.name.startsWith("__ucld"))
 
       // create new vars. We only need new variables for the reads because there should only be
       // one write to a variable in a concurrent block. Blocks with more than one write will have been
@@ -219,59 +219,6 @@ class BlockFlattener() extends ASTRewriter(BlockFlattener.getName(), new BlockFl
   override val repeatUntilNoChange = true
 }
 
-// This pass changes the order of any statements in a block so that
-// assignments to state variables are moved to the end of the block.
-// This avoids issues where one submodule reads from a variable after another
-// submodule has written to it, without introducing additional variables
-// It must be run after the procedures have been inlined and converted into SSA.
-class BlockSorterPass extends RewritePass {
-  lazy val logger = Logger(classOf[BlockSorterPass])
-
-  override def rewriteBlock(blkStmt : BlockStmt, context : Scope) : Option[Statement] = {
-    logger.debug("==> [%s] Input:\n%s".format(analysis.passName, blkStmt.toString()))
-    val init = (List.empty[Statement], Map.empty[Identifier, Type])
-
-    def isStateVarAssign(st : Statement) : Boolean = {
-      st match {
-        case AssignStmt(lhss, rhs) => {
-          lhss.exists {
-            case LhsId(id) => context.map.contains(id) && context.map(id).isInstanceOf[Scope.StateVar] && !(id.toString contains "_ucld_")
-            case _ => false
-          }
-        }
-        case _ => false
-      }
-    }
-
-    val endStmts = blkStmt.stmts.filter(st => isStateVarAssign(st))
-    logger.debug("Moving the following statements to the end of the block: " + endStmts.toString())
-    val filteredStmts = blkStmt.stmts.filter(endStmts.contains(_)==false)
-    logger.debug("Moving these statements to the start of the block " + filteredStmts.toString())
-    val result = BlockStmt(blkStmt.vars, filteredStmts++endStmts, blkStmt.isProcedural)
-    logger.debug("<== Result:\n" + result.toString())
-    Some(result)
-}
-}
-
-object BlockSorter {
-  var index = 0
-  def getName() : String = {
-    index += 1
-    "BlockSorter:" + index.toString()
-  }
-}
-
-class BlockSorter() extends ASTRewriter(BlockSorter.getName(), new BlockSorterPass())
-{
-  override val repeatUntilNoChange = true
-   // Don't reorder procedural code
-  override def visitInit(init : InitDecl, context : Scope) : Option[InitDecl] = Some(init)
-  // Don't reorder procedural code
-  override def visitProcedure(proc : ProcedureDecl, contextIn : Scope) : Option[ProcedureDecl] = Some(proc);
-
-}
-
-
 
 
 object Optimizer {

test/test-nested-instance-1.ucl

@@ -41,11 +41,16 @@ module main
     next(bar1);
   }
 
+  // bar1.foox.a is x, bar1.fooy.a is x. 
+  // y is bar1.z, which is bar1.foox.b + bar1.fooy.b
+  // This property says that x + 1 + x + 1 == y
   property b1: initd ==> (bar1.foox.a + 1 + bar1.fooy.a + 1 == y);
 
   control {
-      v = unroll(5);
+      v = unroll(1);
       check;
       print_results;
+      v.print_cex;
+      print_module;
   }
 }