`generateDatatype` does not generate inner types for ADTs
Closed this issue · 0 comments
adwait commented
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:
uclid/src/main/scala/uclid/smt/SMTLIB2Interface.scala
Lines 143 to 145 in d0f0c10