on tlaps

23 views
Skip to first unread message

Alex Tim

unread,
Apr 27, 2020, 8:48:59 AM4/27/20
to tlaplus
Hello

it is said

"In order to invoke CVC4, use the CVC4 or CVC4T identifiers in a USE or BY clause (but remember that CVC4 is not distributed with TLAPS)."

but when i try to apply a solver explicitly (even a standard one):
PROOF BY SMT (or BY Z3) it generates an exception "unknown operator"...

Thanks.

Stephan Merz

unread,
Apr 27, 2020, 8:51:51 AM4/27/20
to tla...@googlegroups.com
Does your module extend or instantiate TLAPS?

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d018bc38-2ff0-478d-99bb-1edf08eec574%40googlegroups.com.

Alex Tim

unread,
Apr 27, 2020, 9:01:06 AM4/27/20
to tlaplus
Thanks, Stephan. Sorry im newbie. The next question is now solved also

понедельник, 27 апреля 2020 г., 15:48:59 UTC+3 пользователь Alex Tim написал:
Reply all
Reply to author
Forward
0 new messages