Disabling persistent verbose pb solver log messages

[noajshu]

I have been trying for some time to eliminate all Z3 logging output from my C++ program. The undesired output looks like the following:

binary 199@15
167
binary -100@15
antecedent -100 is above consequent in stack
100
(100@15 98@15 -106@11 104@15)
-98
(-98@15 -118@15 -116@15 104@15)
antecedent -118 is above consequent in stack
-119
...

I found the "is above consequent in stack" string in pb_solver.cpp. I read the source code in that file to find the relevant tags to call Z3_disable_trace(tag), as a suggested here. I tried disabling these tags:

Z3_disable_trace("pb");
Z3_disable_trace("pb_verbose");
Z3_disable_trace("ba");
Z3_disable_trace("ba_verbose");
Z3_disable_trace("sat");
Z3_disable_trace("sat_verbose");

This does not silence the output above.

This issue seems related. In both cases the verbosity was 0. The solution then was to increase verbosity to 1, although no example problem instance was provided to reproduce the issue (let me know if a smtlib example would be helpful).

Is this a bug or is there a way to disable this log output using the z3 API? Thank you very much.

[NikolajBjorner]

It is most likely hitting a bug and the output is there to draw attention to it.
If you have a self-contained repro it would help understand.

[noajshu]

Thanks for the advice!
I found that the problem only appears when I add additional constraints to a z3::optimize object, after already finding the minimum, and then re-running .check() a second time.
I can therefore get around the problem by just re-building a new z3::optimize.
Does this seem like a bug or am I just using it wrong? If it's a bug I can work on getting a self-contained repro.

[NikolajBjorner]

it is a bug
maybe with a workaround.

[noajshu]

Thanks, I have a self-contained repro ReproduceZ3Bug.cpp.

(I built z3@5db133f8 with the cmake build on on my x86 Mac. I hope it triggers the error message for you on your platform, but if not please let me know.)

[NikolajBjorner]

it isn't reproducing so far. Tried with 3K random seeds, same result no assertion violations.

[noajshu]

Ok thanks! I also tried building on x86 ubuntu and the bitstring I included did not trigger the bug.
Since it is sensitive to the exact build conditions I have updated the gist to try random bitstrings. After waiting about 5 minutes it finds a bitstring that triggers the bug on my macbook and also a ubuntu box. If you run this for a while on your
platform, does it trigger the bug?

I'm preparing a docker image to reproduce this, and can upload that in .tar.gz exported format if this doesn't reproduce for you.

[NikolajBjorner]

thank you this works. Don't work on docker