Merge pull request #1356 from diffblue/verilog2-fix

netlist: fix off-by-one bug

Author: kroening

regression/ebmc/smv-netlist/verilog2.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 verilog2.sv
 --smv-netlist
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This throws an error.

src/trans-netlist/trans_to_netlist.cpp

@@ -722,7 +722,7 @@ void convert_trans_to_netlistt::add_equality_rec(
 
     bv_varidt bv_varid;
     bv_varid.id=lhs.get(ID_identifier);
-    
+
     for(bv_varid.bit_nr=lhs_from;
         bv_varid.bit_nr!=(lhs_to+1);
         bv_varid.bit_nr++)
@@ -770,9 +770,12 @@ void convert_trans_to_netlistt::add_equality_rec(
 
     boolbv_widtht boolbv_width(ns);
 
+    const auto width = boolbv_width(lhs.type());
+
+    DATA_INVARIANT(width != 0, "add_equality_rec got zero-width bit-vector");
+
     std::size_t new_lhs_from = lhs_from + index.to_ulong();
-    std::size_t new_lhs_to =
-      lhs_from + index.to_ulong() + boolbv_width(lhs.type());
+    std::size_t new_lhs_to = lhs_from + index.to_ulong() + width - 1;
 
     add_equality_rec(
       src, to_extractbits_expr(lhs).src(), new_lhs_from, new_lhs_to, rhs_entry);