On 20 Dec 2020, at 06:43, Willy Schultz <will...@gmail.com> wrote:
If my understanding is correct, TLAPM encodes TLA+ expressions into SMT-LIB format [1] and passes this to a backend solver e.g. Z3. I was wondering if it is possible to have the proof manager output the SMT-LIB formulas that it generates for inspection. I ask mostly out of curiosity i.e. I am interested about what this encoding looks like in practice. I have the proof manager set up on the command line. If there are any special debug flags I can pass to do this that would be great.
--
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/9ce526bb-8566-4514-be39-c65bb26a58fdn%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/78ca8885-0a21-450e-b23c-a31196e0ca6bn%40googlegroups.com.