From 6206ad6378b46a71fd21c50e0d8e5e01e6f7d3e5 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 16 Mar 2015 16:23:30 +0100 Subject: [PATCH] Added some asserts in vectors/sparse vectors --- solver/mcsolver.ml | 2 +- util/sparse_vec.ml | 1 + util/vec.ml | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 2bece663..7f39c374 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -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) diff --git a/util/sparse_vec.ml b/util/sparse_vec.ml index 748eddc6..8ca1bb0c 100644 --- a/util/sparse_vec.ml +++ b/util/sparse_vec.ml @@ -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) diff --git a/util/vec.ml b/util/vec.ml index 57a6571c..a5e3ba44 100644 --- a/util/vec.ml +++ b/util/vec.ml @@ -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)