Skip to content

added fof formula printing, fixed smtlib declare sort bug, theory fla… #27

added fof formula printing, fixed smtlib declare sort bug, theory fla…

added fof formula printing, fixed smtlib declare sort bug, theory fla… #27

Triggered via push September 27, 2024 01:03
Status Failure
Total duration 2m 34s
Artifacts
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

33 errors and 3 warnings
build (3.9)
Process completed with exit code 1.
Ruff (F403): kdrag/smt.py#L15
kdrag/smt.py:15:5: F403 `from z3 import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L17
kdrag/smt.py:17:16: F405 `Solver` may be undefined, or defined from star imports
Ruff (F403): kdrag/smt.py#L19
kdrag/smt.py:19:5: F403 `from z3 import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L22
kdrag/smt.py:22:16: F405 `Solver` may be undefined, or defined from star imports
Ruff (F403): kdrag/smt.py#L28
kdrag/smt.py:28:5: F403 `from cvc5.pythonic import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L31
kdrag/smt.py:31:16: F405 `FuncDeclRef` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L45
kdrag/smt.py:45:17: F405 `Bool` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L47
kdrag/smt.py:47:29: F405 `Implies` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L55
kdrag/smt.py:55:29: F405 `DatatypeSortRef` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L56
kdrag/smt.py:56:17: F405 `DatatypeRef` may be undefined, or defined from star imports
Ruff (F403): kdrag/smt.py#L15
kdrag/smt.py:15:5: F403 `from z3 import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L17
kdrag/smt.py:17:16: F405 `Solver` may be undefined, or defined from star imports
Ruff (F403): kdrag/smt.py#L19
kdrag/smt.py:19:5: F403 `from z3 import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L22
kdrag/smt.py:22:16: F405 `Solver` may be undefined, or defined from star imports
Ruff (F403): kdrag/smt.py#L28
kdrag/smt.py:28:5: F403 `from cvc5.pythonic import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L31
kdrag/smt.py:31:16: F405 `FuncDeclRef` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L45
kdrag/smt.py:45:17: F405 `Bool` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L47
kdrag/smt.py:47:29: F405 `Implies` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L55
kdrag/smt.py:55:29: F405 `DatatypeSortRef` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L56
kdrag/smt.py:56:17: F405 `DatatypeRef` may be undefined, or defined from star imports
build (3.11)
Process completed with exit code 1.
build (3.10)
Process completed with exit code 1.
Ruff (F403): kdrag/smt.py#L15
kdrag/smt.py:15:5: F403 `from z3 import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L17
kdrag/smt.py:17:16: F405 `Solver` may be undefined, or defined from star imports
Ruff (F403): kdrag/smt.py#L19
kdrag/smt.py:19:5: F403 `from z3 import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L22
kdrag/smt.py:22:16: F405 `Solver` may be undefined, or defined from star imports
Ruff (F403): kdrag/smt.py#L28
kdrag/smt.py:28:5: F403 `from cvc5.pythonic import *` used; unable to detect undefined names
Ruff (F405): kdrag/smt.py#L31
kdrag/smt.py:31:16: F405 `FuncDeclRef` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L45
kdrag/smt.py:45:17: F405 `Bool` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L47
kdrag/smt.py:47:29: F405 `Implies` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L55
kdrag/smt.py:55:29: F405 `DatatypeSortRef` may be undefined, or defined from star imports
Ruff (F405): kdrag/smt.py#L56
kdrag/smt.py:56:17: F405 `DatatypeRef` may be undefined, or defined from star imports
build (3.9)
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/setup-python@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
build (3.11)
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/setup-python@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
build (3.10)
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/setup-python@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/