Yet another explanation of modulo inverse using SMT-solvers

By which constant we must multiply a random number, so that the result would be as if we divided them by 3?

from z3 import *

m=BitVec('m', 32)


# wouldn't work for 10, etc

# random constant, must be divisible by divisor:

s.add(const*m == const/divisor)

print s.check()
print "%x" % s.model()[m].as_long()

The magic number is:


Indeed, this is modulo inverse of 3 modulo $2^{32}$:,-1,2%5E32%5D.

Let's check using my calculator:

[3] 123456*0xaaaaaaab
[3] (unsigned) 353492988371136 0x141800000a0c0 0b1010000011000000000000000000000001010000011000000
[4] 123456/3
[4] (unsigned) 41152 0xa0c0 0b1010000011000000

The task is simple enough to be solved using my tow-level SMT-solver.

It wouldn't work for 10, because there are no modulo inverse of 10 modulo $2^{32}$, SMT solver would give "unsat".

Why random constant must be divisible by divisor? See:

→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): dennis(@)