Javaプログラムとの対話中にZ3が死ぬ

私は、Z3プロセスを起動し、stdin/outをキャプチャし、SMTLIB2コマンドを送信し、その答えを読み取るJavaプログラムを持っています。 OSX上でJavaプログラムとの対話中にZ3が死ぬ

これは正常に動作しますが、Linux上で、多くの場合、Z3が予期せずエラーコードで139

を死ぬその標準出力からの読み取り中にこのエラーコードは何を意味していることが起こりますか？

https://stackoverflow.com/questions/38409443/bit-vector-tactic-leads-to-exit-code-139-in-z3pyの可能な複製 - Z3のバージョンと139の原因？ – Rob

Linuxシステムは、受信時にerrono 128 +信号を返します。 128 + 11 = 139。 SIgnal 11はSIGSEV（セグメンテーション違反）です。 =一部のC++コードにメモリアクセスのバグがあります。 – MikeJRamsey56

フィードバックのおかげで、Z3のバージョンは4.4.1です。今日私はZ3のマスターブランチをクローン作成してビルドしましたが、この問題は修正されているようです。 –

答えはコメントに寄せられました。 MikeJRamsey56から、コード139は128 + 11であり、11はセグメンテーション違反であるSIGSEVです。 OPからは、Z3 4.4.1のバグが修正されているようです。

2016-08-04 13:04:17

答えて