如何给Z3中的变量赋值？

Question

我在SMT-Z3-Python-Solver中有一个变量x，并且已经给它赋值了23。
如何将x的值重新分配给例如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"