This seems to be an error in the tutorial? See e.g. page 13 of http://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf