From beebf18b5cbeff329a9bb90d1ce8a874a94c2f39 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 26 Feb 2024 12:32:46 +0100 Subject: [PATCH] Just prevent re-declarations without changing types to set --- src/main/scala/decider/Decider.scala | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 6f9814d33..c6dccdcdc 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -410,9 +410,12 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = { if (!toSymbolStack) { - functions foreach prover.declare + for (f <- functions) { + if (!_declaredFreshFunctions.contains(f)) + prover.declare(f) - _declaredFreshFunctions = _declaredFreshFunctions ++ functions + _declaredFreshFunctions = _declaredFreshFunctions + f + } } else { for (f <- functions) { if (!_declaredFreshFunctions.contains(f))