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

@@ -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
 

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

regression/verilog/assignment-to-concatenation/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --bound 1
 ^EXIT=0$

regression/verilog/assignment-to-range1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --bound 1
 ^EXIT=0$

regression/verilog/bit-extract/bit-extract1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 bit-extract1.v
 --bound 1
 ^EXIT=0$

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$

regression/verilog/case/case3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 case3.v
 --module main --bound 3 --trace
 ^EXIT=10$

regression/verilog/case/case4.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 case4.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/functioncall/functioncall3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 functioncall3.v
 --module main --bound 0
 ^EXIT=0$

regression/verilog/generate/generate-for2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 generate-for2.v
 --bound 0
 ^EXIT=0$

regression/verilog/generate/generate-reg1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 generate-reg1.v
 --module main --bound 0
 ^EXIT=0$

regression/verilog/generate1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/indexed-part-select1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.sv
 --bound 1
 ^EXIT=0$

regression/verilog/modules/ports2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 ports2.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/multiple_assign1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/nondet1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 3 --trace
 ^EXIT=10$

regression/verilog/replication1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --bound 1
 ^EXIT=0$

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$