ADT Type Confusion

[FedericoAureliano]

Query generation fails in certain cases with multiple ADTs. The following is an example that makes the SMTLIB interface fail with [Assertion Failure]: Unexpected result from SMT solver: (error "line 12 column 38: unknown constant C")

module main {
    datatype adt1 = A() | B();
    datatype adt2 = C() | D();

    var y: adt1;
    var x: adt2;

    init {
        assert y == B();
        assert x == C();
    }


    control {
        bmc(0);
        check;
        print_results;
    }
}

I suspect the bug is also present in the Z3 interface but I haven't been able to trigger it.