z3-solver 简单方法遍历多解

使用条件列表遍历多解

while(s.check()==sat): condition = [] m = s.model() p="" for i in range(32): p+=chr(int("%s" % (m[flag[i]]))) condition.append(flag[i]!=int("%s" % (m[flag[i]]))) print(p) s.add(Or(condition))