Range (soteria-c.Soteria_c_lib.Ctree

type t =
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
  * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

val sem_eq : 
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  MemVal.S_bool.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

val size : 
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

val split_at : ('a * 'b) -> 'c -> ('a * 'c) * ('c * 'b)

val offset : 
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
  * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

val subset_eq : 
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  MemVal.S_bool.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

val strictly_inside : 
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  MemVal.S_bool.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

val inside : 
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  (MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  MemVal.S_bool.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

val of_low_and_size : 
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t ->
  MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
  * MemVal.S_bounded_int.t Soteria.Bv_values.Bv_solver.Z3_solver.Value.t

val pp : 
  Stdlib.Format.formatter ->
  ('a Soteria.Bv_values.Bv_solver.Z3_solver.Value.t
   * 'b Soteria.Bv_values.Bv_solver.Z3_solver.Value.t) ->
  unit