1
Ich habe ein Java-Programm, das einen Z3-Prozess startet und mit ihm interagiert, indem er seine stdin/out erfasst, SMTLIB2-Befehle sendet und seine Antworten liest.Z3 stirbt bei der Interaktion mit einem Java-Programm
Auf OSX dies funktioniert gut, aber auf Linux kommt es häufig vor, dass zwar von seinem stdout Lesen unerwartet Z3 stirbt mit dem Fehlercode 139.
Was bedeutet dieser Code Fehler entdeckt?
Mögliches Duplikat von https://stackoverflow.com/questions/38409443/bit-vector-tactic-leads-to-exit-code-139-in-z3py - welche Version von Z3 und was ist der Code, der 139 verursacht ? – Rob
Linux-Systeme geben Fehler 128 + Signal zurück, wenn ein Signal empfangen wurde. 128 + 11 = 139. Kenne 11 ist SIGSEV (d. H. Segmentierungsverletzung). = Es gibt einen Speicherzugriffsfehler in einigen C++ - Code. – MikeJRamsey56
Danke für die Rückmeldung, die Version von Z3 ist 4.4.1. Heute habe ich geklont und den Master-Zweig von Z3 erstellt und es scheint, dass das Problem behoben ist. –