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.