java-smt
java-smt copied to clipboard
CVC4 Incomplete Integer/Numeral Formula Managers
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.
I will take a look.
As CVC4 is deprecated and CVC5 is already available and integrated, we might want to close this issue without any fix.