Missing universe for uninterpreted sort

[wintersteiger]

There seem to be some combinations of circumstances in which the uninterpreted sorts and their universes are not in the model. In the example below, both x and y are assigned the same mysort!val!0, but model.sorts() is empty and model.get_universe(S) says None. It's the solve-eqs tactic that solves the problem, so I suspect the bug must be around that area. (If the ~ is taken off of the constraint, it goes all the way through to the SMT solver and the model is correct.)

from z3 import *

z3.set_param("model", True)
z3.set_param("model.completion", True)

ctx = z3.Context(model=True)
slvr = z3.Solver(ctx=ctx)
slvr.set("model", True)
slvr.set("model.completion", True)

S = z3.DeclareSort("mysort", ctx)
x = z3.Const("x", S)
y = z3.Const("y", S)
slvr.append(~(x != y))

print("Solver: " + str(slvr))
print("Result: " + str(slvr.check()))
model = slvr.model()
print("Model: " + str(model))
print("Sorts: " + str(model.sorts()))
print("Universe: " + str(model.get_universe(S)))

print("Eval: " + str(model.eval(x, True)))

produces

Solver: [Not(x != y)]
Result: sat
Model: [y = mysort!val!0, x = mysort!val!0]
Sorts: []
Universe: None
Eval: mysort!val!0

[wintersteiger]

Thanks for the quick fix!