From 1ccced9f0b62867931f6df0751e41b352743bb79 Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Wed, 16 Oct 2024 16:25:24 +0200
Subject: [PATCH 1/2] Update README.rst

---
 README.rst | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/README.rst b/README.rst
index 6e1e216d..4e9dde53 100644
--- a/README.rst
+++ b/README.rst
@@ -6,8 +6,9 @@ Our CAV 2018 tool paper describing Nagini can be found `here <http://pm.inf.ethz
 Dependencies (Ubuntu Linux)
 ===================================
 
-Install Java 11 or newer (64 bit) and Python 3.9 (64 bit, other versions likely *will not work*) and the required libraries.
-For usage with Viper's verification condition generation backend Carbon, you will also need to install Boogie (version 2.15.9).
+Install Java 11 or newer (64 bit) and Python 3.9 (64 bit, other versions likely *will not work*) and the required libraries
+(in particular, python3.9-dev). For usage with Viper's verification condition generation backend Carbon, you will also need 
+to install Boogie (version 2.15.9).
 
 Dependencies (Windows)
 ==========================
@@ -26,7 +27,7 @@ Execute the following commands (on Windows, you may have to use ``cmd`` and not
 
 1.  Create a virtual environment::
 
-        virtualenv --python=python3 <env>
+        virtualenv --python=python3.9 <env>
         
 2.  Activate it::
 

From 3c3d89b753c62c10c0532070d461fd6069297ca5 Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Thu, 24 Oct 2024 12:24:10 +0200
Subject: [PATCH 2/2] Add basic Windows tests in CI; fix automatic Z3
 executable path detection on Windows (#211)

---
 .github/workflows/testWin.yml        | 35 ++++++++++++++++++++++++++++
 src/nagini_translation/lib/config.py | 27 ++++++++++++++++++---
 2 files changed, 59 insertions(+), 3 deletions(-)
 create mode 100644 .github/workflows/testWin.yml

diff --git a/.github/workflows/testWin.yml b/.github/workflows/testWin.yml
new file mode 100644
index 00000000..379bea76
--- /dev/null
+++ b/.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
diff --git a/src/nagini_translation/lib/config.py b/src/nagini_translation/lib/config.py
index e6d3efa2..3c4a1330 100644
--- a/src/nagini_translation/lib/config.py
+++ b/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