// Description: two modules, n and m, that have a single integer variable called x. A main module that creates an instance of the two submodules, assumes their version of x are not equal in the init and next, and then checks by induction that they are always equal.

module m {
    var x: integer;
}

module n {
    var x: integer;
}

module main {
    instance m_1: m();
    instance n_1: n();

    init {
        assume m_1.x != n_1.x;
    }

    next {
        assume m_1.x != n_1.x;
    }

    invariant aligned: m_1.x == n_1.x;

    control {
        induction;
        check;
        print_results;
    }
}
