let rec is_diophantine = function | App(Arith(Num _), []) -> true | App(Arith(Multq(_)), [x]) -> is_intvar x | App(Arith(Add), xl) -> List.for_all is_diophantine xl | a -> is_intvar a