Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-01-20 | SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787) | Aina Niemetz | |
This enables more strict handling of operators div, mod and abs for Integer arithmetic logics. More strict handling for '/' for Real arithmetic logics is more involved and should be done in the parser -- instead at solving time, like is currently done for checking that the application * is in the linear fragment. The latter should be checked in the parser, too. This is postponed to a later PR. | |||
2019-10-13 | Eliminate negative constant coefficients in div/mod (#2929) | Andrew Reynolds | |
Fixes #1399. |