let rec model s xl =
  Format.eprintf "\nWarning: model generation is work in progress...@.";
  let s0 = ground s in
    s0

and ground s =
  S.fold 
    (fun (x, a, rho) s0 -> 
       let q = Arith.constant_of a
       and ml = Arith.nonconstant_of a in
       let s0' = 
         Term.Map.add x (Arith.mk_num q) s0 
       in
       let s0'' = 
         Arith.fold
           (fun y acc -> 
              if not(Term.Map.mem y acc) then
                Term.Map.add y (Arith.mk_zero()) acc
              else 
                acc)
           a s0'
       in
         s0'')
    s Term.Map.empty