(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)

Mam dwa niezależne twierdzenia, jedno w nieliniowej arytmetyce i innych nieinterpretowanych funkcjach. Z3 daje „model nie jest dostępny” dla powyższego problemu. Czy istnieje sposób na ustawienie logiki na coś, co może obsłużyć oba jednocześnie? Dziękuję Ci.