Hello
on https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html
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.