CODEWITHSUNDEEP
pythonz3z3py
Ahmed Ezzat
Ahmed Ezzat

Reputation: 85

Why this z3 equation is failing?

I need to solve this code (the code in C) 

if ( ((0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1)+ len_input_serial- 3 * ((0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1) != 14)
    return 0xFFFFFFFFLL;

that's my python script 

from z3 import *
len_input_serial = BitVec("serial_len",64)
solve(LShR(LShR(0xAAAAAAAAAAAAAAABL * len_input_serial,64),1) + len_input_serial - 3 * LShR(LShR(0xAAAAAAAAAAAAAAABL * len_input_serial,64),1) == 14)

However this gives me [serial_len = 14]

I know the solution should be around [42,38,40], so what's wrong here ?

Upvotes: 1

Views: 338

Answers (1)

alias
alias

Reputation: 30428

This expression:

(0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1

Is always equivalent to 0. If you right shift a 64-bit quantity to the right by 64 bits, you get 0. (Note that you are using LShr, which treats its input as an unsigned quantity.)

Therefore the whole thing simplifies to solving len_input_serial == 14, which is the answer Z3 is producing.

Note that when you write a long integer in Python (i.e., 0x123L etc.), you get infinite precision. (See here: Maximum value for long integer). In C, you get (most-likely) 64-bit integer. So, your Z3 code is actually correct; it's Python that's using a bigger precision here and thus causing the confusion.

Upvotes: 1

Related Questions