sig
  type solution = (Monome.term * Monome.Int.t) list
  val split_solution :
    Monome.Int.Solve.solution ->
    Libzipperposition.Substs.t * Monome.Int.Solve.solution
  val diophant2 : Z.t -> Z.t -> Z.t -> Z.t * Z.t * Z.t
  val diophant_l : Z.t list -> Z.t -> Z.t list * Z.t
  val coeffs_n : Z.t list -> Z.t -> Monome.term list -> Monome.Int.t list
  val eq_zero :
    ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
    Monome.Int.t -> Monome.Int.Solve.solution list
  val lower_zero :
    ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
    strict:bool -> Monome.Int.t -> Monome.Int.Solve.solution list
  val lt_zero :
    ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
    Monome.Int.t -> Monome.Int.Solve.solution list
  val leq_zero :
    ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
    Monome.Int.t -> Monome.Int.Solve.solution list
  val neq_zero :
    ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
    Monome.Int.t -> Monome.Int.Solve.solution list
end