ERROR: Assert `GetSize(subexpr) == 1' failed in backends/smt2/smt2.cc:410.

[rroohhh]

When running the following yosys script

read_ilang design.il
dffunmap
stat
write_smt2 -wires design_smt2.smt2

I get the following assertion error:

ERROR: Assert `GetSize(subexpr) == 1' failed in backends/smt2/smt2.cc:410. 

I minimized my testcase to the following using bugpoint (and a manual call of opt after bugpoint was done)

# Generated by Yosys 0.9+3755 (git sha1 UNKNOWN, g++ 7.5.0 -fPIC -Os)
autoidx 3073
attribute \keep 1
attribute \nmigen.hierarchy "top.dut.last_fifo.fifo"
attribute \generator "nMigen"
module \fifo
  attribute $bugpoint 1
  wire width 3 output 1 $auto$bugpoint.cc:253:simplify_something$306
  cell $mem \storage
    parameter \ABITS 0
    parameter \INIT 3'000
    parameter \MEMID "\\storage"
    parameter \OFFSET 0
    parameter \RD_CLK_ENABLE 1'0
    parameter \RD_CLK_POLARITY 1'1
    parameter \RD_PORTS 1
    parameter \RD_TRANSPARENT 1'1
    parameter \SIZE 1
    parameter \WIDTH 3
    parameter \WR_CLK_ENABLE 1'1
    parameter \WR_CLK_POLARITY 1'1
    parameter \WR_PORTS 1
    connect \RD_ADDR { }
    connect \RD_CLK 1'x
    connect \RD_DATA $auto$bugpoint.cc:253:simplify_something$306
    connect \RD_EN 1'x
    connect \WR_ADDR { }
    connect \WR_CLK 1'x
    connect \WR_DATA 3'xxx
    connect \WR_EN 3'xxx
  end
end

Here you can find the full design aswell.

[rroohhh]

(I just checked with version 0.9+3891 aswell and this is still happening)

[rroohhh]

Ok this boils down to to the memory size being 1 and therefore the read / write address having zero bits, and get_bv does not seem to support zero width signals. I have no deeper understanding of the smt2 backend, so I am not sure where to take this from here...