diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index f02e22a..efd423d 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 9b8a418..8cbf7e6 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 7d43011..e1d67f8 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 80f2bf4..b140656 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 89b1dbf..0757a46 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 2308d85..4eaa396 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 472a72b..360ac88 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 ef1060a..635625e 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 6d60105..effdedb 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 168a17e..ec48292 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 60a3c80..01c703b 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 6a3d0fa..415cc5c 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 4cf9be7..8161014 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 b4938fc..2c640a8 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 6a3d0fa..415cc5c 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 c711366..c04e092 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 6951d75..de4bd11 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 b8bf0d1..f86fc8b 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$