(declare-const x Real)
(declare-fun f (Real) Real)
(assert (= (f 1.0) 0.0))
(assert (= (* x x) (* 1.0 1.0)))
(check-sat)
(get-model)

Ich habe zwei unabhängige Behauptungen, eine in nichtlinearer Arithmetik und andere nicht interpretierte Funktionen. Z3 gibt ein "Modell ist nicht verfügbar" für das obige Problem an. Gibt es eine Möglichkeit, die Logik auf etwas festzulegen, das beide gleichzeitig verarbeiten kann? Vielen Dank.