Calvin,
Thanks for pointing out the problem in the document. The example in Section 3.6.4 explaining the use of 'as' is indeed incorrect.
Not fixing the example in release 2021-04-02 was an oversight which we have now fixed with a new release: 2021-05-12.
To recap, 'as' takes two arguments: an ambiguous function symbol f (not a term) and the intended return type for f.
Both Z3 and CVC4 1.8 are compliant with respect to this specification. Older versions of CVC4 were not.
Best,
Cesare, also for Clark and Pascal
On 4 May 2021, at 13:16, Calvin Loncaric wrote:
A quick note for anyone following along at home:
CVC4 1.8 accepts only the second syntax, the same as Z3:
(assert (distinct x ((as Right (Either Int Int)) 10)))
It took some digging to find, but I think this is the pull request that
fixed it: https://github.com/CVC4/CVC4/pull/3111
I had been using CVC4 1.7 when I wrote my original email, even though CVC4
1.8 was released months earlier in June 2020. I installed CVC4 through
Homebrew, and the Homebrew package wasn't updated to 1.8 until recently
.
Also, there is now a new release of the SMT-LIB standard
--
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/CABf5HMg8c5PVqN5jjEE2oTEnymAzU%3DW%3D3P8wKU0hSBpeOa-B1g%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/D4452CD1-10DE-440A-BB40-0601B2D81CBB%40uiowa.edu.