From 3d3793316668d179e92d802424ee28956c5e86b6 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 29 Feb 2024 11:49:39 +0100
Subject: [PATCH] Actually fixing the right function this time

---
 src/main/scala/decider/Decider.scala | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
index c6dccdcdc..abc06064d 100644
--- a/src/main/scala/decider/Decider.scala
+++ b/src/main/scala/decider/Decider.scala
@@ -429,15 +429,18 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl], toStack: Boolean): Unit = {
       if (!toStack) {
-        macros foreach prover.declare
-
-        _declaredFreshMacros = _declaredFreshMacros ++ macros
+        for (m <- macros) {
+          if (!_declaredFreshMacros.contains(m)) {
+            prover.declare(m)
+            _declaredFreshMacros = _declaredFreshMacros.appended(m)
+          }
+        }
       } else {
         for (m <- macros) {
-          if (!_declaredFreshMacros.contains(m))
+          if (!_declaredFreshMacros.contains(m)) {
             prover.declare(m)
-
-          _declaredFreshMacros = _declaredFreshMacros.appended(m)
+            _declaredFreshMacros = _declaredFreshMacros.appended(m)
+          }
           _freshMacroStack.foreach(l => l.append(m))
         }
       }