Failed to solve siglog_fig2_sol.smt2

[rainoftime]

Whenever I try z3 4.3.2 or 4.4.1, this case cannot be solved.

[agurfinkel]

Please use spacer.

z3 -v:1 fixedpoint.engine=spacer siglog_fig2_sol.smt2
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...6 rules 0s)
(transform N7datalog27mk_quantifier_instantiationE...no-op 0s)
(transform N7datalog8mk_scaleE...no-op 0s)
(transform N7datalog18mk_karr_invariantsE...no-op 0s)
(transform N7datalog14mk_array_blastE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...3 rules 0s)
(transform N7datalog12mk_bit_blastE...no-op 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...3 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...3 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog8mk_sliceE...no-op 0s)
non-diff: (= (:var 2) (+ (:var 1) (:var 0)))
non-utvpi: (= (:var 2) (+ (:var 1) (:var 0)))
Entering level 1
Entering level 2
(define-fun I ((x!0 Int) (x!1 Int) (x!2 Int) (x!3 Int)) Bool
  (and (<= (+ (* (- 1) x!2) x!0 (* (- 1) x!3)) 0)
       (<= (+ (* (- 1) x!0) x!2 (* (- 1) x!1) x!3) 0)
       (<= (+ x!1 (* (- 1) x!3) x!0 (* (- 1) x!2)) 0)))
unsat

[rainoftime]

Thank you!