// Description: A module with a single 1-bit bit-vector variable. The init block sets the variable to 3, which is larger than the width of the variable. A trivial invariant about that variable and a bmc check.

module main {
    var x: bv1;

    init {
        x = 3bv1;
    }

    invariant trivial: x != 1bv1;

    control {
        bmc(1);
        check;
        print_results;
    }
}
