Why does verbosity level 0 not silence all outputs?

[marcelwa]

I ran into strange behavior that might be totally intended. I wanted to report it just in case. In several bits of code, (presumably debug) output is generated if verbosity level is set to 0. An example can be found e.g. here and here. Since I'm using Z3 in a CLI-based tool, this output generated bugs me a little as the user should not be concerned about it.

As the links show, this refers to current master 2bd8d3b and dates back several versions.

Is there a way to silence Z3 in this regard? I've figured that setting verbosity to negative values is not a thing.

Thanks for your help and best regards!

[NikolajBjorner]

I wanted to catch these cases because they are legal, but I don't know of a setting where this should happen.

[marcelwa]

On specific inputs those cases occur in my tool. I don't think I can boil it down to a toy example showcasing the behavior as those instances are huge and I have no idea which part triggers the mentioned lines in the ba_solver. Everything seems to work fine in the solver and I have no issues with the constraints. It's just the generated output that I was concerned about. If no further handling is needed, this issue can be closed.

[NikolajBjorner]

I increased verbosity to 1. In case you have bandwidth to collect a sample where this triggers it will be appreciated as it would show either a bug or a scenario that I could not produce when I wrote the code.