On Sat, 31 Aug 2024 16:03:30 +0200, Klemens Nanni <[email protected]> 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 <[email protected]> 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
