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