scala - Scala^Z3 在解析器错误时终止正在运行的线程

Question

当我使用 Scala^Z3（Z3 3.2 和根据 Scala^Z3 java 库）并得到如下解析器错误：

(error "line 21 column 41: invalid command, '(' expected")
Error: parser error

执行的线程被杀死，我无法通过用 try/catch 或任何东西包围代码来阻止它。

有没有办法阻止这种行为？

Answer 1

恐怕没什么可做的：据说exitZ3 库中有一个调用，这就是导致这种行为的原因。

据我了解 Java 本机接口，我无法阻止本机函数终止进程。我能做的最好的事情是向 JVM 添加一个退出钩子，它可以警告用户程序由于外部原因而终止，但这不会让您恢复控制流中的位置。

理想的解决方案当然是更新 Z3，使公共接口中的任何函数都不会调用exit。