let rec abstract c x idx term =
    if Z3.is_eq_ast c term x then Z3.mk_bound c idx (Z3.get_sort c x) else
    match Z3.term_refine c term with
    | Z3.Term_app(k, f, args) -> Z3.mk_app c f (Array.map (abstract c x idx) args)
    | Z3.Term_numeral(nm, s) -> term
    | Z3.Term_var(idx, s) -> term
    | Z3.Term_quantifier(b, w, pats, bound, body) -> 
      let idx = (idx + Array.length bound) in
      let body = abstract c x idx body in 
      let is_forall = b = Z3.Forall in
      let mk_pattern terms = Z3.mk_pattern c (Array.map (abstract c x idx) terms) in
      let patterns = Array.map mk_pattern pats in
      Z3.mk_quantifier c is_forall w patterns
        (Array.map snd bound) (Array.map fst bound) body