У меня есть несколько простых ограничений, связанных с умножением реалов в z3, которые производятunknown, Кажется, проблема в том, что они обернуты в тип данных, так как в развернутой версииsat.

Вот упрощенный случай:

(declare-datatypes () ((T (NUM (n Real)))))

(declare-const a T)
(declare-const b T)
(declare-const c T)

(assert (is-NUM a))
(assert (is-NUM b))
(assert (is-NUM c))

(assert (= c (NUM (* (n a) (n b)))))

(check-sat)
;unknown

И без типа данных:

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

(assert (= c (* a b)))

(check-sat)
;sat

Я использую z3 3.2, но это также можно воспроизвести в веб-интерфейсе.