let solve e =
  let (a, b, prf) = Fact.d_equal e in 
  let prf' =  Fact.mk_rule "Arith.solve" [prf] in
    if !integer_solve && is_diophantine a && is_diophantine b then
      let sl = zsolve (a, b) in
        List.map (fun (c, d) -> Fact.mk_equal c d prf') sl
    else 
      match qsolve (a, b) with
        | None -> []
        | Some(c, d) -> [Fact.mk_equal c d prf']