From e6221d7e5044fd73d4fa6051044c8c6f9eef6c11 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 27 Mar 2017 21:05:37 +0200 Subject: [PATCH] add test --- src/data/CCBV.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index a9704052..f00d69f2 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -378,6 +378,13 @@ type 'a sequence = ('a -> unit) -> unit let to_seq bv k = iter_true bv k +(*$Q + Q.(small_int) (fun i -> \ + let i = max 1 i in \ + let bv = create ~size:i true in \ + i = (to_seq bv |> Sequence.length)) + *) + let of_seq seq = let l = ref [] and maxi = ref 0 in seq (fun x -> l := x :: !l; maxi := max !maxi x);