search

Z3Prover / z3

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

Z3 proves `(= 0.0 (^ 0 (- 2))` #7241

Closed someplaceguy closed 1 month ago

someplaceguy commented 1 month ago

I'm not sure if this is expected, because I can't find any description of what Z3's power operator is supposed to do, but apparently the following returns unsat:

(assert (not (= (^ 0 (- 2)) 0.0)))
(check-sat)

I didn't expect this result because 0 raised to the power of -2 is usually infinite in math, not zero, so I expected Z3 to return unknown (or perhaps sat?). I get the same unsat result if I use reals (i.e. if I change 0 => 0.0 and 2 => 2.0.

Also, Z3 appears to return unsat for this input, as expected:

(assert (not (exists ((x Int)) (= (^ x 1) x))))
(check-sat)

But it returns unknown for the following similar one:

(assert (not (exists ((x Int)) (= (^ x 0) 1.0))))
(check-sat)

... even though replacing that assertion with (assert (not (= (^ 1 0) 1.0)))) makes Z3 return unsat as expected.

NikolajBjorner commented 1 month ago

the implemented semantics is at this point 0 ^ n = 0 for n != 0. the value of 0 ^ 0 is underspecified.