removes div_by_zero test

.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

.gitignore

@@ -16,5 +16,3 @@ dist
 # OSX / VSCode ignores
 .DS_Store
 .idea
-
-*directories

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"

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

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

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

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