Skip to content

Commit 2ffab1a

Browse files
authored
Z3 decRefs on context close fix (#116)
* z3 decref for converterNativeObjects on context close fix * z3 decref for uninterpretedSortValue Decls/Interpreters on context close fix
1 parent e5e3bf3 commit 2ffab1a

1 file changed

Lines changed: 15 additions & 4 deletions

File tree

ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,17 +4,17 @@ import com.microsoft.z3.Context
44
import com.microsoft.z3.Solver
55
import com.microsoft.z3.decRefUnsafe
66
import com.microsoft.z3.incRefUnsafe
7-
import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap
8-
import it.unimi.dsi.fastutil.longs.LongOpenHashSet
9-
import it.unimi.dsi.fastutil.longs.LongSet
10-
import it.unimi.dsi.fastutil.objects.Object2LongOpenHashMap
117
import io.ksmt.KContext
128
import io.ksmt.decl.KDecl
139
import io.ksmt.expr.KExpr
1410
import io.ksmt.expr.KUninterpretedSortValue
1511
import io.ksmt.solver.util.KExprLongInternalizerBase.Companion.NOT_INTERNALIZED
1612
import io.ksmt.sort.KSort
1713
import io.ksmt.sort.KUninterpretedSort
14+
import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap
15+
import it.unimi.dsi.fastutil.longs.LongOpenHashSet
16+
import it.unimi.dsi.fastutil.longs.LongSet
17+
import it.unimi.dsi.fastutil.objects.Object2LongOpenHashMap
1818

1919
@Suppress("TooManyFunctions")
2020
class KZ3Context(
@@ -264,6 +264,17 @@ class KZ3Context(
264264
if (isClosed) return
265265
isClosed = true
266266

267+
uninterpretedSortValueInterpreter.clear()
268+
269+
uninterpretedSortValueDecls.keys.decRefAll()
270+
uninterpretedSortValueDecls.clear()
271+
272+
uninterpretedSortValueInterpreters.decRefAll()
273+
uninterpretedSortValueInterpreters.clear()
274+
275+
converterNativeObjects.decRefAll()
276+
converterNativeObjects.clear()
277+
267278
z3Expressions.keys.decRefAll()
268279
expressions.clear()
269280
z3Expressions.clear()

0 commit comments

Comments
 (0)