How to check the theorem that involves some trigonometry with Z3 prover?

Question

I'm trying to proof the following proposition with Z3 Theorem Prover:

|CA|^2 = |AB|^2 + |BC|^2,
|AB| = cos(alpha),
|BC| = sin(alpha)
  =>
|CA| = 1

What exactly I do:

(declare-const AB Real)
(declare-const BC Real)
(declare-const CA Real)
(declare-const alpha Real)

(assert  (and (>= AB 0) (>= BC 0) (>= CA 0)) )
(assert  (= (^ CA 2) (+ (^ AB 2) (^ BC 2))) )
(assert  (= AB (cos alpha)) )
(assert  (= BC (sin alpha)) )

(assert (not  (= CA 1) ))

(check-sat)

I expect unsat but got unknown. Also I know that problem is concentrated in the part with functions sin and cos.

What am I doing wrong? Is it possible to do something at all?

Thanks for help!

Answer 1

z3 has a rather limited understanding of sin and cos, and I wouldn't expect it to be able to decide all such problems. For a detailed discussion on this, see https://github.com/Z3Prover/z3/issues/680. For complicated queries, it's normal for you to get unknown as an answer.

Having said that, you're in luck! Z3 can actually correctly answer your particular query; but you have to use the correct incantation. Instead of:

(check-sat)

Use

(check-sat-using qfnra-nlsat)

and z3 correctly deduces unsat for this problem. This form of check-sat tells z3 to use the internal nl-sat engine for nonlinear real arithmetic.