Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

CVC4 Incomplete Integer/Numeral Formula Managers #304

Open
baierd opened this issue May 11, 2023 · 2 comments
Open

CVC4 Incomplete Integer/Numeral Formula Managers #304

baierd opened this issue May 11, 2023 · 2 comments
Assignees
@baierd @RSoegtrop
Labels
bug

Comments

@baierd
Copy link
Collaborator

baierd commented May 11, 2023

The FormulaManagers for Integers, and possibly Rationals, are incomplete in CVC4. They do not support multiplication for example. However, CVC4 supports these operations.
We need to analyze which operations are missing in these two, and possibly all FormulaManagers and add them. Also we need to make sure that we enable the tests for these cases.
@baierd baierd added the bug label May 11, 2023
@baierd baierd self-assigned this May 11, 2023
@RSoegtrop
Copy link
Contributor

I will take a look.

@kfriedberger
Copy link
Member

As CVC4 is deprecated and CVC5 is already available and integrated, we might want to close this issue without any fix.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@baierd baierd

@RSoegtrop RSoegtrop

Labels
bug
Milestone
No milestone
Development

No branches or pull requests
3 participants
@baierd @kfriedberger @RSoegtrop