From: Klemens Nanni <kn@openbsd.org>
Subject: Re: [update] math/z3: update to 4.13.0
To: OpenBSD ports <ports@openbsd.org>
Date: Sat, 31 Aug 2024 19:08:15 +0000

31.08.2024 18:10, Kirill A. Korinsky пишет:
> 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.

You're right, :Q remained from an earlier iteration.
I dropped it, yielding correct commands now, thanks.