module Unroller:`sig`

..`end`

Very basic helper functions for unrolling. More precisely, asserting
one- and two-state invariants.

`val assert_0_to : ``SMTSolver.t -> Numeral.t -> Term.t -> unit`

Asserts some terms from

`0`

to `k-1`

.`val assert_1_to : ``SMTSolver.t -> Numeral.t -> Term.t -> unit`

Asserts some terms from

`1`

to `k-1`

.`val assert_new_invs_to : ``SMTSolver.t -> Numeral.t -> Term.TermSet.t * Term.TermSet.t -> unit`

Asserts some new one- and two-state invariant up to

`k-1`

, starting at
* `0`

for one-state invariants,
* `1`

for two-state invariants.