EnumSort declaration fails after translating from a different context

[shack]

The following program raises the exception: z3.z3types.Z3Exception: b'enumeration sort name is already declared' when executing the last line, even though the enum A has not been declared in the main context:

from z3 import *

c = Context()
m = main_ctx()
EnumSort('A', ['b', 'c'], ctx=c)
x = Int('x', ctx=c)
x.translate(m)
EnumSort('A', ['b', 'c'], ctx=m)

If I swap the last two lines, the exception is not raised. When I replace the enum declaration by Datatype, no problem occurs.

[NikolajBjorner]

this is expected behavior: When you translate from one context to another, the new context inherits data-type declarations from the first.

[shack]

First, thanks for looking at it. It doesn't seem to be the behavior for all data types:

from z3 import *

def decl_A(ctx):
    s = Datatype('A', ctx=ctx)
    s.declare('b')
    s.declare('c')
    return s.create()

c = Context()
m = main_ctx()
decl_A(ctx=c)
x = Int('x', ctx=c)
x.translate(m)
decl_A(ctx=m)

does not throw any exception. I did not check if the data type A is not translated back or just overwritten by the second declaration. Nevertheless, shouldn't the behavior be the same for all data types?

IMHO translating should only translate those data types the variable is dependent on, so I would expect the behavior of this example. But I might be wrong here.

To explain a bit further what I was doing: I was using context as namespaces. I have a function that solves a couple of SMT problems and declares data types to do that. It creates a context to keep these declarations local, translates in formulas from the main context, and translates the solutions (which don't use the data types) back to the main context. If that translation also translates back all the data types defined in that local context, I can basically not localize these declarations in a context because subsequent calls to that function will inherit the data type declarations from the main context to which they have been translated to by prior calls.