search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
186 stars 46 forks source link

CVC4 Incomplete Integer/Numeral Formula Managers #304

Open baierd opened 1 year ago

baierd commented 1 year ago

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.

RSoegtrop commented 1 year ago

I will take a look.

kfriedberger commented 11 months ago

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