In this paper , we study monadic decomposability of integer linear arithmetic in the setting of SMT .
We show that this decision problem is coNP - complete
In this paper , we study monadic decomposability of integer linear arithmetic in the setting of SMT .
We show that this decision problem is coNP - complete and , when monadically decomposable , a formula admits a decomposition of exponential size in the worst case .