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

On Sat, 31 Aug 2024 16:03:30 +0200,
Klemens Nanni <kn@openbsd.org> wrote:
>
> 31.08.2024 16:35, Klemens Nanni пишет:
> > 30.08.2024 22:17, Kirill A. Korinsky пишет:
> >> On Tue, 27 Aug 2024 21:59:25 +0200,
> >> Klemens Nanni <kn@openbsd.org> wrote:
> >>>
> >>> New diff including all the feedback above, you can now hack on the port and
> >>> iterate over 'make retest' until it no longer crashes (or you give up) ;-)
> >>>
> >>
> >> Here an updated version based on yours. Changes:
> >> - improved testing to use smt2 models from examples;
> >
> > Sounds good. Do those strictly supersede the reproducers from the issue,
> > or would it make sense to run both in post-test?
> >

Yes, they are. They crashed z3 which is built by clang with the same stacktrace.

> > I also noticed that our -DZ3_ENABLE_EXAMPLE_TARGETS=ON is already the default
> > and =OFF results in less targets being built without PLIST change or effect
> > on your tests, so I think we can spare a few cycles and avoid building
> > whatever isn't used, anyway.
> >
> > Plus, -DZ3_INCLUDE_GIT_HASH=OFF implies -DZ3_INCLUDE_GIT_DESCRIBE=OFF, so
> > the latter can be dropped as well.
> >
> >> By some reason gcc produces z3 which works quite stable.
> >
> > Switching COMPILER makes /usr/src/lib/check_sym report removal of dynamically
> > exported symbols, so a major bump to 5.0 would be in order.
> >
> > Good find, perhaps we can narrow it down further!
> >

Quite possible that this is triggered by clang bug similar to
https://github.com/llvm/llvm-project/issues/55844

> +.for _repro in \
> + '(declare-datatype)' \
> + '(declare-datatype a)' \
> + '(declare-const p Bool)'
> + -echo ${_repro:Q} | (cd ${WRKBUILD} && ./z3 -in)

not sure that this :Q is required. If I run it with :Q z3 complains as:

(error "line 1 column 1: unexpected character")
(error "line 1 column 19: unexpected token used as datatype name")
(error "line 1 column 20: unexpected character")

because it makes a command line like:

echo \'\(declare-datatype\)\' |

which produces an invalid input for z3.

--
wbr, Kirill