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.
No comments:
Post a Comment