# SMTInterpol Proof Checker

You can now experiment with SMTInterpol and its proofs in your browser. Paste an SMT-LIB 2.6 compatible input problem in the box below and click the run button. You can also upload files or drag and drop them into this box. This runs SMTInterpol in your browser (powered by TeaVM). Please note that running large problems can affect the performance of your browser.

SMTInterpol will write its proof into the second text box. You
can click on the check proof button to check the proof. You can
also edit the proof or provide your own proof. The format of the
proof box should be the same as the standard output of the SMT
solver (with print-success disabled). It should contain the
word `unsat`

followed by the proof. Error reporting is
very crude and most errors will be reported by a
cryptic message. You can check the JavaScript console (F12 on
most browsers) for more information.

There is a preliminary documentation of the proof format.