CODEWITHSUNDEEP
z3smtsat
user6600604
user6600604

Reputation:

Running time analysis of Z3

I'm using the Z3 SMT solver implemented through python. I have the source code, and I would like to have some, any, indication that the process is running. Is it possible to use some verbose command or anything to get an idea of what the process is currently doing? I know the algorithm behind it, but I want to visualize, even with printf, what is occurring in the code.

Thanks!

Upvotes: 1

Views: 949

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

You can use:

      set_option(verbose=10)

to obtain verbose output to standard err.

After a solver has finished, you can get statistics using the 

     statistics()

method.

In debug mode you can use 

     enable_trace("arith")

to get low level traces (here given with "arith" as an example tag). This is intended for debugging only.

Upvotes: 3

Related Questions