Inconsistent Results from consequences Interface Based on Constant Names

[ptr1120]

Summary:
I'm encountering inconsistent outcomes between the check and consequences methods when using the Z3 Python and dotnet API. The results differ based on the naming of constants. I have tested this behavior across Z3 versions 4.11.2 to 4.12.2.

Details:
When using the following snippet that employs Z3's Python API, the consequences method returns "unknown" while the check method returns "sat".

from z3 import *
a = Bool('a')
b = Bool('b')
c = Bool('c')
r = Bool('r_abc')
i = Int('int')

solver = Solver()
cardinality = And(AtLeast(a, b, c, 1), AtMost(a, b, c, 1))
reification = Implies(r, cardinality)
solver.add(reification)
intBound = And(i >= 1, i <= 1)
solver.add(intBound)

print(solver.check()) # Output: sat
print(solver.consequences([r],[a,b,c,r,i])) # Output: unknown

However, if the name of the integer constant is changed from 'int' to 'integer', both methods return "sat".

from z3 import *
a = Bool('a')
b = Bool('b')
c = Bool('c')
r = Bool('r_abc')
i = Int('integer')

solver = Solver()
cardinality = And(AtLeast(a, b, c, 1), AtMost(a, b, c, 1))
reification = Implies(r, cardinality)
solver.add(reification)
intBound = And(i >= 1, i <= 1)
solver.add(intBound)

print(solver.check()) # Output: sat
print(solver.consequences([r],[a,b,c,r,i])) # Output: sat

Additionally, varying the integer bounds or other constant names also leads to inconsistent results.

Query:
Any idea that helps identify the underlying issue causing this inconsistent behavior?

Thanks,
Peter

[LeventErkok]

(Possibly) Related: #4600