[HWToBTOR2] Fix slice lowering argument meanings

[TaoBi22]

Seems like HWToBTOR2 currently implements the wrong semantics for slice in BTOR2 - we assume that BTOR2's slice operation takes the same arguments as our extract (the lowbit and the width) but it actually requires the upper and lower bits of the slice.

For example:

hw.module @Top() {
    %c0_i8 = hw.constant 0 : i8
    %extract = comb.extract %c0_i8 from 4 : (i8) -> i4
}

currently lowers to

1 sort bitvec 8
2 constd 1 0
3 sort bitvec 1
4 slice 3 2 0 4

which when given to Btor-mc throws

btormc: parse error in 'breaking.btor2' line 4: lower has to be less than or equal to upper

as it's expecting the 3rd argument of the slice to be the upper bit so it should be greater than the 4th.

[dobios]

Nice catch! I can't believe no one ever ran into this before ^^"