SMTInterpol Web Interface

You can now run an SMT solver 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.

; 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)

Run SMTInterpol to see the result here !