Как назначить новое значение переменной в Z3?

Question

У меня есть переменная x внутри SMT-Z3-Python-Solver и ей уже присвоено значение 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"