Closed endre90 closed 6 months ago
I think one can only speculate without code to help reproduce this issue. This output looks like what I would guess the debug_ref_count
parameter might enable?
Hi,
here is a small example:
let cfg = Config::new();
let ctx = Context::new(&cfg);
let x = ast::Int::new_const(&ctx, "x");
let one = ast::Int::from_u64(&ctx, 1);
let zero = ast::Int::from_u64(&ctx, 0);
Running this prints the following:
2024-03-11T15:10:04.075Z DEBUG [z3::config] new config 0x557fffd1a800
2024-03-11T15:10:04.079Z DEBUG [z3::context] new context 0x557fffd1a900
2024-03-11T15:10:04.080Z DEBUG [z3::ast] new ast: id = 5, pointer = 0x557fffd52200
2024-03-11T15:10:04.080Z DEBUG [z3::ast] new ast: id = 6, pointer = 0x557fffd52220
2024-03-11T15:10:04.080Z DEBUG [z3::ast] new ast: id = 7, pointer = 0x557fffd52240
2024-03-11T15:10:04.080Z DEBUG [z3::ast] drop ast: id = 7, pointer = 0x557fffd52240
2024-03-11T15:10:04.080Z DEBUG [z3::ast] drop ast: id = 6, pointer = 0x557fffd52220
2024-03-11T15:10:04.080Z DEBUG [z3::ast] drop ast: id = 5, pointer = 0x557fffd52200
So, when I am running my actual model, there are tens of thousands of lines of this which I don't really want to see. I tried setting the parameter that you mentioned above, but it had no effect. Some ideas?
Thanks again, Endre
Hmm, I'm still not able to reproduce. I'm wondering if it's on z3 itself. How are you installing/building z3? Could it be built in debug mode?
I used the static-link-z3 feature. I now tried z3-sys, and doing the same things with the low level api doesn't produce the printouts. Does it mean that the hl api is adding these printouts when wrapping the low level?
It is the logging included in the high level api with log::debug; I ended up forking the repo to remove that, but also to expose some things like at_most from the z3_sys.
Greetings, I spent quite some time trying to figure out how to disable the default DEBUG output printing, but I couldn't find an answer. The print-out doesn't help me in this situation, and I would like to disable it if possible. Here is an example of what I get:
Any help is appreciated. Best Regards