Z3 Online Demonstrator
SMT-LIB 2 Standard
Z3 sources
Reset
Execute
Input
SMT-LIB 2 script
; Variable declarations (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) ; Constraints (assert (> a 0)) (assert (> b 0)) (assert (> c 0)) (assert (= (+ (* a a) (* b b)) (* c c))) ; Solve (check-sat) (get-model)