|Your theorem TEST3 is proved by Zenon and Isabelle, unlike the two others, so this doesn't prove that the SMT backend works correctly in your installation. The screenshot shows an error message "Cannot reach fixed point" that comes from a pre-processing step of SMT. If you are adventurous, you may try downloading the current version of TLAPS  and compiling from source .|
Hope this helps,
 See INSTALL at , but use a more recent version of OCaml, such as 4.11. https://tla.msr-inria.inria.fr/tlaps/content/Download/Source.html may also be useful, but you should be able to use your existing versions of Zenon and Isabelle.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A31745EB-5D37-4CC3-BDA8-9DB010DDA844%40gmail.com.