Re: [update] math/z3: update to 4.13.0

Klemens,

Thanks for review and tweak of the diff.

On Tue, 27 Aug 2024 21:59:25 +0200,
Klemens Nanni <kn@openbsd.org> wrote:
>
> MODPY_RUNDEP=No seems missing unless z3 really needs python at runtime.
>

It has python binding and python API, and can be used from python. Not sure
that it justify it.

> >>
> >> But it exists on the current version in ports, which means the update
> >> doesn't break anything new.
>
> Which we can use as an argument to not create too much fuzz and leave optimiztions
> on until a proper fix shows up; at least I cannot judge at all what impact that has.
>
> >>
> >
> > After spending some time to dig into the issue which lead to crash, I had
> > discovered that such crash doesn't reproduced if I build z3 wihtout
> > optimization (-O0).
>
> -O1 also crashes.
>

Frankly speaking z3 is quite unstable right now.

For example a build with -O0 crashes at different place (upstream issue is
updated) on trivial theorem:

(declare-const x Int)
(declare-const y Int)
(assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))
(check-sat)

but if I rewrite it into python API, it works:

~ $ python3
Python 3.11.9 (main, Aug 14 2024, 08:01:59) [Clang 16.0.6 ] on openbsd7
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> x, y = Ints('x y')
>>> s = Solver()
>>> s.add((x % 4) + 3 * (y / 2) > x - y)
>>> print(s.sexpr())
(declare-fun y () Int)
(declare-fun x () Int)
(assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))

>>>

my point: -O0 make it unstable but usefull, with any optimization it useless.

--
wbr, Kirill