// Description: A module with a bitvector variable. The init block assigns the value 1000 to the variable, and then asserts that the variable is not equal to that value. Bounded model checking is used to check the assertion fails

module main {
    var test1 : bv64;

    init {
        test1 = 1000bv64;
        assert (test1 != 1000bv64);
    }

    next {

    }

    control {
        f = bmc(2);
        check;
        f.print_cex();
        print_results;
    }
}
