CODEWITHSUNDEEP
z3exponent
Daniel Genin
Daniel Genin

Reputation: 483

Z3 fractional exponent bug (maybe)

Running Z3 on the following sequence of propositions

(declare-const x Real)
(assert (= 1 (^ x (/ 1 2))))
(check-sat-using qfnra-nlsat)
(get-model)
(eval (= x (^ x (/ 1 2))))

produces

sat
(model
    (define-fun x () Real
        (- 1.0)) 
)
Z3(5, 25): ERROR: even root of negative number is not real

Note that the final line simply evaluates the equation from line 2 on the proposed solution for x, so Z3 seems to contradict itself. Is this a bug or am I missing something?

Upvotes: 0

Views: 66

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

This example exposes some bugs in the facilities dealing with root objects. A fix has been checked into the master branch (Z3 now returns unknown for this tactic).

Upvotes: 1

Related Questions