Skip to content

ADT is facing some canonicalization issue during module instantiation #248

@adwait

Description

@adwait

The following code (using SMTLIB2Interface):

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.

Metadata

Metadata

Labels

bugSomething isn't working

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions