The BTOR2 parser in btor2tools (which seems to be the standard implementation) requires that in an init statement, the ID of the state must be higher than the ID of the initial value. Currently we don't adhere to this, so we generate BTOR2 that's not digestible by most tools.

E.g. we currently emit

hw.module @breaks(in %clk: !seq.clock, in %in: i32) {
    %c0_i32 = seq.initial() {
        %0 = hw.constant 0 : i32
        seq.yield %0 : i32
    } : () -> !seq.immutable<i32>
    %reg = seq.compreg %input, %clk initial %c0_i32 : i32
    %input = comb.add %in, %in : i32
}

as

1 sort bitvec 1
2 input 1 reset
3 state 1 reg
4 constd 1 0
5 init 1 3 4
6 constd 1 0
7 eq 1 3 6
8 not 1 7
9 bad 8
10 ite 1 2 6 6
11 next 1 3 10

and btormc throws the error btormc: parse error in 'breaking.btor2' line 5: state id must be greater than id of second operand. After this PR we generate

1 sort bitvec 1
2 input 1 reset
3 constd 1 0
4 state 1 reg
5 init 1 4 3
6 constd 1 0
7 eq 1 4 6
8 not 1 7
9 bad 8
10 ite 1 2 6 6
11 next 1 4 10

which parses fine. This breaks a couple of tests that the PR also fixes (might be worth swapping the firtool BTOR2 tests to the normal regexed format at some point to make changes like this less painful).