From 7af771f8571ab5046969d3dd7977b2b68f6b3696 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 1 Sep 2025 09:40:35 -0700
Subject: [PATCH 1/2] Verilog: Tests for constant folding of index expressions

---
 regression/verilog/expressions/index-constant1.desc |  8 ++++++++
 regression/verilog/expressions/index-constant1.sv   | 11 +++++++++++
 regression/verilog/expressions/index-constant2.desc |  8 ++++++++
 regression/verilog/expressions/index-constant2.sv   |  9 +++++++++
 4 files changed, 36 insertions(+)
 create mode 100644 regression/verilog/expressions/index-constant1.desc
 create mode 100644 regression/verilog/expressions/index-constant1.sv
 create mode 100644 regression/verilog/expressions/index-constant2.desc
 create mode 100644 regression/verilog/expressions/index-constant2.sv

diff --git a/regression/verilog/expressions/index-constant1.desc b/regression/verilog/expressions/index-constant1.desc
new file mode 100644
index 000000000..69a8d73a7
--- /dev/null
+++ b/regression/verilog/expressions/index-constant1.desc
@@ -0,0 +1,8 @@
+CORE
+index-constant1.sv
+
+^\[.*\] .* PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/expressions/index-constant1.sv b/regression/verilog/expressions/index-constant1.sv
new file mode 100644
index 000000000..5e3ba0603
--- /dev/null
+++ b/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
diff --git a/regression/verilog/expressions/index-constant2.desc b/regression/verilog/expressions/index-constant2.desc
new file mode 100644
index 000000000..e7e8b3898
--- /dev/null
+++ b/regression/verilog/expressions/index-constant2.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+index-constant2.sv
+
+^\[.*\] .* PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/expressions/index-constant2.sv b/regression/verilog/expressions/index-constant2.sv
new file mode 100644
index 000000000..e69eff5c8
--- /dev/null
+++ b/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

From 604eebd6843fea745c7d1488ce638d0d51c5a10d Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 2 Sep 2025 15:55:43 -0700
Subject: [PATCH 2/2] Verilog: fix for bit select on boolean argument

Our extractbit IR expression requires a bit-vector argument.  This change
converts booleans to bit-vectors when used as vector argument for a Verilog
bit select expression.
---
 regression/verilog/expressions/index-constant2.desc | 2 +-
 src/verilog/verilog_typecheck_expr.cpp              | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/regression/verilog/expressions/index-constant2.desc b/regression/verilog/expressions/index-constant2.desc
index e7e8b3898..6728da1da 100644
--- a/regression/verilog/expressions/index-constant2.desc
+++ b/regression/verilog/expressions/index-constant2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 index-constant2.sv
 
 ^\[.*\] .* PROVED .*$
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index a57aaf355..8973881e0 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/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);