simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 19:55:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Added some asserts in vectors/sparse vectors

Browse source
This commit is contained in:
Guillaume Bury 2015-03-16 16:23:30 +01:00
parent e748333693
commit 6206ad6378
3 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/mcsolver.ml
View file

@ -631,7 +631,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
let slice_propagate f lvl =
L.debug 100 "entering slice.propagate";
let a = add_atom f in
L.debug 100 "atom added";
L.debug 100 "atom added. growing heap...";
Iheap.grow_to_by_double env.order (St.nb_vars ());
L.debug 100 "heap grown";
enqueue_bool a lvl (Semantic lvl)

1
util/sparse_vec.ml
View file

@ -23,6 +23,7 @@ let init sz f default =
let length {sz} = sz
let grow_to t new_capa =
assert (new_capa >= Array.length t.data);
let data = t.data in
let capa = Array.length data in
t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.default)

1
util/vec.ml
View file

@ -48,6 +48,7 @@ let size t = t.sz
let is_empty t = t.sz = 0
let grow_to t new_capa =
assert (new_capa >= Array.length t.data);
let data = t.data in
let capa = Array.length data in
t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy)