Standardisation of quotations in `echo`

[edwardcwang]

Different solvers seem to differ on whether or not to include the quotation marks in the echo command. e.g. Z3 and Yices exclude the quotes whereas the others include the quotes.

$ cvc5 -i -q --no-interactive
(echo "hello")
"hello"
$ cvc4 -i -q --no-interactive --lang smt2
(echo "hello")
"hello"
$ mathsat 
(echo "hello")
"hello"
$ z3 -smt2 -v:0 -in
(echo "hello")
hello
$ yices-smt2 --smt2-model-format --incremental
(echo "hello")
hello

[fontainep]

Hi,

thanks for your comment. The standard document clarifies that: "(echo s) where s is a string literal, simply prints back s as is—including the surrounding double-quotes." See page 68 of the latest 2.6 release: https://smt-lib.org/papers/smt-lib-reference-v2.6-r2024-09-20.pdf

Does this answer your question?

[edwardcwang]

Hi, thanks for clarifying. In this case z3 and yices are out of spec then?

[fontainep]

It seems so...

[edwardcwang]

So for Z3 as per https://github.com/Z3Prover/z3/issues/5745 it turns out that (set-option :smtlib2_compliant true) is necessary.

$ z3 -smt2 -v:0 -in
(set-option :smtlib2_compliant true)
success
(echo "A")
"A"
$ z3 -smt2 -v:0 -in
(echo "A")
A

[edwardcwang]

For yices this is already filed in https://github.com/SRI-CSL/yices2/issues/416

[fontainep]

Thanks for digging out the information! Can we close the issue for SMT-LIB?

[edwardcwang]

Of course! Thanks for your help.