Can an ADT reuse same field names for different constructors?

[adwait]

The following fails (on SMTLIB2Interface):

module main {

    datatype adt_t = A (i : integer, b : bv4) | B (i : integer, b : boolean);

    var adt1 : adt_t;
    var adt2 : adt_t;

    init {
        adt1 = B(10, true);
        adt2 = A(10, 4bv4);
    }

    next {
        adt1' = B(adt1.i+1, adt1.b);
        adt2' = A(adt2.i+1, adt2.b);
    }

    property match: adt1.i == adt2.i;

    control {
        v = bmc(2);
        check;
        print_results;
        v.print_cex_json();
    }

}

with

Type error at line 16: Argument type error in application.
        adt1' = B(adt1.i+1, adt1.b);
                ^
Parsing failed. 1 errors found.

Renaming apart the fields in the ADT to, e.g.,

datatype adt_t = A (ia : integer, ba : bv4) | B (ib : integer, bb : boolean);

fixes the issue.

---

Will explicitly forbidding field reuse across constructors fix this in general? If so, we could internally/silently perform field renaming.

Even if there is no change, we need some documentation clarifying such details.

[adwait]

Added a new test tracking this: test-adt-28-fieldreuse.ucl