diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 5112d9e0..b262f905 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -59,8 +59,7 @@ jobs:
         run: |
           brew install python@${{ matrix.py-version }}
           echo "${{ matrix.brew }}/opt/python@${{ matrix.py-version }}/libexec/bin" >> $GITHUB_PATH
-          curl https://bootstrap.pypa.io/get-pip.py -o get-pip.py
-          python${{ matrix.py-version }} get-pip.py
+          python${{ matrix.py-version }} -m ensurepip
       - name: Install dependencies
         run: |
           python -m pip install --upgrade pip
diff --git a/.gitignore b/.gitignore
index 7d637c18..938b91f0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,5 +16,3 @@ dist
 # OSX / VSCode ignores
 .DS_Store
 .idea
-
-*directories
diff --git a/requirements.txt b/requirements.txt
index 2a6d4f7e..55def475 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -3,4 +3,4 @@ pylint>=2.17
 coverage>=7.2
 sphinx>=7.0
 pyvcg==1.0.6
-cvc5
+cvc5>=1.1.1; sys.platform == "linux" or sys.platform == "darwin"
diff --git a/tests-system/lint-ug-examples/div_by_zero.rsl b/tests-system/lint-ug-examples/div_by_zero.rsl
deleted file mode 100644
index 960d84c3..00000000
--- a/tests-system/lint-ug-examples/div_by_zero.rsl
+++ /dev/null
@@ -1,13 +0,0 @@
-package Div_By_Zero
-
-type T {
-  x Integer
-  y Integer
-}
-
-checks T {
-  x > 2, fatal "x too small"
-  y > 2, fatal "y too small"
-
-  100 / (111 - x * y) > 0, "example"
-}
diff --git a/tests-system/lint-ug-examples/output b/tests-system/lint-ug-examples/output
index c909f055..bfcc389a 100644
--- a/tests-system/lint-ug-examples/output
+++ b/tests-system/lint-ug-examples/output
@@ -13,13 +13,6 @@ len(x) >= 3 implies x[3] > 0, "too small"
                      |   T bad_potato {
                      |     x = [1, 1, 1]
                      |   }
-100 / (111 - x * y) > 0, "example"
-    ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero]
-    | example record_type triggering error:
-    |   T bad_potato {
-    |     x = 3
-    |     y = 37
-    |   }
 len(description) >= 10, "too short"
     ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null]
               | example record_type triggering error:
@@ -44,4 +37,4 @@ y Integer [0 .. 1]
                 | be an optional Integer instead.
 abstract type T {
               ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types]
-Processed 14 models, 0 checks and 0 requirement files and found 12 warnings
+Processed 13 models, 0 checks and 0 requirement files and found 11 warnings
diff --git a/tests-system/lint-ug-examples/output.json b/tests-system/lint-ug-examples/output.json
index 32da48be..88569d50 100644
--- a/tests-system/lint-ug-examples/output.json
+++ b/tests-system/lint-ug-examples/output.json
@@ -1,2 +1,2 @@
 {}
-Processed 14 models, 0 checks and 0 requirement files and found no issues
+Processed 13 models, 0 checks and 0 requirement files and found no issues
diff --git a/tests-system/lint-ug-examples/output.smtlib b/tests-system/lint-ug-examples/output.smtlib
index c909f055..bfcc389a 100644
--- a/tests-system/lint-ug-examples/output.smtlib
+++ b/tests-system/lint-ug-examples/output.smtlib
@@ -13,13 +13,6 @@ len(x) >= 3 implies x[3] > 0, "too small"
                      |   T bad_potato {
                      |     x = [1, 1, 1]
                      |   }
-100 / (111 - x * y) > 0, "example"
-    ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero]
-    | example record_type triggering error:
-    |   T bad_potato {
-    |     x = 3
-    |     y = 37
-    |   }
 len(description) >= 10, "too short"
     ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null]
               | example record_type triggering error:
@@ -44,4 +37,4 @@ y Integer [0 .. 1]
                 | be an optional Integer instead.
 abstract type T {
               ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types]
-Processed 14 models, 0 checks and 0 requirement files and found 12 warnings
+Processed 13 models, 0 checks and 0 requirement files and found 11 warnings
diff --git a/util/check_local_modifications.sh b/util/check_local_modifications.sh
index 433c0faa..e227600a 100755
--- a/util/check_local_modifications.sh
+++ b/util/check_local_modifications.sh
@@ -5,7 +5,7 @@ if [[ $(git status -s) ]]; then
     git -P diff
     echo "Summary:"
     git status -s
-    exit 0
+    exit 1
 else
     exit 0
 fi