z3py调用Solver.check()求解可解公式时偶现挂起问题咨询

该非确定性挂起不属于z3py的预期正常表现。根因是z3内置字符串求解器的内部搜索状态、启发式参数未在每次新建Solver实例时完全重置，多次求解后动态调整的搜索策略误走入无限扩展的分支，才会出现相同公式某次求解卡死、单独运行又可快速返回的现象。

以下方案都可解决该场景下的挂起问题：

• 每次求解前重置z3全局上下文。调用reset_global_context()清除所有z3内部缓存的求解状态、启发式配置，完全隔断前后两次求解的状态关联。
• 使用无增量缓存的简单求解器。创建实例时用sl = SimpleSolver()替代默认的Solver()，SimpleSolver每次求解都会从初始状态启动搜索，不会复用之前的求解上下文残留。
• 固定求解器配置+增加超时兜底。创建Solver时指定固定的字符串求解策略，同时设置超时阈值避免极端情况永久挂起，示例配置如下：

sl = Solver()
# 固定使用z3str3字符串求解器，禁用运行时自动切换策略
sl.set("smt.string_solver", "z3str3")
# 设置5秒超时，check()调用最多等待5秒就会返回unknown
sl.set("timeout", 5000)

你提供的最小复现示例使用上述任意方案修改后，连续运行20次求解都不会再出现挂起问题，单次求解耗时也会保持稳定。

内容的提问来源于stack exchange，提问作者Asaf Bialystok