Почему Z3 не может решить этот случай без, казалось бы, тривиальной модификации?

Первоначальная проблема:

(declare-const a Real)
(declare-const b Bool)
(declare-const c Int)

(assert (distinct a 0.))

(assert (= b (distinct (* a a) 0.)))

(assert (= c (ite b 1 0)))

(assert (not (distinct c 0)))

(check-sat)

Результат неизвестен.

Но последние два ограничения, вместе взятые, эквивалентны (assert (= b false)), и после выполнения этого переписать вручную

(declare-const a Real)
(declare-const b Bool)
(declare-const c Int)

(assert (distinct a 0.))

(assert (= b (distinct (* a a) 0.)))

(assert (= b false))

;(assert (= c (ite b 1 0)))

;(assert (not (distinct c 0)))

(check-sat)

Z3 теперь может решить этот экземпляр (он не пройден).

Почему Z3 может решить второй экземпляр, но не может решить первый, хотя первый экземпляр можно упростить до второго?

изменить:

При поиске проблемы я обнаружил кое-что очень странное.

Z3 решает следующий пример и возвращает «unsat»:

(declare-fun a() Real)
(declare-fun b() Bool)
(declare-fun c() Int)

(assert (distinct a 0.0))

(assert (= b (distinct (* a a) 0.0)))

(assert (= b false))

;(assert (= c 0))

(check-sat)

Но если я раскомментирую (assert (= c 0)), решатель вернет «неизвестно», хотя c=0 не имеет ничего общего с приведенными выше утверждениями.