我们可以在z3中使用带有软约束的量词吗？当它们一起使用时，我得到以下消息。
WARNING: optimization with quantified constraints is not supported
否，不支持。这是之前要求的，您可以添加您的意见：https://github.com/Z3Prover/z3/issues/1711