let display_symbol c out s =
  match Z3.symbol_refine c s with
  | Z3.Symbol_int i -> fprintf out "#%d" i;
  | Z3.Symbol_string r ->fprintf out "%s" r;
  | Z3.Symbol_unknown -> ()