smt backend option --dump-vlogtb produces Verilator error

[trayres]

Duplicate definition of genclock causes Verilator simulation failure.

It looks like this option is only used with option --dump-vlogtb of yosys-smtbmc, and the test for it is in examples/smtbmc with Makefile target demo2; but this test only runs the resulting testbench with Icarus, which appears to be more accepting of such redefinitions(?).

I think this can be greatly simplified - Verilator DOES now cover # style delays. It looks like this DUT instantiation also does not use the full compliment of inputs and outputs, and I can't determine why in one case it is a "standalone" testbench module and in the Verilator case it has inputs/outputs (genclock and clock).

If someone could point me in the right direction I'd be glad to help out with further changes. Thank you!