conversion method from my local antlr-based language to z3 constraints.

Z3Converter.kt

    override fun exitLiteral(ctx: LiteralContext) {
        exprs.push(when {
            ctx.FLOAT() != null -> z3.mkReal(ctx.FLOAT().text)
            ctx.INTEGER() != null -> z3.mkReal(ctx.INTEGER().text)
            ctx.CONSTANT() != null -> when(ctx.text.toLowerCase()){
                //RealExpr(z3, Native.rcfMkPi(z3))
//                "pi" -> z3.mkReal(Math.PI.toString())
                "pi" -> {
                    val exprCtor = RealExpr::class.constructors.single().apply { isAccessible = true }
                    val nCtxMember = Context::class.members.single { it.name == "nCtx" }.apply { isAccessible = true }
                    exprCtor.call(z3, Native.rcfMkPi(nCtxMember.call(z3) as Long))
                    // results in JVM crash with EXCEPTION_ACCESS_VIOLATION  
                }
                "e" -> z3.mkReal(Math.E.toString())
                else -> TODO()
            }
            else -> TODO()
        })

    }