segfault in mk_unit_resolution about z3 HOT 5 CLOSED

Is this for the opt branch? In this case it seems you are enabling proof mode, which should not be necessary.

from z3.

Indeed. Sure, I'll disable it, I just recall having segfaults with PROOF mode disabled and no performance benefits, but perhaps the situation has changed.
Thanks!

from z3.

Hopefully the segfaults you reported earlier without proof mode have been addressed. At least I looked at them and found problems with the difference logic engines for optimization. The behavior with proof mode is that Z3 uses the Simplex solver. The default solver selection has also changed somewhat recently, so it should pick the simplex engine unless instructed otherwise. The crash in mk_unit_resolution should of course be addressed, but hopefully this is not necessary for this use.

from z3.

Thanks! I've re-run my integration tests and the segfaults are gone, and the performance has increased as well.

from z3.

I am unable to reproduce the bug using the latest version of the opt branch.

from z3.