Merge

.github/workflows/test.yml

@@ -28,4 +28,4 @@ jobs:
         pip install .
     - name: Test with pytest
       run: |
-        pytest -v -p no:faulthandler src/nagini_translation/tests.py --silicon --carbon
+        pytest -v src/nagini_translation/tests.py --silicon --carbon

.github/workflows/testWin.yml

@@ -0,0 +1,36 @@
+# 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/[email protected]
+      with:
+        java-version: 17
+        distribution: oracle
+    - name: Set up Python 3.12
+      uses: actions/setup-python@v2
+      with:
+        python-version: "3.12"
+        architecture: "x64"
+    - 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

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.12 (64 bit, other versions likely *will not work*) and the required libraries (python3.12-dev).
-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.12 (64 bit, other versions likely *will not work*) and the required libraries
+(in particular, python3.12-dev). For usage with Viper's verification condition generation backend Carbon, you will also need
+to install Boogie (version 2.15.9).
 
 Dependencies (Windows)
 ==========================

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