CODEWITHSUNDEEP
z3smtz3py
Tan
Tan

Reputation: 115

z3: print a very long assertion

Take the following as an example.

trues = [True] * 1000
a = z3.And(trues)

So a is a conjunction of 1000 Trues. Note that this is not a practical example since a is logically equivalent to True.

If we print(a), the full assertion is not showed. Instead, the result is ended with ...).

To print the full assertion, one solution I found is to print the s-expression of a. That is, print(a.sexpr()). In this way, all of the 1000 Trues are showed.

So my question: is there a better way to print a very long assertion like a?

Upvotes: 1

Views: 281

Answers (1)

alias
alias

Reputation: 30525

Sure. Try:

import z3

z3.set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)

trues = [True] * 1000
a = z3.And(trues)

print(a)

You can play with the numbers to set_option to get something more reasonable for your use case.

Upvotes: 2

Related Questions