SMV netlists: SMV identifier syntax

SMV identifiers may start with $, _, a-z, A-Z, 0-9.  In addition, #, -, and
.  are allowed as subsequent characters.

Author: kroening

regression/ebmc/smv-netlist/smv_netlist1.desc

@@ -0,0 +1,11 @@
+CORE
+smv_netlist1.v
+--smv-netlist
+^VAR Verilog\.main\.my-bit: boolean;$
+^VAR Verilog\.main\.clk: boolean;$
+^ASSIGN next\(Verilog\.main\.my-bit\):=!Verilog\.main\.my-bit;$
+^INIT !Verilog\.main\.my-bit$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/smv-netlist/smv_netlist1.v

@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg \my-bit ;
+
+  always @(posedge clk)
+    \my-bit = !\my-bit ;
+
+  initial \my-bit = 0;
+
+endmodule

src/trans-netlist/netlist.cpp

@@ -389,9 +389,14 @@ std::string netlistt::id2smv(const irep_idt &id)
 
   for(unsigned i=0; i<id.size(); i++)
   {
+    const bool first = i == 0;
     char ch=id[i];
-    if(isalnum(ch) || ch=='_' || ch=='.' || ch=='#')
+    if(
+      isalnum(ch) || ch == '_' || (ch == '.' && !first) ||
+      (ch == '#' && !first) || (ch == '-' && !first))
+    {
       result+=ch;
+    }
     else if(ch==':')
     {
       result+='.';