Open
Description
When I try to divide an integer by a constant and use Yices as the solver, I get QF_NIA not supported error. However, the manual says on p. 5 that QF_NIA is indeed supported, except that "Division by a non-constant term is not supported." (p. 45).
Could it also be that PySMT only checks for DIVs, regardless of whether it is a division by constant or not? The situation might be similar for other solvers, I only have Z3 and Yices installed.
Metadata
Metadata
Assignees
Labels
No labels