sig
  val make : unit -> Z3.Solver.solver
  val add :
    solver:Z3.Solver.solver -> ZZ3_sigs.S.zbool ZZ3_sigs.S.term -> unit
  val check :
    solver:Z3.Solver.solver ->
    ZZ3_sigs.S.zbool ZZ3_sigs.S.term list -> ZZ3_sigs.S.sat
end