let rec is_diophantine a =
try
match a with
| Term.App((Sym.Arith(op), _), al, _) ->
(match op, al with
| Sym.Num _, [] -> true
| Sym.Multq _, [a] -> is_diophantine a
| Sym.Add, al -> List.for_all is_diophantine al
| _ -> false)
| _ ->
Term.Var.is_int a
with
Not_found -> Term.Var.is_int a