You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
module main {
datatype t = B(f: t) | A();
var a : t;
init {
havoc a;
if (is_A(a)) { } else {
if (is_B(a)) { }
else {
assert (false);
}
}
}
next {
havoc a;
if (is_A(a)) { } else {
if (is_B(a) && is_A(a.f)) { }
else {
assert (false);
}
}
}
control {
v = induction;
print_module;
check;
print_results;
v.print_cex ();
}
}
results in an instantiated module with the following lang.DataType:
type t = t = | (B,List((_rec_f,t = | (B,List((_rec_f,t))) | (A,List())))) | (A,List()); // test.ucl
Rather, it should have been:
type t = t = | (B,List((_rec_f,t = (self) t))) | (A,List()); // test.ucl
using the SelfReference type at the second level (instead of the third).
This is even before lang-to-SMT conversion. It breaks downstream fixes (#243,#247) in generateDatatype as the ADT leads to two SMT declare-datatype commands.
The text was updated successfully, but these errors were encountered:
The following code (using SMTLIB2Interface):
results in an instantiated module with the following lang.DataType:
Rather, it should have been:
using the
SelfReference
type at the second level (instead of the third).This is even before lang-to-SMT conversion. It breaks downstream fixes (#243,#247) in
generateDatatype
as the ADT leads to two SMTdeclare-datatype
commands.The text was updated successfully, but these errors were encountered: