search

UnitTestBot / ksmt

Kotlin/Java API for various SMT solvers
https://ksmt.io/
Apache License 2.0
30 stars 14 forks source link

Fix Z3 model detach #139

Closed Damtev closed 1 year ago

Damtev commented 1 year ago 
io.ksmt.solver.KSolverUnsupportedFeatureException: Z3 internal decl Z3_OP_INTERNAL is not supported
    at app//io.ksmt.solver.z3.KZ3ExprConverter.convertApp-h_aMM1A(KZ3ExprConverter.kt:414)
    at app//io.ksmt.solver.z3.KZ3ExprConverter.convertNativeExpr-h_aMM1A(KZ3ExprConverter.kt:163)
    at app//io.ksmt.solver.util.KExprLongConverterBase.convertFromNative(KExprLongConverterBase.kt:27)
    at app//io.ksmt.solver.z3.KZ3ExprConverter.convertExpr(KZ3ExprConverter.kt:85)
    at app//io.ksmt.solver.z3.KZ3Model.funcInterp(KZ3Model.kt:342)
    at app//io.ksmt.solver.z3.KZ3Model.interpretation(KZ3Model.kt:101)
    at app//io.ksmt.solver.z3.KZ3Model.detach(KZ3Model.kt:164)