zagier.smt2

; z3 zagier.smt2

(declare-const p Int)

(declare-const k Int)
(assert (> k 0))
(assert (= p (+ 1 (* 4 k))))

(assert (forall ((a Int) (b Int)) (not (and (<= 2 a) (<= 2 b) (= p (* a b))))))

(declare-datatypes () ((Triple (mk (x Int) (y Int) (z Int)))))

(define-fun S ((t Triple)) Bool
  (and (= (+ (* (x t) (x t)) (* 4 (y t) (z t))) p)
       (<= 0 (x t)) (<= 0 (y t)) (<= 0 (z t))))
(define-fun f1 ((t Triple)) Triple
  (mk (x t) (z t) (y t)))
(define-fun f2 ((t Triple)) Triple
  (ite (< (+ (x t) (z t)) (y t))
       (mk (+ (x t) (* 2 (z t))) (z t) (- (y t) (x t) (z t)))
       (ite (< (* 2 (y t)) (x t))
            (mk (- (x t) (* 2 (y t))) (+ (- (x t) (y t)) (z t)) (y t))
            (mk (- (* 2 (y t)) (x t)) (y t) (+ (- (x t) (y t)) (z t))))))

(declare-const t Triple)
(assert (S t))

(push)
(assert (not (S (f1 t))))
(check-sat)                             ; unsat
(pop)

(push)
(assert (not (= t (f1 (f1 t)))))
(check-sat)                             ; unsat
(pop)

(push)
(assert (not (S (f2 t))))
(check-sat)				; unsat
(pop)

(push)
(assert (not (= t (f2 (f2 t)))))
(check-sat)                             ; unsat
(pop)

(push)
(assert (= t (f2 t)))
(assert (not (= (x t) (y t))))
(check-sat)                             ; unsat
(pop)

(push)
(assert (= t (f2 t)))
(assert (not (and (= 1 (x t)) (= 1 (y t)))))
(check-sat)                             ; unknown
(pop)