can you give hint me why case2 doesn't work??

root@ubuntu:/root# cat test.py

!/usr/bin/env python

from z3 import *

CASE1

key = BitVec("tag", 32)
solve(RotateRight(key, 7) == 0x9a000000)

CASE2

tag = BitVec("tag", 32)
key = BitVecVal(0, 32)
key = key + tag
RotateRight(key, 7)
solve(key == 0x9a000000, tag == 77)
root@ubuntu:/root# ./test.py
[tag = 77]
no solution

Hello!

I saw here that Z3 supports having hard and soft constraints using assert-soft. However, I'm wondering if you know how I can use the python API to do that?

Cheers,
Varun

from z3 import *

a, b = BitVecs('a b', 32)
c, d = Ints('c d')
solve(a + b == 1337)
solve(c + d == 1337)

s = Solver()
s.add(a + b == 1337)
print s.check()
print s.model()

s = Solver()
s.add(c + d == 1337)
print s.check()
print s.model()

s = Solver()
s.add(a + b == 1337)
s.push()
s.add(a*a == 32)
print s
print s.check()

s.pop()
print s
print s.check()
print s.model()
print (469762080 + 3825206553) & 0xffffffff

root@ubuntu:~/z3-playground/essentials# python test.py
[b = 0, a = 1337]
[d = 0, c = 1337]
sat
[b = 0, a = 1337]
sat
[d = 0, c = 1337]
[a + b == 1337, a*a == 32]
unsat
[a + b == 1337]
sat
[b = 469762080, a = 3825206553]
1337

my test result show me that push&pop operation affect to result.

but It's not what I want. How can I fix it?

https://udel.edu/~os/riddle-solution.html

Apologies if this is not the correct place to ask such questions.