diff --git a/src/solver/sLR.ml b/src/solver/sLR.ml
index fc7f921dde..3bfc233e5e 100644
--- a/src/solver/sLR.ml
+++ b/src/solver/sLR.ml
@@ -76,9 +76,9 @@ module SLR3 =
             HM.replace rho x tmp;
             let w = try HM.find infl x with Not_found -> VS.empty in
             let w = if wpx then VS.add x w else w in
-            q := Seq.fold_left (fun x y -> H.add y x) !q (VS.to_seq w);
+            q := VS.fold H.add w !q;
             HM.replace infl x VS.empty;
-            Seq.iter (HM.remove stable) (VS.to_seq w)
+            VS.iter (HM.remove stable) w
           end;
           while (H.size !q <> 0) && (min_key q <= get_key x) do
             solve (extract_min q)
@@ -107,7 +107,7 @@ module SLR3 =
         HM.find rho y
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
-        Seq.fold_left (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.to_seq w)
+        VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ())
       and side x y d =
         HM.add globals y ();
         if not (HM.mem rho y) then begin
diff --git a/src/solver/sLRphased.ml b/src/solver/sLRphased.ml
index 8146fed6d3..67e8c114a1 100644
--- a/src/solver/sLRphased.ml
+++ b/src/solver/sLRphased.ml
@@ -126,7 +126,7 @@ module Make =
           HM.replace rho x val_new;
           let w = try HM.find infl x with Not_found -> VS.empty in
           (* let w = if wpx then VS.add x w else w in *)
-          q := Seq.fold_left (fun x y -> H.add y x) !q (VS.to_seq w);
+          q := VS.fold H.add w !q;
           HM.replace infl x VS.empty
         end
       and solve0 ?(side=false) x =
@@ -156,12 +156,12 @@ module Make =
           HM.replace rho1 x d;
           let w = VS.add x @@ try HM.find infl x with Not_found -> VS.empty in
           HM.replace infl x VS.empty;
-          q := Seq.fold_left (fun x y -> H.add y x) !q (VS.to_seq w);
+          q := VS.fold H.add w !q;
           iterate true prio
         )
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
-        let v = Seq.fold_left (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.to_seq w)
+        let v = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ())
         in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pretty_trace x S.Dom.pretty v; v
       and eq x get set =
         eval_rhs_event x;
diff --git a/src/solver/sLRterm.ml b/src/solver/sLRterm.ml
index 7025e23301..70419cfb37 100644
--- a/src/solver/sLRterm.ml
+++ b/src/solver/sLRterm.ml
@@ -69,7 +69,7 @@ module SLR3term =
       in
       let sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
-        let v = Seq.fold_left (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.to_seq w) in
+        let v = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in
         if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pretty_trace x S.Dom.pretty v; v
       in
       let rec iterate b_old prio =
@@ -180,7 +180,7 @@ module SLR3term =
           HM.replace rho x val_new;
           let w = try HM.find infl x with Not_found -> VS.empty in
           (* let w = if wpx then VS.add x w else w in *)
-          q := Seq.fold_left (fun x y -> H.add y x) !q (VS.to_seq w);
+          q := VS.fold H.add w !q;
           HM.replace infl x VS.empty
         end;
         b_new
diff --git a/src/solver/topDown.ml b/src/solver/topDown.ml
index f23b4e8cbd..6bd08a72c4 100644
--- a/src/solver/topDown.ml
+++ b/src/solver/topDown.ml
@@ -97,7 +97,7 @@ module WP =
         HM.find rho y
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
-        let d = Seq.fold_left (fun d y -> let r = try S.Dom.join d (HPM.find rho' (y,x)) with Not_found -> d in if tracing then trace "sol2" "sides: side %a from %a: %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty r; r) (S.Dom.bot ()) (VS.to_seq w) in
+        let d = VS.fold (fun y d -> let r = try S.Dom.join d (HPM.find rho' (y,x)) with Not_found -> d in if tracing then trace "sol2" "sides: side %a from %a: %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty r; r) w (S.Dom.bot ()) in
         if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
         d
       and side x y d =
diff --git a/src/solver/topDown_deprecated.ml b/src/solver/topDown_deprecated.ml
index 67f5cc0e09..5743aee5ac 100644
--- a/src/solver/topDown_deprecated.ml
+++ b/src/solver/topDown_deprecated.ml
@@ -93,7 +93,7 @@ module TD3 =
         HM.find rho y
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
-        let d = Seq.fold_left (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.to_seq w) in
+        let d = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in
         if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
         d
       and side x y d =