From ee7de80777d7704a17c5a4f85491ef39024a974c Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 16 Sep 2024 11:39:43 +0200
Subject: [PATCH] Cleaning up code that records fresh functions and macros

---
 src/main/scala/decider/Decider.scala | 38 ++++++++--------------------
 1 file changed, 11 insertions(+), 27 deletions(-)

diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
index d4d8afe3..fd852e1d 100644
--- a/src/main/scala/decider/Decider.scala
+++ b/src/main/scala/decider/Decider.scala
@@ -515,41 +515,25 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     def freshMacros: Vector[MacroDecl] = _declaredFreshMacros
 
     def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = {
-      if (!toSymbolStack) {
-        for (f <- functions) {
-          if (!_declaredFreshFunctions.contains(f))
-            prover.declare(f)
-
-          _declaredFreshFunctions = _declaredFreshFunctions + f
-        }
-      } else {
-        for (f <- functions) {
-          if (!_declaredFreshFunctions.contains(f))
-            prover.declare(f)
-
+      for (f <- functions) {
+        if (!_declaredFreshFunctions.contains(f)) {
+          prover.declare(f)
           _declaredFreshFunctions = _declaredFreshFunctions + f
-          _freshFunctionStack.foreach(s => s.add(f))
         }
       }
+      if (toSymbolStack)
+        _freshFunctionStack.foreach(s => s.addAll(functions))
     }
 
     def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl], toStack: Boolean): Unit = {
-      if (!toStack) {
-        for (m <- macros) {
-          if (!_declaredFreshMacros.contains(m)) {
-            prover.declare(m)
-            _declaredFreshMacros = _declaredFreshMacros.appended(m)
-          }
-        }
-      } else {
-        for (m <- macros) {
-          if (!_declaredFreshMacros.contains(m)) {
-            prover.declare(m)
-            _declaredFreshMacros = _declaredFreshMacros.appended(m)
-          }
-          _freshMacroStack.foreach(l => l.append(m))
+      for (m <- macros) {
+        if (!_declaredFreshMacros.contains(m)) {
+          prover.declare(m)
+          _declaredFreshMacros = _declaredFreshMacros.appended(m)
         }
       }
+      if (toStack)
+        _freshMacroStack.foreach(l => l.appendAll(macros))
     }
 
     def pushSymbolStack(): Unit = {