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.

; Can you prove that 1 + 1 is 2? (set-option :produce-proofs true) (set-option :proof-level lowlevel) (set-logic QF_LIA) (assert (not (= (+ 1 1) 2))) (check-sat) (get-proof)

unsat (let ((eq (= (+ 1 1) 2))) (res (not eq) (assume (not eq)) (res eq (poly+ (+ 1 1) 2) (not- (not eq)))))