search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

Solving problems with formulas related to square roots #7249

Closed Heaven2024 closed 3 weeks ago

Heaven2024 commented 3 weeks ago

Hi! Z3 version 4.13.1 - 64 bit ubuntu:22.04

For the following examples：

(set-logic ALL)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const q36 Real)
(declare-const q37 Real)
(declare-const q38 Bool)
(declare-const q39 Bool)
(declare-const sqrt_q36 Real)
(assert (= (* sqrt_q36 sqrt_q36) q36))
(assert (exists ((q36 Real) (q37 Real) (q38 Bool) (q39 Bool))
   (and (ite q38 (= q36 (tan r0)) (= q36 (/ r1 2)))
       (ite q39 (> q37 sqrt_q36) (< q37 (* r1 2.5))))))
(check-sat)

results:

z3 test.smt2
unkonwn

cvc5  test.smt2
sat
NikolajBjorner commented 3 weeks ago

the arithmetic solver knows little to nothing about functions like "tan"