diff --git a/ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt b/ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt index f4eae36e9..834c28b7c 100644 --- a/ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt +++ b/ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt @@ -4,10 +4,6 @@ import com.microsoft.z3.Context import com.microsoft.z3.Solver import com.microsoft.z3.decRefUnsafe import com.microsoft.z3.incRefUnsafe -import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap -import it.unimi.dsi.fastutil.longs.LongOpenHashSet -import it.unimi.dsi.fastutil.longs.LongSet -import it.unimi.dsi.fastutil.objects.Object2LongOpenHashMap import io.ksmt.KContext import io.ksmt.decl.KDecl import io.ksmt.expr.KExpr @@ -15,6 +11,10 @@ import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.solver.util.KExprLongInternalizerBase.Companion.NOT_INTERNALIZED import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort +import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap +import it.unimi.dsi.fastutil.longs.LongOpenHashSet +import it.unimi.dsi.fastutil.longs.LongSet +import it.unimi.dsi.fastutil.objects.Object2LongOpenHashMap @Suppress("TooManyFunctions") class KZ3Context( @@ -264,6 +264,17 @@ class KZ3Context( if (isClosed) return isClosed = true + uninterpretedSortValueInterpreter.clear() + + uninterpretedSortValueDecls.keys.decRefAll() + uninterpretedSortValueDecls.clear() + + uninterpretedSortValueInterpreters.decRefAll() + uninterpretedSortValueInterpreters.clear() + + converterNativeObjects.decRefAll() + converterNativeObjects.clear() + z3Expressions.keys.decRefAll() expressions.clear() z3Expressions.clear()