let sigma op l =
  match op, l with
    | Sym.Const(c), [] -> mk_const c
    | Sym.Sub(n,i,j), [x] -> mk_sub n i j x
    | Sym.Conc(n,m), [x;y] ->  mk_conc n m x y
    | Sym.Bitwise(n), [x;y;z] -> mk_bitwise n x y z
    | _ -> failwith "Bv.sigma: ill-formed expression"