Add basic Windows tests in CI; fix automatic Z3 executable path detec…

…tion on Windows (#211)

.github/workflows/testWin.yml

@@ -0,0 +1,35 @@
+# This workflow will install Python dependencies, run tests and lint with a single version of Python
+# For more information see: https://help.github.com/actions/language-and-framework-guides/using-python-with-github-actions
+
+name: Nagini Basic Tests Windows
+
+on: [push, pull_request, workflow_dispatch]
+
+jobs:
+  build:
+
+    runs-on: windows-latest
+    env:
+      BOOGIE_EXE: "/home/runner/.dotnet/tools/boogie"
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up Java 17
+      uses: actions/setup-java@v4.4.0
+      with:
+        java-version: 17
+        distribution: oracle
+    - name: Set up Python 3.9
+      uses: actions/setup-python@v2
+      with:
+        python-version: 3.9
+    - name: Install Boogie
+      run: |
+        dotnet tool install --global Boogie --version 2.15.9
+    - name: Install Nagini
+      run: |
+        python -m pip install --upgrade pip
+        pip install pytest
+        pip install .
+    - name: Test with pytest
+      run: |
+        pytest -v src/nagini_translation/tests.py --silicon --functional

src/nagini_translation/lib/config.py

@@ -212,12 +212,33 @@ def _get_z3_path():
     if z3_exe:
         return z3_exe
 
-    script_path = os.path.join(os.path.abspath(os.path.dirname(sys.argv[0])), 'z3')
+    script_dir = os.path.abspath(os.path.dirname(sys.argv[0]))
+    script_path = os.path.join(script_dir, 'z3')
     if os.path.exists(script_path):
         return script_path
 
-    path = os.path.join(os.path.dirname(sys.executable),
-                        'z3.exe' if sys.platform.startswith('win') else 'z3')
+    script_path = os.path.join(script_dir, 'z3.exe')
+    if os.path.exists(script_path):
+        return script_path
+
+    # On Windows, the script dir is Script, but the Z3 executable seems to be in bin.
+    python_dir = os.path.abspath(os.path.dirname(script_dir))
+    bin_dir = os.path.join(python_dir, 'bin')
+
+    bin_path = os.path.join(bin_dir, 'z3')
+    if os.path.exists(bin_path):
+        return bin_path
+
+    bin_path = os.path.join(bin_dir, 'z3.exe')
+    if os.path.exists(bin_path):
+        return bin_path
+
+
+    path = os.path.join(os.path.dirname(sys.executable), 'z3')
+    if os.path.exists(path):
+        return path
+
+    path = os.path.join(os.path.dirname(sys.executable), 'z3.exe')
     if os.path.exists(path):
         return path