search

UnitTestBot / ksmt

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

Z3: support fp.to_sbv internal decl #141

Closed Damtev closed 1 year ago

Damtev commented 1 year ago 
io.ksmt.solver.KSolverUnsupportedFeatureException: Z3 internal decl fp.to_sbv is not supported
    at app//io.ksmt.solver.z3.KZ3ExprConverter.tryConvertInternalAppExpr-aM00XZQ(KZ3ExprConverter.kt:591)
    at app//io.ksmt.solver.z3.KZ3ExprConverter.convertApp-h_aMM1A(KZ3ExprConverter.kt:413)
    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)