Pono outputs longer than expected witness

[Gallagator]

I have the following chisel code

class DivisionByZeroIsEq(to: Int) extends Module {
  val a = IO(Input(UInt(2.W)))
  val b = IO(Input(UInt(2.W)))
  val d = a / b
  assume(b === 0.U)
  assert(d === to.U)
}

Which compiles to the following btor2 output:

1 sort bitvec 1
2 input 1 reset
3 sort bitvec 2
4 input 3 a ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 61:13]
5 input 3 b ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 62:13]
6 input 3 d_invalid ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
; _resetCount.init
7 zero 1
8 state 1 _resetCount
9 init 1 8 7
10 zero 3
11 eq 1 5 10 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
12 udiv 3 4 5
13 ite 3 11 6 12 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
14 zero 1
15 uext 3 14 1
16 eq 1 5 15 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:12]
17 not 1 2 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
18 not 1 16 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
19 zero 1
20 uext 3 19 1
21 eq 1 13 20 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:12]
22 not 1 21 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:9]
23 one 1
24 ugte 1 8 23
25 not 1 24
26 implies 1 17 16
27 constraint 26 ; assume @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
28 implies 1 17 21
29 not 1 28
30 bad 29 ; assert @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:9]
31 implies 1 25 2
32 constraint 31 ; _resetActive
; _resetCount.next
33 uext 3 8 1
34 one 1
35 uext 3 34 1
36 add 3 33 35
37 slice 1 36 0 0
38 ite 1 25 37 8
39 next 1 8 38

The output of pono gives a witness of length 2:

$ pono -e bmc -k 2 --vcd ignore.vcd DivisionByZeroIsEq.btor
sat
b0
#0
0 0 _resetCount@0
@0
0 1 reset@0
1 00 a@0
2 00 b@0
3 00 d_invalid@0
@1
0 0 reset@1
1 11 a@1
2 00 b@1
3 10 d_invalid@1
@2
0 1 reset@2
1 00 a@2
2 00 b@2
3 00 d_invalid@2
.

Whereas btormc takes only a single step:

$ btormc --kmax 1 DivisionByZeroIsEq.btor 
b0
@0
0 1 reset@0
1 00 a@0
2 00 b@0
3 00 d_invalid@0
@1
0 0 reset@1
1 00 a@1
2 00 b@1
3 10 d_invalid@1
.

Pono really should be failing the bounded model check in a single step.

[CyanoKobalamyne]

This should be fixed now, but please let us know if the issue persists.