sig
  val assert_0_to : SMTSolver.t -> Numeral.t -> Term.t -> unit
  val assert_1_to : SMTSolver.t -> Numeral.t -> Term.t -> unit
  val assert_new_invs_to :
    SMTSolver.t -> Numeral.t -> Term.TermSet.t * Term.TermSet.t -> unit
end