uclid-org/uclid

`generateDatatype` does not generate inner types for ADTs

Closed this issue · 0 comments

The following fails (on SMTLIB2Interface):

module main {

    type e_t = enum {X, Y, Z};

    datatype adt_t = 
        A (a: e_t) | B (b : e_t, c: e_t);


    var adt1 : adt_t;
    var adt2 : adt_t;

    init {
        adt1 = A(X);
        adt2 = B(Y, Y);
    }

    next {
        adt1' = A(adt1.a);
        adt2' = B(adt2.b, adt2.c);
    }

    property match: adt1.a == adt2.b;

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

}

The SMT solver returns:

[Assertion Failure]: Unexpected result from SMT solver: (error "line 2 column 19: invalid datatype declaration, unknown sort '_type_enum_1_'")

as the generated SMT does not contain the declaration for the enum datatype.

Reason: generateDatatype does not actually return declarations created for newly discovered inner types:

val newType = "(declare-datatypes %s ((%s)))".format(nameString, constructorsString)
typeMap = typeMap.addSynonym(typeName, t)
(typeName, typeName :: Nil, newType :: List.empty)