search

marcoeilers / nagini

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
Mozilla Public License 2.0
233 stars 8 forks source link

Logs of Z3-solver #206

Closed alex28sh closed 2 months ago

alex28sh commented 2 months ago

Hello, now, for debugging and understanding the reasons for some issues we are facing, we are interested in logs produced by Z3 Solver. Is there any way to extract these logs?

Thank you for considering this request.

Best regards, Alex

alex28sh commented 2 months ago

Or, maybe, is there any way of printing code, used by Z3 solver?

marcoeilers commented 2 months ago

Assuming you're using Nagini with the default Viper backend, you can use the command line argument --viper-arg=--enableTempDirectory, and Viper will create a tmp folder in the current directory that contains .smt2 files that contain all interactions with Z3.