// Purpose: tests that bitvectors must be the same width when compared in a procedure
// Description: A module with no variables that just tries to compare two literal bitvectors of different widths inside of a procedure
// Expectation: UCLID5 should report an error saying that the bitvectors are different widths
// Validation: removing the UCLID5 checks for bitvector widths should result in an error at the solver side.

module main {
    procedure bad_widths() {
        assert 1bv8 == 1bv16;
    }
}
