diff --git a/CHANGELOG b/CHANGELOG
index 659ff0bea..de26baf5b 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,5 +1,6 @@
 # EBMC 5.8
 
+* AIG/netlist engine: fix for conversion of extract bits operator
 * Verilog: semantic fix for output register ports
 * SystemVerilog: cover sequence
 * SystemVerilog: labeled immediate assert/assume/cover statements
diff --git a/regression/ebmc/smv-netlist/verilog3.desc b/regression/ebmc/smv-netlist/verilog3.desc
new file mode 100644
index 000000000..37a0b22e7
--- /dev/null
+++ b/regression/ebmc/smv-netlist/verilog3.desc
@@ -0,0 +1,5 @@
+CORE
+verilog3.sv
+--smv-netlist
+^EXIT=0$
+^SIGNAL=0$
diff --git a/regression/ebmc/smv-netlist/verilog3.sv b/regression/ebmc/smv-netlist/verilog3.sv
new file mode 100644
index 000000000..514292ca5
--- /dev/null
+++ b/regression/ebmc/smv-netlist/verilog3.sv
@@ -0,0 +1,5 @@
+module main;
+  wire [7:0] some_wire;
+  wire [31:0] something_else;
+  assign something_else = some_wire[7:1];
+endmodule
diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp
index 7f04cc306..cea043f47 100644
--- a/src/trans-netlist/trans_to_netlist.cpp
+++ b/src/trans-netlist/trans_to_netlist.cpp
@@ -594,7 +594,10 @@ void convert_trans_to_netlistt::convert_lhs_rec(
     if(!to_integer_non_constant(to_extractbits_expr(expr).index(), new_from))
     {
       boolbv_widtht boolbv_width(ns);
-      mp_integer new_to = new_from + boolbv_width(expr.type());
+      const auto width = boolbv_width(expr.type());
+      DATA_INVARIANT(
+        width != 0, "trans_to_netlist got extractbits with zero-width operand");
+      mp_integer new_to = new_from + width - 1;
 
       from = new_from.to_ulong();
       to = new_to.to_ulong();