Merge pull request #675 from diffblue/netlist-conversion1

fix for netlist conversion

Author: kroening

regression/ebmc/netlist/netlist-conversion1.desc

@@ -0,0 +1,5 @@
+CORE
+netlist-conversion1.v
+--bound 1 --aig
+^EXIT=10$
+^SIGNAL=0$

regression/ebmc/netlist/netlist-conversion1.v

@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [0:0] q;
+
+  always @(posedge clk)
+    q[0] <= q[0];
+
+  always assert p1: q[0];
+
+endmodule

src/trans-netlist/trans_to_netlist.cpp

@@ -593,6 +593,11 @@ void convert_trans_to_netlistt::convert_lhs_rec(
   // default
   forall_operands(it, expr)
   {
+    // natural/integer-typed expressions do not contain symbols, and hence,
+    // do not need to be recursed into.
+    if(it->type().id() == ID_natural || it->type().id() == ID_integer)
+      continue;
+
     std::size_t width=boolbv_width(it->type());
 
     if(width==0)