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 Native Interface を理解している限り、ネイティブ関数がプロセスを終了するのを防ぐことはできません。私ができる最善の方法は、プログラムが外部の理由で終了していることをユーザーに警告できる終了フックを JVM に追加することですが、それでは制御フローにあった場所から再開することはできません。

もちろん、理想的な解決策は、Z3 を更新して、パブリック インターフェイスの関数が を呼び出さないようにすることexitです。