Add Windows/Visual Studio CI job

This adds a Windows 2022 Visual Studio CI job.

Author: kroening

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

@@ -264,3 +264,61 @@ jobs:
         run: node --no-experimental-fetch src/ebmc/ebmc.js --version
       - name: Print ccache stats
         run: ccache -s
+
+  check-vs-2022-make-build-and-test:
+    runs-on: windows-2022
+    env:
+      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Setup MSBuild
+        uses: microsoft/setup-msbuild@v2
+      - name: Fetch dependencies
+        run: |
+          choco install -y --no-progress winflexbison3 strawberryperl wget
+          if($LastExitCode -ne 0)
+          {
+            Write-Output "::error ::Dependency installation via Chocolatey failed."
+            exit $LastExitCode
+          }
+          nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
+          echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
+          echo "c:\Strawberry\" >> $env:GITHUB_PATH
+          Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip
+          Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools
+          echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH
+          New-Item -ItemType directory "C:\tools\parallel"
+          wget.exe -O c:\tools\parallel\parallel https://git.savannah.gnu.org/cgit/parallel.git/plain/src/parallel
+          echo "c:\tools\parallel" >> $env:GITHUB_PATH
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Initialise Developer Command Line
+        uses: ilammy/msvc-dev-cmd@v1
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          save-always: true
+          path: .ccache
+          key: ${{ runner.os }}-msbuild-make-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-msbuild-make-${{ github.ref }}
+            ${{ runner.os }}-msbuild-make
+      - name: ccache environment
+        run: |
+          echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
+          echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
+      - name: Zero ccache stats and limit in size (2 GB)
+        run: |
+          clcache -z
+          clcache -M 2147483648
+      - name: Download minisat with make
+        run: make -C lib/cbmc/src minisat2-download
+      - name: Build EBMC with make
+        env:
+          # disable MSYS file-name mangling
+          MSYS2_ARG_CONV_EXCL: "*"
+        run: make CXX=clcache BUILD_ENV=MSVC -j4 -C src
+      - name: Print ccache stats
+        run: clcache -s

regression/ebmc/example1/test.desc

@@ -4,4 +4,3 @@ example1.sv
 PROVED up to bound 10$
 ^EXIT=0$
 ^SIGNAL=0$
-

regression/ebmc/example3/test.desc

@@ -5,4 +5,3 @@ example3.sv
 ^\[counter\.assert\.2\] .* REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
-

regression/ebmc/example4_reset/test.desc

@@ -5,4 +5,3 @@ example4.sv
 ^\[counter\.assert\.2\] .* PROVED up to bound 10$
 ^EXIT=0$
 ^SIGNAL=0$
-

regression/ebmc/example4_trace/test.desc

@@ -6,4 +6,3 @@ example4.sv
 ^  counter\.state = 254 \(11111110\)$
 ^EXIT=10$
 ^SIGNAL=0$
-

regression/ebmc/example5/test.desc

@@ -4,4 +4,3 @@ example5.sv
 PROVED up to bound 10$
 ^EXIT=0$
 ^SIGNAL=0$
-

regression/ebmc/netlist/netlist-trace1.desc

@@ -5,4 +5,3 @@ netlist-trace1.sv
 ^  counter\.state = 3 \(00000011\)$
 ^EXIT=10$
 ^SIGNAL=0$
-

regression/ebmc/ring_buffer_bdd/test.desc

@@ -4,4 +4,3 @@ ring_buffer.sv
 PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
-

regression/ebmc/ring_buffer_induction/test.desc

@@ -6,4 +6,3 @@ ring_buffer.sv
 ^\[ring_buffer\.assert\.3\] always \(ring_buffer\.writeptr - ring_buffer\.readptr & 15\) == ring_buffer\.count: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
-

regression/verilog/Array1/test.desc

@@ -3,4 +3,3 @@ main.sv
 --module top --bound 1
 ^EXIT=0$
 ^SIGNAL=0$
-