使用Z3符号执行时遭遇「model is not available」错误的求助

大家好，我最近在用Z3做符号执行相关测试时遇到了一个问题，想请教一下各位。

情况是这样的：我写了一段代码，通过伪随机数的输出反推种子，一开始用随机生成的v1和v2测试时，代码能正常运行；但当我把v1和v2替换成具体数值后，就一直出现「model is not available」的错误。我查了不少相关帖子，但没找到能解决我问题的答案。

我的代码如下：

SEED = 682466241
prng = RNG(SEED)
v1 = prng.next(26)
v2 = prng.next(26)
print(SEED, v1, v2)

v1 = 57508594
v2 = 29407552
s = Solver()
s.add(seed >= 0)
s.add(seed <= 0xFFFFFFFF)
s.add(RNG(seed).next(26) == v1)
s.add(RNG(seed).next2(26) == v2)
s.check()
#print(s.check())
#print(s.model())
m = s.model()
print("Seed is: ", m[seed])

prng = RNG(int(str(m[seed])))
prng.next(26)
prng.next(26)
v3 = prng.next(26)
print("V3 is:", v3)

这段代码参考了一篇关于破解滚动码锁的文章和配套视频，但我自己运行时就触发了模型不可用的错误。

有没有大佬能帮我看看问题出在哪？非常感谢！

备注：内容来源于stack exchange，提问作者A S