我想构造一个SMT公式，它有许多关于整数线性算术和布尔变量的断言，以及一些关于实数非线性算术和布尔变数的断言。整数和实数上的断言只共享布尔变量。例如，考虑以下公式：
(declare-fun b () Bool)
(assert (= b true))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (or (not b) (>= (+ x y) (- x (+ (* 2 z) 1)))))
(declare-fun r () Real)
(assert (or (not b) (= (+ (* r r) (* 3 r) (- 4)) 0)))
如果我用这个公式喂养z3，它会立即报告"未知"。但如果我去掉它的整数部分，我会立即得到解，它满足变量"r"的约束。我认为这意味着非线性约束本身对求解器来说并不困难。问题应该是混合整数上的（线性）约束和实数上的（非线性）约束。
所以我的问题如下。使用z3处理这种混合公式的正确方法是什么（如果有的话）？我对DPLL（T）的理解是，对于不同的约束，它应该能够使用不同的理论求解器来处理这样的公式。如果我错了，请纠正我。
正如George在评论中所说，Z3中的非线性求解器相当脆弱，开箱即用的性能也不太好。也就是说，在stackoverflow上有很多关于这个问题的问题和答案，例如，请参阅以下内容：
Z3与非线性算术的性能
Z3如何处理非线性整数运算？
Z3：非线性算术的奇怪行为
非线性算术和未解释函数
Z3定理证明：勾股定理（非线性算法）
z3中使用哪些技术来处理非线性整数实问题？
非线性整数运算的可满足性检验