Some errata for smt-lib-reference-v2.6-r2021-05-12

[Siyuan Chen]

Dear SMT community,

I have just finished reading the smt-lib-reference-v2.6-r2021-05-12. It is a very good document for learning SMT indeed!

The following are some errata in my reading.

p.63 footnote 4

> In fact, it is even possible, although certainly not desirable, to have a definition like `(define-funs-rec ((f (x Bool) Bool)) ((not (f x))) )`,  which makes the set of formulas in the context unsatisfiable.

It missed a parenthesis. It should be `(define-funs-rec ((f ((x Bool)) Bool)) ((not (f x))))`

p.76

> If B is an Ω-signature with universe B and ...

It should be `Ω-structure`.

Thanks.

Best regards,
Siyuan Chen

[Pascal Fontaine]

Dear Siyuan Chen,

thanks a lot for your feedback!  These are indeed typos, they are now fixed in the last version on the web site.

Best,

  Pascal (also for Clark and Cesare)

Siyuan Chen --
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/5fe5f372-5db4-4de9-b94e-45e019df3fb0n%40googlegroups.com.