presburger

The decision procedure is based on the algorithm used in CVC4, which is itself based on the Omega test.