Sample program computes sat until version 4.8.9 but unknown with later versions

[bastianhagedorn]

Hi,

we have a sample program which returns unknown on versions > 4.8.9 including the latest version.
It should compute sat and find a model regardless of the version

from z3 import *

s = Solver()
 
Bc = Int("Bc")
d = Int("d")
warps_per_col = Int("warps_per_col")
warps_per_row = Int("warps_per_row")

# d = [16, ... 128] - power of two
_d = Int("_d")
s.add(d == 2**_d)
s.add(_d <= 4)
s.add(_d >= 4)                                                                                                                                                               
#s.add(_d == 4)

# Bc is multiple of 64
_Bc = Int("_Bc")
s.add(Bc == _Bc * 64)
#s.add(_Bc > 0)
s.add(_Bc == 1)

# Use 4 warps
s.add(warps_per_row == 2)
s.add(warps_per_col == 2)


s.add(d % ((Bc * d) / ((warps_per_row * warps_per_col) * 32)) == 0)

stat = s.check()
if stat == z3.sat:
    print(s.model())
else:
    print(stat)

[bastianhagedorn]

It works with version 4.8.9 on both OS but breaks with newer versions

[vinodgro]

it prints unknown with 4.9.0.0

[NikolajBjorner]

_d is fixed at 4, but the pre-processor doesn't detect this.
It should have replaced _d by 4 and then the problem can be dealt with.
Don't use exponentiation (with variables). There is almost no reasoning support for exponentiation.

It would still be better if pre-processor detected this.
So, this is good takeaway whether regardless of whether your manual elimination of exponentiation unblocks you.

[NikolajBjorner]

added bounds propagation to pre-processing solve-eqs.
Either way, you should not use exponentiation especially when the exponent is already fixed.