corrected use of ArrayStack

uuverifiers · Mar 11, 2024 · 4345836 · 4345836
1 parent 67a428d
commit 4345836
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/src/main/scala/lazabs/horn/bottomup/CEGAR.scala b/src/main/scala/lazabs/horn/bottomup/CEGAR.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2011-2024 Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -401,7 +401,7 @@ class CEGAR[CC <% HornClauses.ConstraintClause]
 
     for (n <- 0 until abstractEdges.size)
       if (abstractEdges(n).from.isEmpty)
-        edgesTodo += n
+        edgesTodo push n
 
     while (!edgesTodo.isEmpty) {
       val n = edgesTodo.pop
@@ -437,7 +437,7 @@ class CEGAR[CC <% HornClauses.ConstraintClause]
 
           for (outgoing <- edgesFromState get newTo)
             for ((_, nextN) <- outgoing)
-              edgesTodo += nextN
+              edgesTodo push nextN
         }
       }
     }

diff --git a/src/main/scala/lazabs/horn/preprocessor/ReachabilityChecker.scala b/src/main/scala/lazabs/horn/preprocessor/ReachabilityChecker.scala
@@ -64,7 +64,8 @@ object ReachabilityChecker extends HornPreprocessor {
 
     val fwdReachableClauses = {
       val workList = new ArrayStack[Predicate]
-      workList ++= fwdReachable
+      for (x <- fwdReachable)
+        workList push x
 
       // add entry predicates
       for (Clause(IAtom(p, _), Seq(), _) <- clauses)
@@ -103,7 +104,8 @@ object ReachabilityChecker extends HornPreprocessor {
 
     val bwdReachableClauses = {
       val workList = new ArrayStack[Predicate]
-      workList ++= bwdReachable
+      for (x <- bwdReachable)
+        workList push x
 
       // fixed-point iteration
       val clausesWithHeadPred = fwdReachableClauses groupBy (_.head.pred)

diff --git a/src/main/scala/lazabs/prover/PrincessAPI.scala b/src/main/scala/lazabs/prover/PrincessAPI.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2022 Hossein Hojjat and Philipp Ruemmer.
+ * Copyright (c) 2011-2024 Hossein Hojjat and Philipp Ruemmer.
  * All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
@@ -100,7 +100,8 @@ case class Tree[D](d : D, children : List[Tree[D]]) {
     def hasNext = !todo.isEmpty
     def next = {
       val Tree(data, children) = todo.pop
-      todo ++= children
+      for (c <- children)
+        todo push c
       data
     }
   }