From de67aafea93f49acd43f1bf686cfd3a77adc823a Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 3 Feb 2024 08:22:27 -0800
Subject: [PATCH 1/2] CI: run the Verilog tests with Z3

This exercises additonal functionality of the solver backend, and is hence
worth running in CI.
---
 .github/workflows/pull-request-checks.yaml                 | 4 ++++
 regression/verilog/Makefile                                | 7 ++++++-
 regression/verilog/assignment-to-concatenation/test.desc   | 2 +-
 regression/verilog/assignment-to-range1/test.desc          | 2 +-
 regression/verilog/bit-extract/bit-extract1.desc           | 2 +-
 regression/verilog/bit-extract/bit-extract2.desc           | 2 +-
 regression/verilog/case/case3.desc                         | 2 +-
 regression/verilog/case/case4.desc                         | 2 +-
 regression/verilog/functioncall/functioncall3.desc         | 2 +-
 regression/verilog/generate/generate-for2.desc             | 2 +-
 regression/verilog/generate/generate-reg1.desc             | 2 +-
 regression/verilog/generate1/test.desc                     | 2 +-
 regression/verilog/indexed-part-select1/test.desc          | 2 +-
 regression/verilog/modules/ports2.desc                     | 2 +-
 regression/verilog/multiple_assign1/test.desc              | 2 +-
 regression/verilog/nondet1/test.desc                       | 2 +-
 regression/verilog/replication1/test.desc                  | 2 +-
 .../system_verilog_assertion3.desc                         | 2 +-
 18 files changed, 26 insertions(+), 17 deletions(-)

diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index f02e22a4e..efd423d65 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.github/workflows/pull-request-checks.yaml
@@ -49,6 +49,8 @@ jobs:
         run: make -C regression/ebmc test-z3
       - name: Run the verilog tests
         run: make -C regression/verilog test
+      - name: Run the verilog tests with Z3
+        run: make -C regression/verilog test-z3
       - name: Print ccache stats
         run: ccache -s
 
@@ -100,6 +102,8 @@ jobs:
         run: make -C regression/ebmc test-z3
       - name: Run the verilog tests
         run: make -C regression/verilog test
+      - name: Run the verilog tests with Z3
+        run: make -C regression/verilog test-z3
       - name: Print ccache stats
         run: ccache -s
 
diff --git a/regression/verilog/Makefile b/regression/verilog/Makefile
index 9b8a418a4..8cbf7e641 100644
--- a/regression/verilog/Makefile
+++ b/regression/verilog/Makefile
@@ -1,4 +1,9 @@
 default: test
 
+TEST_PL = ../../lib/cbmc/regression/test.pl
+
 test:
-	@../../lib/cbmc/regression/test.pl -c ../../../src/ebmc/ebmc
+	@$(TEST_PL) -c ../../../src/ebmc/ebmc
+
+test-z3:
+	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend
diff --git a/regression/verilog/assignment-to-concatenation/test.desc b/regression/verilog/assignment-to-concatenation/test.desc
index 7d430115f..e1d67f822 100644
--- a/regression/verilog/assignment-to-concatenation/test.desc
+++ b/regression/verilog/assignment-to-concatenation/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/assignment-to-range1/test.desc b/regression/verilog/assignment-to-range1/test.desc
index 80f2bf465..b14065602 100644
--- a/regression/verilog/assignment-to-range1/test.desc
+++ b/regression/verilog/assignment-to-range1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/bit-extract/bit-extract1.desc b/regression/verilog/bit-extract/bit-extract1.desc
index 89b1dbf3c..0757a46b0 100644
--- a/regression/verilog/bit-extract/bit-extract1.desc
+++ b/regression/verilog/bit-extract/bit-extract1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 bit-extract1.v
 --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/bit-extract/bit-extract2.desc b/regression/verilog/bit-extract/bit-extract2.desc
index 2308d8508..4eaa39621 100644
--- a/regression/verilog/bit-extract/bit-extract2.desc
+++ b/regression/verilog/bit-extract/bit-extract2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 bit-extract2.v
 --module main --bound 1 --trace
 ^EXIT=10$
diff --git a/regression/verilog/case/case3.desc b/regression/verilog/case/case3.desc
index 472a72b12..360ac8899 100644
--- a/regression/verilog/case/case3.desc
+++ b/regression/verilog/case/case3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 case3.v
 --module main --bound 3 --trace
 ^EXIT=10$
diff --git a/regression/verilog/case/case4.desc b/regression/verilog/case/case4.desc
index ef1060a3b..635625e78 100644
--- a/regression/verilog/case/case4.desc
+++ b/regression/verilog/case/case4.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 case4.v
 --module main --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/functioncall/functioncall3.desc b/regression/verilog/functioncall/functioncall3.desc
index 6d6010571..effdedbf2 100644
--- a/regression/verilog/functioncall/functioncall3.desc
+++ b/regression/verilog/functioncall/functioncall3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 functioncall3.v
 --module main --bound 0
 ^EXIT=0$
diff --git a/regression/verilog/generate/generate-for2.desc b/regression/verilog/generate/generate-for2.desc
index 168a17e6e..ec4829241 100644
--- a/regression/verilog/generate/generate-for2.desc
+++ b/regression/verilog/generate/generate-for2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 generate-for2.v
 --bound 0
 ^EXIT=0$
