很抱歉重新发布这个问题， 如何让 z3 返回多个 unsat 核心，多个令人满意的分配
为了完整起见，上面链接中的原始问题是：
我有兴趣检索（用于 QF_LRA）
-多个（最小或其他）UNSAT核心和-多个SAT分配
我在论坛上查看了有关此主题的早期讨论，例如，如何在逻辑 QF_LRA 上使用 z3 时获得不同的未饱和内核。这些是指 z3 Python 教程，例如 http://rise4fun.com/Z3Py/tutorial/musmss，目前似乎已离线。我尝试了 github 等的其他建议来找到提到的教程，但没有运气。
感谢 Nikolaj Bjorner 发布了我之前问题的答案。但是，我不确定答案中发布的代码片段是否完整？有人可以对此发表评论吗？
我查看了引用的论文和 Mark Liffiton 的网页，在我原来的问题的答案中提到。如果可以重新发布或澄清完整的代码片段，那将是最有帮助的。
非常感谢