A problem occurs when using the lec_main tool. How to use the lec_main tool correctly? Is there any example?

The cell name of the netlist generated by using rules_hdl repository cannot match the logic of the NodeToNetlistName function in lec_main. As a result, the verification fails. Because z3 ast is empty, the verification result is always equivalent.