diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index a01f18a1..55e2830e 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -659,6 +659,7 @@ module type SOLVER = sig val stats : t -> Stat.t val tst : t -> T.Term.state + val ty_st : t -> T.Ty.state val create : ?stat:Stat.t -> diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index d9675bc6..63f650ac 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -498,6 +498,7 @@ module Make(A : ARG) let[@inline] cc self = Solver_internal.cc self.si let[@inline] stats self = self.stat let[@inline] tst self = Solver_internal.tst self.si + let[@inline] ty_st self = Solver_internal.ty_st self.si let[@inline] mk_atom_lit_ self lit : Atom.t = Sat_solver.make_atom self.solver lit