smtbmc: match on full property paths instead of just names

[georgerennie]

Fixes #296 by searching for properties by full paths parsed from the smtbmc output. This also required some changes to the formatting of the output from smtbmc to allow more unambiguous parsing, so corresponds to a matching change in yosys YosysHQ/yosys#4609 (and thus the CI will fail on this currently)

[georgerennie]

The tests are passing locally for me with a build of yosys from YosysHQ/yosys#4609, but I'm not 100% sure I have all the SMT solver etc configs installed for tests and am not running verific tests

[jix]

The tests are also passing with verific build of YosysHQ/yosys#4609 and all the solvers that ship with tabby cad in the path.

To make independent simulation of smtbmc found counterexamples work reliably, I added the ; yosys-smt2-witness metadata a while ago which is using the RTLIL hdlname attributes to be flatten-invariant, uses JSON instead of splitting on whitespace and doesn't rely on being able to match smt2 and RTLIL identifiers just by their names.

I do think we should merge this PR as an immediate fix, but I think extending the smt2 backend to also emit ; yosys-smt2-witness metadata for assertions and using that might be more robust long term.

[georgerennie]

Yeah that all makes sense, I would agree. I wonder if at somepoint it would be worth having a flag for smtbmc so that it prints lines of json with the info about properties being proven/cexs found etc instead of just printing human readable text. Would make it much easier to gather that information in a way that avoids all the corner cases with trying to parse its output.