diff --git a/regression/verilog/generate/generate-reg1.desc b/regression/verilog/generate/generate-reg1.desc
index 60a3c80a2..01c703bc9 100644
--- a/regression/verilog/generate/generate-reg1.desc
+++ b/regression/verilog/generate/generate-reg1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 generate-reg1.v
 --module main --bound 0
 ^EXIT=0$
diff --git a/regression/verilog/generate1/test.desc b/regression/verilog/generate1/test.desc
index 6a3d0fa20..415cc5c10 100644
--- a/regression/verilog/generate1/test.desc
+++ b/regression/verilog/generate1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/indexed-part-select1/test.desc b/regression/verilog/indexed-part-select1/test.desc
index 4cf9be71f..8161014e3 100644
--- a/regression/verilog/indexed-part-select1/test.desc
+++ b/regression/verilog/indexed-part-select1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.sv
 --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/modules/ports2.desc b/regression/verilog/modules/ports2.desc
index b4938fc43..2c640a8a2 100644
--- a/regression/verilog/modules/ports2.desc
+++ b/regression/verilog/modules/ports2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 ports2.v
 --module main --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/multiple_assign1/test.desc b/regression/verilog/multiple_assign1/test.desc
index 6a3d0fa20..415cc5c10 100644
--- a/regression/verilog/multiple_assign1/test.desc
+++ b/regression/verilog/multiple_assign1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/nondet1/test.desc b/regression/verilog/nondet1/test.desc
index c71136658..c04e092d8 100644
--- a/regression/verilog/nondet1/test.desc
+++ b/regression/verilog/nondet1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 3 --trace
 ^EXIT=10$
diff --git a/regression/verilog/replication1/test.desc b/regression/verilog/replication1/test.desc
index 6951d7524..de4bd11c2 100644
--- a/regression/verilog/replication1/test.desc
+++ b/regression/verilog/replication1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/system_verilog_assertion/system_verilog_assertion3.desc b/regression/verilog/system_verilog_assertion/system_verilog_assertion3.desc
index b8bf0d16b..f86fc8b84 100644
--- a/regression/verilog/system_verilog_assertion/system_verilog_assertion3.desc
+++ b/regression/verilog/system_verilog_assertion/system_verilog_assertion3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 system_verilog_assertion3.sv
 --module main --bound 1
 ^EXIT=0$

From ac27405ae94d3d9b84c7190a553b4162e2b8cbd4 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 3 Feb 2024 08:23:42 -0800
Subject: [PATCH 2/2] Verilog: replication count may be zero

The SystemVerilog 1800-2017 standard explicitly allows replications with
count zero.
---
 .../test.desc => replication/replication1.desc}        |  4 ++--
 .../main.v => replication/replication1.v}              |  6 +++++-
 src/verilog/verilog_typecheck_expr.cpp                 | 10 +++-------
 3 files changed, 10 insertions(+), 10 deletions(-)
 rename regression/verilog/{replication1/test.desc => replication/replication1.desc} (72%)
 rename regression/verilog/{replication1/main.v => replication/replication1.v} (81%)

diff --git a/regression/verilog/replication1/test.desc b/regression/verilog/replication/replication1.desc
similarity index 72%
rename from regression/verilog/replication1/test.desc
rename to regression/verilog/replication/replication1.desc
index de4bd11c2..364027370 100644
--- a/regression/verilog/replication1/test.desc
+++ b/regression/verilog/replication/replication1.desc
@@ -1,6 +1,6 @@
 CORE broken-smt-backend
-main.v
---bound 1
+replication1.v
+--bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/replication1/main.v b/regression/verilog/replication/replication1.v
similarity index 81%
rename from regression/verilog/replication1/main.v
rename to regression/verilog/replication/replication1.v
index c9e4189a6..bef4a48d5 100644
--- a/regression/verilog/replication1/main.v
+++ b/regression/verilog/replication/replication1.v
@@ -13,8 +13,12 @@ module main(in);
   always assert property2:
     {{ 1 { in }}, in } == { in, in };
 
-  // replication of something boolean
+  // 0-replication
   always assert property3:
+    {{ 0 { in }}, in } == { in };
+
+  // replication of something boolean
+  always assert property4:
     {{ 1 { 1'b0 }}, in } == in;
 
 endmodule
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 8d8622d0c..fc965739e 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -1911,7 +1911,7 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
   if(op1.type().id()==ID_bool)
     op1 = typecast_exprt{op1, unsignedbv_typet{1}};
 
-  unsigned width=get_width(expr.op1().type());
+  auto width = get_width(expr.op1().type());
 
   mp_integer op0 = convert_integer_constant_expression(expr.op0());
 
@@ -1921,12 +1921,8 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
       << "number of replications must not be negative";
   }
 
-  if(op0==0)
-  {
-    // ruled out by IEEE 1364-2001
-    throw errort().with_location(expr.source_location())
-      << "number of replications must not be zero";
-  }
+  // IEEE 1800-2017 explicitly allows replication with
+  // count zero.
 
   {
     expr.op0()=from_integer(op0, natural_typet());