Merge pull request #1278 from diffblue/debug-KNOWNBUG

Fix running KNOWNBUG tests

Author: kroening

.github/workflows/pull-request-checks.yaml

@@ -502,7 +502,13 @@ jobs:
           chmod a+x ./bin/ebmc ; ./bin/ebmc --version
           chmod a+x ./bin/hw-cbmc ; ./bin/hw-cbmc --version
           chmod a+x ./bin/vlindex ; ./bin/vlindex --version
-          echo "PATH=$PATH:$PWD/bin" >> $GITHUB_ENV
+      - name: Put binaries back in place
+        run: |
+          cp bin/ebmc src/ebmc/
+          cp bin/hw-cbmc src/hw-cbmc/
+          cp bin/vlindex src/vlindex/
+      - name: Run the verilog tests (CORE)
+        run: make -C regression/verilog test TEST_PL="../../lib/cbmc/regression/test.pl -C"
       - name: Run the ebmc tests with SAT
         run: make -C regression/ebmc test TEST_PL="../../lib/cbmc/regression/test.pl -K"
       - name: Run the ebmc tests with Z3

regression/verilog/modules/input_and_ansi_input.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 input_and_ansi_input.v
 
 ^EXIT=2$
 ^SIGNAL=0$
 --
 --
-The redeclaration must be errored.