Performance issue when solving bit-vectors

[VoodooChild99]

Hi,

I'm using z3 to decide the satisfiability of bit-vector formulas. However, z3 failed to process one of the formulas (even after 1-2 hours). My working environment and the Python script to reproduce this problem are listed below:

z3 version: 4.11.2.0 OS: Ubuntu 20.04 Linux kernel version: 5.4.0-125-generic Arch: x86_64

from z3 import *

a = BitVec("a", 32)
b = BitVec("b", 32)
s = Solver()
e = ULT(3 * UDiv(a, 100), a - UDiv(2 * b, UDiv(2 * b, a)))
s.add(And(
  (a == 0) == False,
  ((a * 16) == 0) == False,
  (UDiv(b, 16 * a) == 0) == False,
  (UDiv(2 * b, a) == 0) == False,
  ULT(a, UDiv(2 * b, UDiv(2 * b, a))) == False
))
print(s.check(e))
print(s.model())

Could you please look into it? Thanks!

(Note: I‘m not sure if this formula is satisfiable. e can be further simplified to ULT(..., 0), which is obviously unsat, if b and a are integers. But this might not be the case since they are actually bit-vectors.)

[VoodooChild99]

Seems that the last constraint is the key. This smaller script can reproduce the problem:

from z3 import *

a = BitVec("a", 32)
b = BitVec("b", 32)
s = Solver()
e = ULT(3 * UDiv(a, 100), a - UDiv(2 * b, UDiv(2 * b, a)))
s.add(And(
  ULT(a, UDiv(2 * b, UDiv(2 * b, a))) == False
))
print(s.check(e))
print(s.model())

Also, I tried to check(e) directly without adding any constraints, z3 produces sat, but the model will make UDiv(2 * b, a) zero. Maybe this means that e is actually unsat when the divisor cannot be zero? But still, I don't know why z3 failed to produce a result after a long time.

Update: I'm sure e is satisfiable without the last constraint.

[NikolajBjorner]

z3 does not solve bit-vector problems with division/mod/rem well. The circuits created by bit-blasting these operations are not handled well by the search engine. This is not a new issue or a fluke.