sig
  val get_value : model:Z3.Model.model -> ('a, 'b) ZZ3_sigs.S.symbol -> 'a
end