bugfix in find_val_opt and lin_independent

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

@@ -215,7 +215,7 @@ module ListMatrix: AbstractMatrix =
       | x::xs ->
         let pivot_opt = V.findi_val_opt ((<>:) A.zero) v in
         match pivot_opt with
-        | None -> true (* When we found no pivot, the vector is already A.zero. *)
+        | None -> false (* When we found no pivot, the vector is already A.zero. *)
         | Some (pivot_id, pivot) ->
           let new_v = V.map2_preserve_zero (fun v1 v2 -> v1 -: (pivot *: v2)) v x in
           is_linearly_independent_rref new_v xs
@@ -238,10 +238,7 @@ module ListMatrix: AbstractMatrix =
               let linearly_indep = is_linearly_independent_rref v1 m' in 
               if linearly_indep then false else is_covered_by_helper vs1 m'
         in is_covered_by_helper m1 m2
-
-
-
-
+
     let is_covered_by m1 m2 = Timing.wrap "is_covered_by" (is_covered_by m1) m2
 
     let find_opt f m =

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -193,15 +193,14 @@ module SparseVector: AbstractVector =
 
     (* Returns optional of (index * value) where f evaluated to true *)
     let findi_val_opt f v =
-      if f A.zero then  
-        (
-          let i, (col_idx, value) = List.findi (fun i (idx, value) -> if idx > i then true else f value) v.entries  in
-          if i < col_idx then (* In this case, Zero was the first element found because iteration index i is smaller than "found" value *)
-            Some (i, A.zero)
-          else Some (col_idx, value)
-        )
-      else
-        Some (List.find (fun (idx, value) -> f value) v.entries) 
+      let rec find_zero_or_val vec last_col_idx =
+            match vec, last_col_idx with
+            | [], _ -> if v.len <> last_col_idx + 1 && f A.zero then Some (last_col_idx + 1, A.zero) else None
+            | (idx, value) :: xs, i -> 
+              if idx <> last_col_idx + 1 && f A.zero then Some (last_col_idx + 1, A.zero) 
+              else if f value then Some (idx, value) 
+              else find_zero_or_val xs idx
+      in find_zero_or_val v.entries (-1)
 
     let map f v = 
       of_list (List.map f (to_list v))