2016-04-15 4 views
0

Ich verwende Java API von Z3. Beim Überprüfen der 'ZUFRIEDENHEIT' (s.status) erhalte ich einen Segmentierungsfehler. Kann jemand bitte helfen, dieses Problem zu debuggen. Gibt es eine Möglichkeit, Nachricht zu dumpen, damit ich dieses Problem debuggen kann. Ich habe versucht mit Log.open(), aber es schien nicht viel zu helfen.Segmentierungsfehler für Z3 SMT

Vielen Dank im Voraus.

Antwort

1

Log.open() muss vor jeder anderen Interaktion mit Z3 aufgerufen werden. Sobald es aktiviert ist, wird es eine Datei namens z3.log erzeugen, die wir wiedergeben können, ohne auf Ihre Anwendung/Eingabe/Daten/etc zugreifen zu müssen.

Weder 'SATISFIABILITY' noch s.status sind gültige Z3/Java Ausdrücke, also kann ich nicht sagen, was genau Sie versuchen zu tun. Wenn Sie glauben, dass irgendetwas davon auf einen Fehler in Z3 zurückzuführen ist, erstellen Sie bitte ein neues Problem in unserem issue tracker.