let rec display_numeral c out nm = 
   match nm with 
   | Z3.Numeral_small(n,1L) -> 
     Printf.fprintf out "%Ld" n
   | Z3.Numeral_small(n,d) -> 
     Printf.fprintf out "%Ld/%Ld" n d
   | Z3.Numeral_large s -> 
     Printf.fprintf out "%s" s