After reverse engineering a program, I found the constraints.

I have to find two unsigned numbers such that:

```
x + y = 0xC0ED91BD
```

and

```
x * y = Z
```

In the original program, the multiplication of the numbers is performed using imul instruction.

Z should be such that when only the lower 32-bits of Z are checked, it should be less than 60.

```
Z & 0x00000000ffffffff < 60
```

However, when I add the second equation as a constraint, z3 gives me an error.

Here's my code:

```
#! /usr/bin/python
from z3 import *
import sys
s = Solver()
result = int(sys.argv[1], 16)
x = Int('x')
y = Int('y')
s.add(x + y == result)
s.add(x > 0, y > 0)
s.add((x * y) & 0x00000000ffffffff < 60)
while s.check() == sat:
print s.model()
s.add(Or(x != s.model()[x], y != s.model()[y]))
```

**Updated:**

Here is the code based on the recommended solution:

```
#! /usr/bin/python
from z3 import *
import sys
s = Solver()
x = BitVec('x', 32)
y = BitVec('y', 32)
result = BitVecVal(int(sys.argv[1], 16), 32)
s.add(x + y == result)
s.add(x > 0, y > 0)
s.add(x * y < 10)
print s.check()
print s.model()
```

The binary is 64-bit.

However, the multiplication operation is performed using 32-bit integers as shown below:

```
mov edx, [rbp+var_14]
mov eax, [rbp+var_10]
imul eax, edx
```

So if eax = 0x425a95e5 and edx = 0x7e92fbd8

Then after multiplication using imul instruction, eax will store: 0x00000038.

Both, the Carry Flag and Overflow Flag bits in the EFLAGS register will be set after it.

The issue here is that you have declared `x`

and `y`

to be arbitrarily wide integers, as opposed to bit-vectors of a fixed length. Simply change your declarations to match what the underlying bit-size should be. Assuming you want your arithmetic to be done in 32 bits, you'd say:

```
x = BitVec('x', 32)
y = BitVec('y', 32)
```

instead. You should also declare `result`

similarly:

```
result = BitVecVal(int(sys.argv[1], 16), 32)
```

Once you make these changes, your program should work just fine.

Note that in this case masking with `0x00000000ffffffff`

isn't really necessary; since the numbers are already 32-bits wide. You only need to keep it if your `x`

and `y`

are larger; say 64 bits.

With the above changes, I get the following output when I run your program and call it with `0xC0ED91BD`

:

```
[y = 2123561944, x = 1113232869]
[y = 1440310864, x = 1796483949]
[y = 1171875408, x = 2064919405]
... many other lines ..
```

This might look confusing, as the numbers seem to be larger than what you think they should be. But remember that arithmetic over bitvectors is done modulo `2^n`

where `n`

is the bit-size, so the results are actually correct:

```
>>> 2123561944 + 1113232869 % 2**32 == 0xC0ED91BD
True
>>> 2123561944 * 1113232869 % 2**32 < 60
True
```

etc.

User contributions licensed under CC BY-SA 3.0