From: Kirill A. Korinsky <kirill@korins.ky>
Subject: Re: [update] math/z3: update to 4.13.0
To: Klemens Nanni <kn@openbsd.org>
Cc: OpenBSD ports <ports@openbsd.org>
Date: Wed, 28 Aug 2024 04:08:08 +0200

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