[tlaplus] Viewing the SMT Encoding from TLAPM

[Willy Schultz <will62794@xxxxxxxxx>]

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.

[1] https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.652.2372&rep=rep1&type=pdf

-- 
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/9ce526bb-8566-4514-be39-c65bb26a58fdn%40googlegroups.com.