python - 如何为 Z3 中的变量分配新值？

Question

我x在 SMT-Z3-Python-Solver 中有一个变量，并且已经为其分配了 value 23。
如何重新分配xto eg的值42？
我正在寻找类似的功能s.reassign(x == 42)。

# coding=utf-8
from z3 import *

x = Int('x')
s = Solver()

s.add(x == 36)
s.reassign(x == 42) # <- PseudoCode

if s.check() == sat:
    print s.model()[x]
else:
    print "UNSAT"

标签： pythonz3smtz3py