presburger-arithmetic