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.
