Verilog: fix for bit select on boolean argument

regression/verilog/expressions/index-constant1.desc

@@ -0,0 +1,8 @@
+CORE
+index-constant1.sv
+
+^\[.*\] .* PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/index-constant1.sv

@@ -0,0 +1,11 @@
+module main;
+
+  // index expressions yield constants
+  parameter p = 'b1010;
+  parameter q = p[3];
+  parameter r = p[0];
+
+  assert final (q == 1);
+  assert final (r == 0);
+
+endmodule

regression/verilog/expressions/index-constant2.desc

@@ -0,0 +1,8 @@
+CORE
+index-constant2.sv
+
+^\[.*\] .* PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/index-constant2.sv

@@ -0,0 +1,9 @@
+module main;
+
+  // index expressions yield constants
+  parameter p = (1>0); // boolean
+  parameter q = p[0];
+
+  assert final (q == 1);
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -2738,6 +2738,9 @@ exprt verilog_typecheck_exprt::convert_bit_select_expr(binary_exprt expr)
   }
   else
   {
+    // extractbit works on bit vectors only
+    no_bool_ops(expr);
+
     auto width = get_width(op0.type());
     auto offset = op0.type().get_int(ID_C_offset);