Missing universe for uninterpreted sort #7121
Description
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