diff --git a/soteria-c/lib/ctree_block.ml b/soteria-c/lib/ctree_block.ml
index bed7479f3..81bd57ca8 100644
--- a/soteria-c/lib/ctree_block.ml
+++ b/soteria-c/lib/ctree_block.ml
@@ -11,24 +11,29 @@ module MemVal = struct
   module TB = Soteria.Sym_states.Tree_block
   module Symex = Csymex
 
-  module SBoundedInt = struct
-    include Typed
-    include Typed.Infix
+  module Bounded_int = struct
+    module Symex = Symex
 
-    type sint = T.sint
-    type sbool = T.sbool
+    type t = T.sint Typed.t
 
     let zero () = Usize.(0s)
-    let ( <@ ) = Typed.Infix.( <$@ )
-    let ( <=@ ) = Typed.Infix.( <=$@ )
+    let one () = Usize.(1s)
 
-    (* We assume addition/overflow within the range of an allocation may never overflow.
-       This allows extremely good reductions around inequalities, which Tree_block relies on.  *)
-    let ( +@ ) = Typed.Infix.( +!!@ )
-    let ( -@ ) = Typed.Infix.( -!!@ )
-
-    let in_bound (v : sint Typed.t) : sbool Typed.t =
+    let in_bound (v : t) : T.sbool Typed.t =
       v >=@ zero () &&@ (v <=@ Typed.BitVec.isize_max)
+
+    let pp = Value.ppa
+    let of_z z = Typed.BitVec.usize z
+    let subst = Typed.subst
+    let iter_vars v f = Typed.iter_vars v f
+    let equal = Typed.equal
+    let sem_eq = Typed.sem_eq
+    let distinct = Typed.distinct
+    let add = Infix.( +!@ )
+    let sub = Infix.( -!@ )
+    let to_z = Typed.BitVec.to_z
+    let lt = Infix.( <@ )
+    let leq = Infix.( <=@ )
   end
 
   let pp_init ft (v, ty) =
diff --git a/soteria-c/lib/driver.ml b/soteria-c/lib/driver.ml
index c7cc87514..32dcb75d3 100644
--- a/soteria-c/lib/driver.ml
+++ b/soteria-c/lib/driver.ml
@@ -338,7 +338,7 @@ let dump_summaries results =
       let pp_summary ~fid ft summary =
         Fmt.pf ft "@[<v 2>%a@]" Summary.pp (Summary.analyse ~fid summary)
       in
-      let@ oc = Channels.with_out_file file in
+      let@ oc = Out_channel.with_open_text file in
       let ft = Format.formatter_of_out_channel oc in
       List.iter
         (fun (fid, summaries) ->
diff --git a/soteria-c/lib/globs.ml b/soteria-c/lib/globs.ml
index 63df1ce5d..6f821d1e2 100644
--- a/soteria-c/lib/globs.ml
+++ b/soteria-c/lib/globs.ml
@@ -57,7 +57,7 @@ let get sym st =
                let open Typed.Infix in
                if Cerb_frontend.Symbol.equal_sym k sym then None
                else
-                 let neq = Typed.not (v ==@ loc) in
+                 let neq = Typed.S_bool.not (v ==@ loc) in
                  Some neq)
         |> List.of_seq
       in
@@ -75,7 +75,7 @@ let produce serialized st =
       |> Seq.self_cross_product
       |> Seq.map (fun ((_, loca), (_, locb)) ->
              let open Typed.Infix in
-             Typed.not (loca ==@ locb))
+             Typed.S_bool.not (loca ==@ locb))
       |> List.of_seq
     in
     assume to_assume
diff --git a/soteria-c/lib/interp.ml b/soteria-c/lib/interp.ml
index 4fe634a85..15de1b5bb 100644
--- a/soteria-c/lib/interp.ml
+++ b/soteria-c/lib/interp.ml
@@ -1304,7 +1304,7 @@ module Make (State : State_intf.S) = struct
         let rec loop () =
           let* cond_v = eval_expr cond in
           let^ cond_v = cast_aggregate_to_bool cond_v in
-          let neg_cond = Typed.not cond_v in
+          let neg_cond = Typed.S_bool.not cond_v in
           if%sat neg_cond then ok Normal
           else
             let () = L.trace (fun m -> m "Condition is SAT!") in
@@ -1325,7 +1325,7 @@ module Make (State : State_intf.S) = struct
           | Normal | Continue ->
               let* cond_v = eval_expr cond in
               let^ cond_v = cast_aggregate_to_bool cond_v in
-              if%sat Typed.not cond_v then ok Normal else loop ()
+              if%sat Typed.S_bool.not cond_v then ok Normal else loop ()
           | Case _ -> failwith "SOTERIA BUG: Case in do body"
         in
         loop ()
diff --git a/soteria-c/test/cram/simple_bi.t/run.t b/soteria-c/test/cram/simple_bi.t/run.t
index 900a4f1c3..8e2a8ef53 100644
--- a/soteria-c/test/cram/simple_bi.t/run.t
+++ b/soteria-c/test/cram/simple_bi.t/run.t
@@ -23,7 +23,7 @@
                info = None })];
            globs = [] }
           ];
-        pc = [(0x0000000000000000 != V|1|); (0xfffffffffffffffc <=u V|2|)];
+        pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)];
         post =
         { heap =
           [(V|1|,
@@ -122,7 +122,7 @@ NO_COLOR=true is necessary to avoid test output changing in CI. For some reason,
                info = None })];
            globs = [] }
           ];
-        pc = [(0x0000000000000000 != V|1|); (0xfffffffffffffffc <=u V|2|)];
+        pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)];
         post =
         { heap =
           [(V|1|,
@@ -255,7 +255,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
           ];
         pc =
         [(0x0000000000000000 != V|2|); (0x00000001 <=u V|1|);
-          (V|1| <=u 0x7fffffff); (0xfffffffffffffffc <=u V|3|)];
+          (V|1| <=u 0x7fffffff); (V|3| <=u 0x7ffffffffffffffb)];
         post =
         { heap =
           [(V|2|,
@@ -309,7 +309,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
           ];
         pc =
         [(0x0000000000000000 != V|1|); (V|3| == 0x00000001);
-          (0xfffffffffffffffc <=u V|2|); (V|3| == 0x00000001)];
+          (V|2| <=u 0x7ffffffffffffffb); (V|3| == 0x00000001)];
         post =
         { heap =
           [(V|1|,
@@ -341,9 +341,12 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
           ];
         pc =
         [(0x0000000000000000 != V|1|);
+          ((V|2| <s 0x0000000000000000) == ((V|2| + 0x0000000000000004) <s 0x0000000000000000));
+          ((V|2| + 0x0000000000000004) <u (V|2| + 0x0000000000000008));
+          ((V|2| + 0x0000000000000004) <=u (V|2| +ck 0x0000000000000004));
           ((V|4| <s 0x00000000) != ((V|4| + V|5|) <s 0x00000000));
           ((V|4| <s 0x00000000) == (V|5| <s 0x00000000));
-          (0xfffffffffffffffc <=u V|2|); (0x00000002 <=u V|3|);
+          (V|2| <=u 0x7ffffffffffffff7); (0x00000002 <=u V|3|);
           (V|3| <=u 0x7fffffff)];
         post =
         { heap =
@@ -351,7 +354,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
             { node =
               [MemVal {offset = V|2|; len = 0x0000000000000004;
                  v = V|4| : signed int};
-               MemVal {offset = (V|2| +ck 0x0000000000000004);
+               MemVal {offset = (V|2| + 0x0000000000000004);
                  len = 0x0000000000000004; v = V|5| : signed int}];
               info = None })];
           globs = [] };
@@ -381,8 +384,11 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
           ];
         pc =
         [(0x0000000000000000 != V|1|);
+          ((V|2| <s 0x0000000000000000) == ((V|2| + 0x0000000000000004) <s 0x0000000000000000));
+          ((V|2| + 0x0000000000000004) <u (V|2| + 0x0000000000000008));
+          ((V|2| + 0x0000000000000004) <=u (V|2| +ck 0x0000000000000004));
           (((V|4| <s 0x00000000) == ((V|4| + V|5|) <s 0x00000000)) || ((V|4| <s 0x00000000) != (V|5| <s 0x00000000)));
-          (V|3| == 0x00000002); (0xfffffffffffffffc <=u V|2|);
+          (V|3| == 0x00000002); (V|2| <=u 0x7ffffffffffffff7);
           (V|3| == 0x00000002)];
         post =
         { heap =
@@ -390,7 +396,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
             { node =
               [MemVal {offset = V|2|; len = 0x0000000000000004;
                  v = V|4| : signed int};
-               MemVal {offset = (V|2| +ck 0x0000000000000004);
+               MemVal {offset = (V|2| + 0x0000000000000004);
                  len = 0x0000000000000004; v = V|5| : signed int}];
               info = None })];
           globs = [] };
diff --git a/soteria-rust/lib/interp.ml b/soteria-rust/lib/interp.ml
index fdcda8584..e069bf8a3 100644
--- a/soteria-rust/lib/interp.ml
+++ b/soteria-rust/lib/interp.ml
@@ -108,7 +108,7 @@ module Make (State : State_intf.S) = struct
   let rec resolve_constant (const : Expressions.constant_expr) =
     match const.kind with
     | CLiteral (VScalar scalar) -> ok (Base (BV.of_scalar scalar))
-    | CLiteral (VBool b) -> ok (Base (BV.of_bool (Typed.bool b)))
+    | CLiteral (VBool b) -> ok (Base (BV.of_bool (Typed.S_bool.of_bool b)))
     | CLiteral (VChar c) -> ok (Base (BV.u32i (Uchar.to_int c)))
     | CLiteral (VFloat { float_value; float_ty }) ->
         ok (Base (Typed.Float.mk float_ty float_value))
diff --git a/soteria-rust/lib/rtree_block.ml b/soteria-rust/lib/rtree_block.ml
index 9c8592cf4..90928378b 100644
--- a/soteria-rust/lib/rtree_block.ml
+++ b/soteria-rust/lib/rtree_block.ml
@@ -19,26 +19,31 @@ module Make (Sptr : Sptr.S) = struct
     module TB = Soteria.Sym_states.Tree_block
     module Symex = DecayMapMonad
 
-    module SBoundedInt = struct
-      include Typed
-      include Typed.Infix
+    module Bounded_int = struct
+      module Symex = Symex
 
-      type sint = T.sint
-      type sbool = T.sbool
+      type t = T.sint Typed.t
 
       let zero () = Typed.BitVec.usize Z.zero
-      let ( <@ ) = Typed.Infix.( <$@ )
-      let ( <=@ ) = Typed.Infix.( <=$@ )
+      let one () = Typed.BitVec.usize Z.one
 
-      (* We assume addition/overflow within the range of an allocation may never overflow.
-         This allows extremely good reductions around inequalities, which Tree_block relies on.  *)
-      let ( +@ ) = Typed.Infix.( +!!@ )
-      let ( -@ ) = Typed.Infix.( -!!@ )
-
-      let in_bound (v : sint Typed.t) : sbool Typed.t =
+      let in_bound (v : t) : S_bool.t Typed.t =
         let max = Layout.max_value_z (TInt Isize) in
         let max = Typed.BitVec.usize max in
         v >=@ zero () &&@ (v <=@ max)
+
+      let pp = Value.ppa
+      let of_z z = Typed.BitVec.usize z
+      let subst = Typed.subst
+      let iter_vars v f = Typed.iter_vars v f
+      let equal = Typed.equal
+      let sem_eq = Typed.sem_eq
+      let distinct = Typed.distinct
+      let add = Infix.( +!@ )
+      let sub = Infix.( -!@ )
+      let to_z = Typed.BitVec.to_z
+      let lt = Infix.( <@ )
+      let leq = Infix.( <=@ )
     end
 
     let pp_init ft (v, ty) =
diff --git a/soteria-rust/lib/rustsymex.ml b/soteria-rust/lib/rustsymex.ml
index 1b7f93cd8..66f341ff3 100644
--- a/soteria-rust/lib/rustsymex.ml
+++ b/soteria-rust/lib/rustsymex.ml
@@ -12,7 +12,7 @@ include
 
 include Syntaxes.FunctionWrap
 
-let match_on (elements : 'a list) ~(constr : 'a -> Typed.sbool Typed.t) :
+let match_on (elements : 'a list) ~(constr : 'a -> Typed.S_bool.t Typed.t) :
     'a option t =
   let open Syntax in
   let rec aux = function
diff --git a/soteria-rust/lib/typed.ml b/soteria-rust/lib/typed.ml
index 17127893a..7285ce713 100644
--- a/soteria-rust/lib/typed.ml
+++ b/soteria-rust/lib/typed.ml
@@ -94,7 +94,7 @@ module BitVec = struct
   let of_literal : Values.literal -> [> T.sint ] t = function
     | VScalar s -> of_scalar s
     | VChar c -> u32i (Uchar.to_int c)
-    | VBool b -> of_bool (bool b)
+    | VBool b -> of_bool (S_bool.of_bool b)
     | l ->
         Fmt.failwith "Cannot convert non-scalar literal %s to bitvector"
           (PrintValues.literal_to_string l)
diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml
index 442dd36b6..7a6ed163b 100644
--- a/soteria/lib/bv_values/analyses.ml
+++ b/soteria/lib/bv_values/analyses.ml
@@ -18,7 +18,7 @@ module type S = sig
 
   (** Encode all the information relevant to the given variables and conjuncts
       them with the given accumulator. *)
-  val encode : ?vars:Var.Hashset.t -> t -> Typed.sbool Typed.t Iter.t
+  val encode : ?vars:Var.Hashset.t -> t -> Typed.S_bool.t Typed.t Iter.t
 end
 
 module Merge (A1 : S) (A2 : S) : S = struct
@@ -45,7 +45,7 @@ module Merge (A1 : S) (A2 : S) : S = struct
     let v'', vars2 = A2.add_constraint a2 v' in
     (v'', Var.Set.union vars1 vars2)
 
-  let encode ?vars (a1, a2) : Typed.sbool Typed.t Iter.t =
+  let encode ?vars (a1, a2) : Typed.S_bool.t Typed.t Iter.t =
     Iter.append (A1.encode ?vars a1) (A2.encode ?vars a2)
 end
 
@@ -266,7 +266,7 @@ module Interval : S = struct
           m "Useless range  %a: %a %a = %a" Var.pp var Data.pp range Range.pps
             new_range Data.pp range');
       let is_ok = not (Data.is_empty range) in
-      (Svalue.Bool.bool is_ok, Var.Set.empty, st))
+      (Svalue.S_bool.of_bool is_ok, Var.Set.empty, st))
     else
       let st = Var.Map.add var range' st in
       log (fun m ->
@@ -281,12 +281,12 @@ module Interval : S = struct
         (eq, Var.Set.empty, st)
       else if Data.is_empty range' then
         (* The range is empty, so this cannot be true *)
-        (Svalue.Bool.v_false, Var.Set.empty, st)
+        (Svalue.S_bool.v_false, Var.Set.empty, st)
       else
         (* We could cleanly absorb the range, so the PC doesn't need to store it -- however
            we must mark this variable as dirty, as maybe the modified range still renders
            the branch infeasible, e.g. because of some additional PC assertions. *)
-        (Svalue.Bool.v_true, Var.Set.singleton var, st)
+        (Svalue.S_bool.v_true, Var.Set.singleton var, st)
 
   let rec as_range (v : Svalue.t) =
     match v.node.kind with
@@ -430,8 +430,8 @@ module Interval : S = struct
         (v1' &&@ v2', learnt1 &&@ learnt2, Var.Set.union vars1 vars2, st'')
     | _, (lazy (Some (var, size, srange))) ->
         let learnt, vars, st' = update st var size srange in
-        (Svalue.Bool.v_true, learnt, vars, st')
-    | _, (lazy None) -> (v, Svalue.Bool.v_true, Var.Set.empty, st)
+        (Svalue.S_bool.v_true, learnt, vars, st')
+    | _, (lazy None) -> (v, Svalue.S_bool.v_true, Var.Set.empty, st)
 
   let simplify (v : Svalue.t) st =
     match (v.node.kind, lazy (as_range v)) with
@@ -447,10 +447,10 @@ module Interval : S = struct
         (* If the state is unchanged, then the conjunction covers all possible states and
            this is always true. (I think.) *)
         if
-          Svalue.equal v1' Svalue.Bool.v_true
-          && Svalue.equal v2' Svalue.Bool.v_true
+          Svalue.equal v1' Svalue.S_bool.v_true
+          && Svalue.equal v2' Svalue.S_bool.v_true
           && st_equal st st'
-        then Svalue.Bool.v_true
+        then Svalue.S_bool.v_true
         else v
     | _, (lazy (Some (var, size, srange))) ->
         let range = get size var st in
@@ -460,8 +460,8 @@ module Interval : S = struct
         let range', redundant = Data.add range srange in
         log (fun m ->
             m "Redundant? %b Empty? %b" redundant (Data.is_empty range'));
-        if redundant then Svalue.Bool.v_true
-        else if Data.is_empty range' then Svalue.Bool.v_false
+        if redundant then Svalue.S_bool.v_true
+        else if Data.is_empty range' then Svalue.S_bool.v_false
         else v
     | _, (lazy None) -> v
 
@@ -480,7 +480,7 @@ module Interval : S = struct
   let simplify st v = wrap_read (simplify v) st
   let add_constraint st v = wrap (add_constraint v) st
 
-  let encode ?vars st : Typed.sbool Typed.t Iter.t =
+  let encode ?vars st : Typed.S_bool.t Typed.t Iter.t =
     let to_check =
       Option.fold ~none:(fun _ -> true) ~some:Var.Hashset.mem vars
     in
@@ -566,8 +566,8 @@ module Equality : S = struct
         | None -> (
             match v.node.kind with
             | Binop ((Eq | Leq _), l, r) when known_eq l r st ->
-                Svalue.Bool.v_true
-            | Binop (Lt _, l, r) when known_eq l r st -> Svalue.Bool.v_false
+                Svalue.S_bool.v_true
+            | Binop (Lt _, l, r) when known_eq l r st -> Svalue.S_bool.v_false
             | Binop (op, l, r) ->
                 let l' = simplify l in
                 let r' = simplify r in
diff --git a/soteria/lib/bv_values/bv_solver.ml b/soteria/lib/bv_values/bv_solver.ml
index 363cf04a0..8b265efdb 100644
--- a/soteria/lib/bv_values/bv_solver.ml
+++ b/soteria/lib/bv_values/bv_solver.ml
@@ -8,34 +8,34 @@ let rec simplify ~trivial_truthiness ~fallback (v : Svalue.t) =
   | Bool _ | BitVec _ | Float _ -> v
   | _ -> (
       match trivial_truthiness (Typed.type_ v) with
-      | Some true -> Svalue.Bool.v_true
-      | Some false -> Svalue.Bool.v_false
+      | Some true -> Svalue.S_bool.v_true
+      | Some false -> Svalue.S_bool.v_false
       | None -> (
           match v.node.kind with
           | Unop (Not, e) ->
               let e' = simplify e in
-              if Svalue.equal e e' then fallback v else Svalue.Bool.not e'
+              if Svalue.equal e e' then fallback v else Svalue.S_bool.not e'
           | Binop (Eq, e1, e2) ->
-              if Svalue.equal e1 e2 then Svalue.Bool.v_true
-              else if Svalue.sure_neq e1 e2 then Svalue.Bool.v_false
-              else fallback v
+              if Svalue.equal e1 e2 then Svalue.S_bool.v_true
+              else if Svalue.sure_neq e1 e2 then Svalue.S_bool.v_false
+              else v
           | Binop (And, e1, e2) ->
               let se1 = simplify e1 in
               let se2 = simplify e2 in
               if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v
-              else Svalue.Bool.and_ se1 se2
+              else Svalue.S_bool.and_ se1 se2
           | Binop (Or, e1, e2) ->
               let se1 = simplify e1 in
               let se2 = simplify e2 in
-              if Svalue.equal se1 e1 && Svalue.equal se2 e2 then fallback v
-              else Svalue.Bool.or_ se1 se2
+              if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v
+              else Svalue.S_bool.or_ se1 se2
           | Ite (g, e1, e2) ->
               let sg = simplify g in
               let se1 = simplify e1 in
               let se2 = simplify e2 in
               if Svalue.equal sg g && Svalue.equal se1 e1 && Svalue.equal se2 e2
               then v
-              else Svalue.Bool.ite sg se1 se2
+              else Svalue.S_bool.ite sg se1 se2
           | _ -> fallback v))
 
 module Make_incremental
@@ -52,7 +52,7 @@ struct
   end)
 
   module Solver_state = struct
-    type t = Typed.sbool Typed.t Dynarray.t Dynarray.t
+    type t = Typed.S_bool.t Typed.t Dynarray.t Dynarray.t
 
     let init () =
       let t = Dynarray.create () in
@@ -93,7 +93,7 @@ struct
 
     let iter (t : t) f = Dynarray.iter (fun t -> Dynarray.iter f t) t
 
-    let trivial_truthiness_of (t : t) (v : Typed.sbool Typed.t) =
+    let trivial_truthiness_of (t : t) (v : Typed.S_bool.t Typed.t) =
       let neg_v = Typed.not v in
       Dynarray.find_map
         (Dynarray.find_map (fun value ->
@@ -213,7 +213,7 @@ struct
         instance because an auxiliary analysis has new information about it that
         is not directly in the PC. *)
     type slot_content =
-      | Asrt of Typed.sbool Typed.t [@printer Typed.ppa]
+      | Asrt of Typed.S_bool.t Typed.t [@printer Typed.ppa]
       | Dirty of Var.Set.t [@printer Fmt.(iter ~sep:comma) Var.Set.iter Var.pp]
     [@@deriving show]
 
@@ -276,7 +276,7 @@ struct
       | _ -> None
 
     (* We check if the thing contains the value itself, or its negation. *)
-    let trivial_truthiness_of (t : t) (v : Typed.sbool Typed.t) =
+    let trivial_truthiness_of (t : t) (v : Typed.S_bool.t Typed.t) =
       let neg_v = Typed.not v in
       Dynarray.find_map
         (Dynarray.find_map (function
@@ -475,7 +475,7 @@ struct
     [|n| == v] exists, in which case we replace it with the value [v].
     If the constraint evaluates to true, then it is satisfiable. *)
     let v_eqs = Var.Hashtbl.create 8 in
-    Svalue.Bool.split_ands to_check (fun v ->
+    Svalue.S_bool.split_ands to_check (fun v ->
         match v.node.kind with
         | Binop
             ( Eq,
@@ -496,7 +496,7 @@ struct
       | _ -> v_var
     in
     let res = Eval.eval ~eval_var to_check in
-    Svalue.equal res Svalue.Bool.v_true
+    Svalue.equal res Svalue.S_bool.v_true
 
   let check_sat_raw solver relevant_vars to_check =
     (* TODO: we shouldn't wait for ack for each command individually... *)
@@ -534,9 +534,11 @@ struct
           Solver_state.unchecked_constraints solver.state
         in
         (* This will put the check in a somewhat-normal form, to increase cache hits. *)
-        let to_check = Dynarray.fold_left Typed.and_ Typed.v_true to_check in
         let to_check =
-          Iter.fold Typed.and_ to_check
+          Dynarray.fold_left Typed.S_bool.and_ Typed.v_true to_check
+        in
+        let to_check =
+          Iter.fold Typed.S_bool.and_ to_check
             (Analysis.encode ~vars:relevant_vars solver.analysis)
         in
         let answer = check_sat_raw_memo solver relevant_vars to_check in
diff --git a/soteria/lib/bv_values/encoding.ml b/soteria/lib/bv_values/encoding.ml
index bb795edef..baa55a95b 100644
--- a/soteria/lib/bv_values/encoding.ml
+++ b/soteria/lib/bv_values/encoding.ml
@@ -130,7 +130,7 @@ and encode_value_memo v =
       k
 
 let encode_value (v : Svalue.t) =
-  Svalue.Bool.split_ands v
+  Svalue.S_bool.split_ands v
   |> Iter.map encode_value_memo
   |> Iter.to_list
   |> bool_ands
diff --git a/soteria/lib/bv_values/eval.ml b/soteria/lib/bv_values/eval.ml
index 32eed2d97..ccb43e241 100644
--- a/soteria/lib/bv_values/eval.ml
+++ b/soteria/lib/bv_values/eval.ml
@@ -2,9 +2,9 @@ open Svalue
 open Soteria_std
 
 let eval_binop : Binop.t -> t -> t -> t = function
-  | And -> Bool.and_
-  | Or -> Bool.or_
-  | Eq -> Bool.sem_eq
+  | And -> S_bool.and_
+  | Or -> S_bool.or_
+  | Eq -> S_bool.sem_eq
   | FEq -> Float.eq
   | FLeq -> Float.leq
   | FLt -> Float.lt
@@ -31,7 +31,7 @@ let eval_binop : Binop.t -> t -> t -> t = function
   | AShr -> BitVec.ashr
 
 let eval_unop : Unop.t -> t -> t = function
-  | Not -> Bool.not
+  | Not -> S_bool.not
   | FAbs -> Float.abs
   | GetPtrLoc -> Ptr.loc
   | GetPtrOfs -> Ptr.ofs
@@ -68,12 +68,12 @@ let rec eval ~eval_var (x : t) : t =
   | Nop (nop, l) -> (
       let l, changed = List.map_changed eval l in
       if Stdlib.not changed then x
-      else match nop with Distinct -> Bool.distinct l)
+      else match nop with Distinct -> S_bool.distinct l)
   | Ite (guard, then_, else_) ->
       let guard = eval guard in
-      if equal guard Bool.v_true then eval then_
-      else if equal guard Bool.v_false then eval else_
-      else Bool.ite guard (eval then_) (eval else_)
+      if equal guard S_bool.v_true then eval then_
+      else if equal guard S_bool.v_false then eval else_
+      else S_bool.ite guard (eval then_) (eval else_)
   | Seq l ->
       let l, changed = List.map_changed eval l in
       if Stdlib.not changed then x else Svalue.SSeq.mk ~seq_ty:x.node.ty l
diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml
index 99cb9421f..32744575d 100644
--- a/soteria/lib/bv_values/svalue.ml
+++ b/soteria/lib/bv_values/svalue.ml
@@ -113,7 +113,7 @@ end
 
 module Binop = struct
   type t =
-    (* Bool *)
+    (* S_bool *)
     | And
     | Or
     (* Comparison *)
@@ -352,11 +352,11 @@ let rec subst subst_var sv =
 
 (** {2 Operator declarations} *)
 
-module type Bool = sig
+module type S_bool = sig
   val v_true : t
   val v_false : t
-  val as_bool : t -> bool option
-  val bool : bool -> t
+  val to_bool : t -> bool option
+  val of_bool : bool -> t
   val and_ : t -> t -> t
   val or_ : t -> t -> t
   val conj : t list -> t
@@ -464,16 +464,16 @@ end
 
 (** {2 Booleans} *)
 
-module rec Bool : Bool = struct
+module rec S_bool : S_bool = struct
   let v_true = Bool true <| TBool
   let v_false = Bool false <| TBool
 
-  let as_bool t =
+  let to_bool t =
     if equal t v_true then Some true
     else if equal t v_false then Some false
     else None
 
-  let bool b =
+  let of_bool b =
     (* avoid re-alloc and re-hashconsing *)
     if b then v_true else v_false
 
@@ -550,9 +550,9 @@ module rec Bool : Bool = struct
   and sem_eq v1 v2 =
     match (v1.node.kind, v2.node.kind) with
     | _ when equal v1 v2 -> v_true
-    | Bool b1, Bool b2 -> bool (b1 = b2)
+    | Bool b1, Bool b2 -> of_bool (b1 = b2)
     | Ptr (l1, o1), Ptr (l2, o2) -> and_ (sem_eq l1 l2) (sem_eq o1 o2)
-    | BitVec b1, BitVec b2 -> bool (Z.equal b1 b2)
+    | BitVec b1, BitVec b2 -> of_bool (Z.equal b1 b2)
     (* Arithmetics *)
     | BitVec _, Unop (Neg, v2) -> sem_eq (BitVec.neg v1) v2
     | Unop (Neg, v1), BitVec _ -> sem_eq v1 (BitVec.neg v2)
@@ -572,16 +572,16 @@ module rec Bool : Bool = struct
         sem_eq (BitVec.sub l v2) r
     | _, Binop (Add _, v2, { node = { kind = BitVec bv; _ }; _ })
       when equal v1 v2 ->
-        bool Z.(equal bv zero)
+        of_bool Z.(equal bv zero)
     | _, Binop (Add _, { node = { kind = BitVec bv; _ }; _ }, v2)
       when equal v1 v2 ->
-        bool Z.(equal bv zero)
+        of_bool Z.(equal bv zero)
     | Binop (Add _, { node = { kind = BitVec bv; _ }; _ }, v1), _
       when equal v1 v2 ->
-        bool Z.(equal bv zero)
+        of_bool Z.(equal bv zero)
     | Binop (Add _, v1, { node = { kind = BitVec bv; _ }; _ }), _
       when equal v1 v2 ->
-        bool Z.(equal bv zero)
+        of_bool Z.(equal bv zero)
     | ( ( Binop (Add _, ({ node = { kind = BitVec bv_l; _ }; _ } as l), y)
         | Binop (Add _, y, ({ node = { kind = BitVec bv_l; _ }; _ } as l)) ),
         ( Binop (Add _, ({ node = { kind = BitVec bv_r; _ }; _ } as r), x)
@@ -601,7 +601,7 @@ module rec Bool : Bool = struct
         | Binop (Mul { checked = true }, x, { node = { kind = BitVec m; _ }; _ })
           ),
         BitVec n ) ->
-        if Z.(equal m zero) then bool (Z.equal n Z.zero)
+        if Z.(equal m zero) then of_bool (Z.equal n Z.zero)
         else if Z.(equal n zero) then sem_eq x (BitVec.zero (size_of x.node.ty))
         else if Z.(divisible n m) then
           sem_eq x (BitVec.mk (size_of x.node.ty) Z.(n / m))
@@ -781,25 +781,25 @@ and BitVec : BitVec = struct
     let res = op l r in
     Z.Compare.(res < minz || res > maxz)
 
-  let ovf_check ~signed n l r op = Bool.bool @@ overflows ~signed n l r op
+  let ovf_check ~signed n l r op = S_bool.of_bool @@ overflows ~signed n l r op
 
   let of_bool n b =
-    if equal Bool.v_true b then one n
-    else if equal Bool.v_false b then zero n
+    if equal S_bool.v_true b then one n
+    else if equal S_bool.v_false b then zero n
     else Unop (BvOfBool n, b) <| TBitVector n
 
   let to_bool v =
     match v.node.kind with
-    | BitVec z -> Bool.bool (Stdlib.not (Z.equal z Z.zero))
+    | BitVec z -> S_bool.of_bool (Stdlib.not (Z.equal z Z.zero))
     | Unop (BvOfBool _, sv') -> sv'
-    | _ -> Bool.not (Bool.sem_eq v (zero (size_of v.node.ty)))
+    | _ -> S_bool.not (S_bool.sem_eq v (zero (size_of v.node.ty)))
 
   let not_bool v =
     let n = size_of v.node.ty in
     match v.node.kind with
     | BitVec z -> if Z.equal z Z.zero then one n else zero n
-    | Unop (BvOfBool n, g) -> of_bool n (Bool.not g)
-    | _ -> of_bool n (Bool.sem_eq v (zero n))
+    | Unop (BvOfBool n, g) -> of_bool n (S_bool.not g)
+    | _ -> of_bool n (S_bool.sem_eq v (zero n))
 
   let rec add ?(checked = false) v1 v2 =
     assert (equal_ty v1.node.ty v2.node.ty);
@@ -875,7 +875,7 @@ and BitVec : BitVec = struct
         (* only propagate down ites if we know it's concrete *)
         let n = size_of v1.node.ty in
         let x = mk n x in
-        Bool.ite b (add ~checked l x) (add ~checked r x)
+        S_bool.ite b (add ~checked l x) (add ~checked r x)
     | _ -> mk_commut_binop (Add { checked }) v1 v2 <| v1.node.ty
 
   and sub ?(checked = false) v1 v2 =
@@ -902,10 +902,10 @@ and BitVec : BitVec = struct
     | Binop (Add _, l1, r1), Binop (Add _, l2, r2) when equal l1 l2 ->
         sub ~checked r1 r2
     (* only propagate down ites if we know it's concrete *)
-    | Ite (b, l, r), BitVec _ -> Bool.ite b (sub l v2) (sub r v2)
-    | BitVec _, Ite (b, l, r) -> Bool.ite b (sub v1 l) (sub v1 r)
-    | Unop (BvOfBool n, b), BitVec _ -> Bool.ite b (sub (one n) v2) (neg v2)
-    | BitVec _, Unop (BvOfBool n, b) -> Bool.ite b (sub v1 (one n)) v1
+    | Ite (b, l, r), BitVec _ -> S_bool.ite b (sub l v2) (sub r v2)
+    | BitVec _, Ite (b, l, r) -> S_bool.ite b (sub v1 l) (sub v1 r)
+    | Unop (BvOfBool n, b), BitVec _ -> S_bool.ite b (sub (one n) v2) (neg v2)
+    | BitVec _, Unop (BvOfBool n, b) -> S_bool.ite b (sub v1 (one n)) v1
     | _ -> Binop (Sub { checked }, v1, v2) <| v1.node.ty
 
   and neg v =
@@ -917,8 +917,8 @@ and BitVec : BitVec = struct
     match v.node.kind with
     | BitVec bv -> mk_masked n Z.(neg bv)
     | Unop (Neg, v) -> v
-    | Ite (b, l, r) -> Bool.ite b (neg l) (neg r)
-    | Unop (BvOfBool n, b) -> Bool.ite b (neg (one n)) (zero n)
+    | Ite (b, l, r) -> S_bool.ite b (neg l) (neg r)
+    | Unop (BvOfBool n, b) -> S_bool.ite b (neg (one n)) (zero n)
     | _ -> Unop (Neg, v) <| v.node.ty
 
   (** [mod_ v1 v2] is the signed remainder of [v1 / v2], which takes the sign of
@@ -968,7 +968,7 @@ and BitVec : BitVec = struct
     | BitVec bv ->
         let n = size_of v.node.ty in
         mk_masked n Z.(lognot bv)
-    | Ite (b, l, r) -> Bool.ite b (not l) (not r)
+    | Ite (b, l, r) -> S_bool.ite b (not l) (not r)
     | _ -> Unop (BvNot, v) <| v.node.ty
 
   and and_ v1 v2 =
@@ -991,8 +991,8 @@ and BitVec : BitVec = struct
            let low_mask = Z.(pred (one lsl bitwidth)) in
            Z.(equal (mask land low_mask) low_mask) ->
         base <| t_bv n
-    | BitVec _, Ite (b, l, r) -> Bool.ite b (and_ v1 l) (and_ v1 r)
-    | Ite (b, l, r), BitVec _ -> Bool.ite b (and_ l v2) (and_ r v2)
+    | BitVec _, Ite (b, l, r) -> S_bool.ite b (and_ v1 l) (and_ v1 r)
+    | Ite (b, l, r), BitVec _ -> S_bool.ite b (and_ l v2) (and_ r v2)
     (* if it's a right mask, it's usually beneficial to propagate it *)
     | (BitVec mask, Binop (BitAnd, l, r) | Binop (BitAnd, l, r), BitVec mask)
       when is_right_mask mask ->
@@ -1002,12 +1002,12 @@ and BitVec : BitVec = struct
     | BitVec o, Unop (BvOfBool _, _) when Z.equal o Z.one -> v2
     | Unop (BvOfBool _, _), BitVec o when Z.equal o Z.one -> v1
     | Unop (BvOfBool _, b1), Unop (BvOfBool _, b2) ->
-        of_bool n (Bool.and_ b1 b2)
+        of_bool n (S_bool.and_ b1 b2)
     | ( Ite (b1, l1, { node = { kind = BitVec r1; _ }; _ }),
         Ite (b2, l2, { node = { kind = BitVec r2; _ }; _ }) )
       when Z.(equal r1 zero) && Z.(equal r2 zero) ->
         let n = size_of v1.node.ty in
-        Bool.ite (Bool.and_ b1 b2) (and_ l1 l2) (zero n)
+        S_bool.ite (S_bool.and_ b1 b2) (and_ l1 l2) (zero n)
     | _, _ -> mk_commut_binop BitAnd v1 v2 <| t_bv n
 
   and or_ v1 v2 =
@@ -1034,7 +1034,8 @@ and BitVec : BitVec = struct
         else
           let new_tail = extract 0 (nx - 1) tail in
           concat new_tail base
-    | Unop (BvOfBool n, b1), Unop (BvOfBool _, b2) -> of_bool n (Bool.or_ b1 b2)
+    | Unop (BvOfBool n, b1), Unop (BvOfBool _, b2) ->
+        of_bool n (S_bool.or_ b1 b2)
     | _ -> mk_commut_binop BitOr v1 v2 <| v1.node.ty
 
   and xor v1 v2 =
@@ -1045,7 +1046,7 @@ and BitVec : BitVec = struct
     | BitVec z, _ when Z.equal z Z.zero -> v2
     | _, BitVec z when Z.equal z Z.zero -> v1
     | Unop (BvOfBool n, b1), Unop (BvOfBool _, b2) ->
-        of_bool n (Bool.not (Bool.sem_eq b1 b2))
+        of_bool n (S_bool.not (S_bool.sem_eq b1 b2))
     | _ -> mk_commut_binop BitXor v1 v2 <| v1.node.ty
 
   (** [extract from_ to_ v] returns a bitvector covering bits from index
@@ -1087,7 +1088,7 @@ and BitVec : BitVec = struct
     | Ite (b, l, r) ->
         let l = extract from_ to_ l in
         let r = extract from_ to_ r in
-        Bool.ite b l r
+        S_bool.ite b l r
     | Unop (BvExtend (false, by), _) when from_ >= prev_size - by ->
         (* zero extension, and we're extracting only the extended bits *)
         zero size
@@ -1161,7 +1162,7 @@ and BitVec : BitVec = struct
     | Ite (b, l, r) ->
         let l = extend ~signed extend_by l in
         let r = extend ~signed extend_by r in
-        Bool.ite b l r
+        S_bool.ite b l r
     (* can't extend if signed && n == 1, as it should be all 1s *)
     | Unop (BvOfBool n, b) when Stdlib.not signed || n > 1 -> of_bool to_ b
     (* | Unop (BvExtract (_, t), v)
@@ -1204,7 +1205,7 @@ and BitVec : BitVec = struct
       when equal x y ->
         concat left (concat right v2)
     | Ite (b1, l1, r1), Ite (b2, l2, r2) when equal b1 b2 ->
-        Bool.ite b1 (concat l1 l2) (concat r1 r2)
+        S_bool.ite b1 (concat l1 l2) (concat r1 r2)
     | _, _ -> Binop (BvConcat, v1, v2) <| t_bv (n1 + n2)
 
   and shl v1 v2 =
@@ -1260,7 +1261,7 @@ and BitVec : BitVec = struct
     | Ite (b, l, r), BitVec x | BitVec x, Ite (b, l, r) ->
         let n = size_of v1.node.ty in
         let x = mk n x in
-        Bool.ite b (mul l x) (mul r x)
+        S_bool.ite b (mul l x) (mul r x)
     | _ -> mk_commut_binop (Mul { checked }) v1 v2 <| v1.node.ty
 
   let rec div ~signed v1 v2 =
@@ -1307,8 +1308,8 @@ and BitVec : BitVec = struct
     let bits = size_of v1.node.ty in
     match (v1.node.kind, v2.node.kind) with
     | BitVec l, BitVec r ->
-        Bool.bool @@ Z.lt (bv_to_z signed bits l) (bv_to_z signed bits r)
-    | _ when equal v1 v2 -> Bool.v_false
+        S_bool.of_bool @@ Z.lt (bv_to_z signed bits l) (bv_to_z signed bits r)
+    | _ when equal v1 v2 -> S_bool.v_false
     | ( BitVec _,
         ( Binop
             ( Add { checked = true },
@@ -1369,31 +1370,33 @@ and BitVec : BitVec = struct
         lt ~signed (zero bits) b
     | _, BitVec x when Stdlib.not signed && Z.(equal x one) ->
         (* unsigned x < 1 is x == 0 *)
-        Bool.sem_eq v1 (zero bits)
+        S_bool.sem_eq v1 (zero bits)
     (* x < ite(b, 1, 0) => ite(b, x < 1, x < 0) => ite(b, x = 0, false) => b && x = 0 *)
     | _, Unop (BvOfBool n, b) when Stdlib.not signed ->
-        Bool.and_ b (Bool.sem_eq v1 (zero n))
-    | Ite (b, l, r), _ -> Bool.ite b (lt ~signed l v2) (lt ~signed r v2)
-    | _, Ite (b, l, r) -> Bool.ite b (lt ~signed v1 l) (lt ~signed v1 r)
+        S_bool.and_ b (S_bool.sem_eq v1 (zero n))
+    | Ite (b, l, r), _ -> S_bool.ite b (lt ~signed l v2) (lt ~signed r v2)
+    | _, Ite (b, l, r) -> S_bool.ite b (lt ~signed v1 l) (lt ~signed v1 r)
     | _, BitVec x when signed && Z.(equal x zero) ->
         let lt_zero v =
           Binop (Lt signed, v, zero (size_of v.node.ty)) <| TBool
         in
-        let not_eq_0 v = Bool.not (Bool.sem_eq v1 (zero (size_of v.node.ty))) in
+        let not_eq_0 v =
+          S_bool.not (S_bool.sem_eq v1 (zero (size_of v.node.ty)))
+        in
         (* this function returns if this node is negative if we can tell,
            and otherwise the node that represents the sign bit *)
         let rec aux_lt_zero v =
           match v.node.kind with
           | Unop (BvExtend (true, _), v) -> aux_lt_zero v
-          | Unop (BvExtend (false, _), _) -> Bool.v_false
-          | Binop (Mod, _, r) -> Bool.and_ (aux_lt_zero r) (not_eq_0 v)
-          | Binop (Rem true, l, _) -> Bool.and_ (aux_lt_zero l) (not_eq_0 v)
+          | Unop (BvExtend (false, _), _) -> S_bool.v_false
+          | Binop (Mod, _, r) -> S_bool.and_ (aux_lt_zero r) (not_eq_0 v)
+          | Binop (Rem true, l, _) -> S_bool.and_ (aux_lt_zero l) (not_eq_0 v)
           | Binop (Div true, l, r) ->
-              Bool.and_ (not_eq_0 v)
-                (Bool.not (Bool.sem_eq (aux_lt_zero l) (aux_lt_zero r)))
+              S_bool.and_ (not_eq_0 v)
+                (S_bool.not (S_bool.sem_eq (aux_lt_zero l) (aux_lt_zero r)))
           | Binop (BvConcat, l, _) -> aux_lt_zero l
           | Unop (BvNot, v) -> not (aux_lt_zero v)
-          | Unop (BvOfBool n, _) when n > 1 -> Bool.v_false
+          | Unop (BvOfBool n, _) when n > 1 -> S_bool.v_false
           | Ite (_, l, r) ->
               let pos_l = aux_lt_zero l in
               let pos_r = aux_lt_zero r in
@@ -1402,13 +1405,13 @@ and BitVec : BitVec = struct
         in
         aux_lt_zero v1
     | BitVec x, _ when Z.equal (bv_to_z signed bits x) (max_for signed bits) ->
-        Bool.v_false
+        S_bool.v_false
     | _, BitVec x when Z.equal (bv_to_z signed bits x) (min_for signed bits) ->
-        Bool.v_false
+        S_bool.v_false
     | BitVec x, _ when Z.equal (bv_to_z signed bits x) (min_for signed bits) ->
-        Bool.not (Bool.sem_eq v1 v2)
+        S_bool.not (S_bool.sem_eq v1 v2)
     | _, BitVec x when Z.equal (bv_to_z signed bits x) (max_for signed bits) ->
-        Bool.not (Bool.sem_eq v1 v2)
+        S_bool.not (S_bool.sem_eq v1 v2)
     | ( BitVec c2,
         ( Binop
             ( Mul { checked = true },
@@ -1446,7 +1449,7 @@ and BitVec : BitVec = struct
               signed
               && Z.equal c1 (Z.of_int (-1))
               && Z.equal c2 (min_for signed bits)
-            then Bool.v_true
+            then S_bool.v_true
             else lt ~signed x (div ~signed v1 v2)
           else lt ~signed (div ~signed v1 v2) x
         else if Z.lt c1 Z.zero then leq ~signed x (div ~signed v1 v2)
@@ -1487,7 +1490,7 @@ and BitVec : BitVec = struct
               signed
               && Z.equal c1 (Z.of_int (-1))
               && Z.equal c2 (min_for signed bits)
-            then Bool.v_false
+            then S_bool.v_false
             else lt ~signed (div ~signed v2 v1) x
           else lt ~signed x (div ~signed v2 v1)
         else if Z.lt c1 Z.zero then leq ~signed (div ~signed v2 v1) x
@@ -1505,9 +1508,9 @@ and BitVec : BitVec = struct
     assert (equal_ty v1.node.ty v2.node.ty);
     let bits = size_of v1.node.ty in
     match (v1.node.kind, v2.node.kind) with
-    | _ when equal v1 v2 -> Bool.v_true
+    | _ when equal v1 v2 -> S_bool.v_true
     | BitVec l, BitVec r ->
-        Bool.bool @@ Z.leq (bv_to_z signed bits l) (bv_to_z signed bits r)
+        S_bool.of_bool @@ Z.leq (bv_to_z signed bits l) (bv_to_z signed bits r)
     | ( BitVec _,
         ( Binop
             ( Add { checked = true },
@@ -1562,9 +1565,9 @@ and BitVec : BitVec = struct
         let b = if equal v2 v1 then v1' else v1 in
         leq ~signed b (zero bits)
     | BitVec x, _ when Z.equal (bv_to_z signed bits x) (min_for signed bits) ->
-        Bool.v_true
+        S_bool.v_true
     | _, BitVec x when Z.equal (bv_to_z signed bits x) (max_for signed bits) ->
-        Bool.v_true
+        S_bool.v_true
     | ( BitVec c2,
         ( Binop
             ( Mul { checked = true },
@@ -1606,7 +1609,7 @@ and BitVec : BitVec = struct
               signed
               && Z.equal c1 (Z.of_int (-1))
               && Z.equal c2 (min_for signed bits)
-            then Bool.v_true
+            then S_bool.v_true
             else leq ~signed x (div ~signed v1 v2)
           else leq ~signed (div ~signed v1 v2) x
         else if Z.lt c1 Z.zero then
@@ -1654,7 +1657,7 @@ and BitVec : BitVec = struct
               signed
               && Z.equal c1 (Z.of_int (-1))
               && Z.equal c2 (min_for signed bits)
-            then Bool.v_false
+            then S_bool.v_false
             else leq ~signed (div ~signed v2 v1) x
           else leq ~signed x (div ~signed v2 v1)
         else if Z.lt c1 Z.zero then
@@ -1671,11 +1674,11 @@ and BitVec : BitVec = struct
         else leq ~signed l1 l2
     | Binop (Div false, _, { node = { kind = BitVec d; _ }; _ }), BitVec n
       when Stdlib.not signed && Z.(gt (mul n d) (max_for false bits)) ->
-        Bool.v_true
+        S_bool.v_true
     | Ite (b, l, r), BitVec _ ->
-        Bool.ite b (leq ~signed l v2) (leq ~signed r v2)
+        S_bool.ite b (leq ~signed l v2) (leq ~signed r v2)
     | BitVec _, Ite (b, l, r) ->
-        Bool.ite b (leq ~signed v1 l) (leq ~signed v1 r)
+        S_bool.ite b (leq ~signed v1 l) (leq ~signed v1 r)
     | _ -> Binop (Leq signed, v1, v2) <| TBool
 
   let gt ~signed v1 v2 = lt ~signed v2 v1
@@ -1684,8 +1687,8 @@ and BitVec : BitVec = struct
   let add_overflows ~signed v1 v2 =
     match (v1.node.kind, v2.node.kind) with
     | BitVec l, BitVec r -> ovf_check ~signed (size_of v1.node.ty) l r Z.( + )
-    | BitVec z, _ when Z.equal z Z.zero -> Bool.v_false
-    | _, BitVec z when Z.equal z Z.zero -> Bool.v_false
+    | BitVec z, _ when Z.equal z Z.zero -> S_bool.v_false
+    | _, BitVec z when Z.equal z Z.zero -> S_bool.v_false
     | BitVec z, _ when Stdlib.not signed ->
         let n = size_of v1.node.ty in
         let z = bv_to_z signed n z in
@@ -1696,13 +1699,13 @@ and BitVec : BitVec = struct
         let z = bv_to_z signed n z in
         let m = max_for signed n in
         gt ~signed v1 (mk_masked n Z.(m - z))
-    | Unop (BvOfBool _, _), Unop (BvOfBool _, _) -> Bool.v_false
+    | Unop (BvOfBool _, _), Unop (BvOfBool _, _) -> S_bool.v_false
     | Unop (BvOfBool _, b), other | other, Unop (BvOfBool _, b) ->
         (* ite(b, 1, 0) + x only overflows if b && x == max *)
         let n = size_of v1.node.ty in
         let max = max_for signed n in
         let other = other <| t_bv n in
-        Bool.and_ b (Bool.sem_eq other (mk n max))
+        S_bool.and_ b (S_bool.sem_eq other (mk n max))
     | _ ->
         let size = size_of v1.node.ty in
         if signed then
@@ -1710,13 +1713,13 @@ and BitVec : BitVec = struct
           let sign_l = sign_of v1 in
           let sign_r = sign_of v2 in
           let msb_res = sign_of (add v1 v2) in
-          Bool.and_
-            (Bool.sem_eq sign_l sign_r)
-            (Bool.not (Bool.sem_eq sign_l msb_res))
+          S_bool.and_
+            (S_bool.sem_eq sign_l sign_r)
+            (S_bool.not (S_bool.sem_eq sign_l msb_res))
         else
           let max = max_for signed size in
           let max = mk size max in
-          Bool.or_
+          S_bool.or_
             (gt ~signed v1 (sub ~checked:true max v2))
             (gt ~signed v2 (sub ~checked:true max v1))
 
@@ -1726,10 +1729,10 @@ and BitVec : BitVec = struct
     | _
       when if signed then msb_of v1 + msb_of v2 < size_of v1.node.ty - 1
            else msb_of v1 + msb_of v2 < size_of v1.node.ty ->
-        Bool.v_false
+        S_bool.v_false
     | BitVec z, x | x, BitVec z ->
         (* z is a known constant *)
-        if Z.equal z Z.zero || Z.equal z Z.one then Bool.v_false
+        if Z.equal z Z.zero || Z.equal z Z.one then S_bool.v_false
         else
           let n = size_of v1.node.ty in
           let z = bv_to_z signed n z in
@@ -1759,7 +1762,7 @@ and BitVec : BitVec = struct
                 let max_x = Z.(min_val / z) in
                 (min_x, max_x)
             in
-            Bool.or_
+            S_bool.or_
               (lt ~signed (x <| v1.node.ty) (mk_masked n min_x))
               (gt ~signed (x <| v1.node.ty) (mk_masked n max_x))
           else
@@ -1771,7 +1774,7 @@ and BitVec : BitVec = struct
 
   let neg_overflows v =
     let n = size_of v.node.ty in
-    Bool.sem_eq (mk_masked n (min_for true n)) v
+    S_bool.sem_eq (mk_masked n (min_for true n)) v
 
   let sub_overflows ~signed v1 v2 =
     if Stdlib.not signed then lt ~signed v1 v2
@@ -1779,7 +1782,7 @@ and BitVec : BitVec = struct
       let neg_ovf = neg_overflows v2 in
       let neg_v2 = neg v2 in
       let add_ovf = add_overflows ~signed v1 neg_v2 in
-      Bool.or_ neg_ovf add_ovf
+      S_bool.or_ neg_ovf add_ovf
 
   let of_float ~rounding ~signed ~size v =
     let p = precision_of_f v.node.ty in
@@ -1815,12 +1818,12 @@ and Float : Float = struct
 
   let lt v1 v2 =
     match (v1.node.kind, v2.node.kind) with
-    | Float f1, Float f2 -> Bool.bool (str2f f1 < str2f f2)
+    | Float f1, Float f2 -> S_bool.of_bool (str2f f1 < str2f f2)
     | _ -> Binop (FLt, v1, v2) <| TBool
 
   let leq v1 v2 =
     match (v1.node.kind, v2.node.kind) with
-    | Float f1, Float f2 -> Bool.bool (str2f f1 <= str2f f2)
+    | Float f1, Float f2 -> S_bool.of_bool (str2f f1 <= str2f f2)
     | _ -> Binop (FLeq, v1, v2) <| TBool
 
   let gt v1 v2 = lt v2 v1
@@ -1843,7 +1846,8 @@ and Float : Float = struct
   let[@inline] is_floatclass fc =
    fun sv ->
     match sv.node.kind with
-    | Float f -> Bool.bool (FloatClass.as_fpclass fc = classify_float (str2f f))
+    | Float f ->
+        S_bool.of_bool (FloatClass.as_fpclass fc = classify_float (str2f f))
     | _ -> Unop (FIs fc, sv) <| TBool
 
   let is_normal = is_floatclass Normal
@@ -1867,7 +1871,7 @@ module Ptr = struct
     | _ -> Unop (GetPtrLoc, p) <| TLoc (size_of p.node.ty)
 
   let null_loc n = BitVec Z.zero <| TLoc n
-  let is_null_loc l = Bool.sem_eq l (null_loc (size_of l.node.ty))
+  let is_null_loc l = S_bool.sem_eq l (null_loc (size_of l.node.ty))
   let loc_of_z n z = BitVec z <| TLoc n
   let loc_of_int n i = loc_of_z n (Z.of_int i)
 
@@ -1886,7 +1890,7 @@ module Ptr = struct
     mk loc (BitVec.add ofs o)
 
   let null n = mk (null_loc n) (BitVec.zero n)
-  let is_null p = Bool.sem_eq p (null (size_of p.node.ty))
+  let is_null p = S_bool.sem_eq p (null (size_of p.node.ty))
   let is_at_null_loc p = is_null_loc (loc p)
 end
 
@@ -1905,10 +1909,10 @@ module Infix = struct
   let bv_z = BitVec.mk
   let ptr = Ptr.mk
   let seq = SSeq.mk
-  let ( ==@ ) = Bool.sem_eq
-  let ( ==?@ ) = Bool.sem_eq_untyped
-  let ( &&@ ) = Bool.and_
-  let ( ||@ ) = Bool.or_
+  let ( ==@ ) = S_bool.sem_eq
+  let ( ==?@ ) = S_bool.sem_eq_untyped
+  let ( &&@ ) = S_bool.and_
+  let ( ||@ ) = S_bool.or_
   let ( >@ ) = BitVec.gt ~signed:false
   let ( >=@ ) = BitVec.geq ~signed:false
   let ( <@ ) = BitVec.lt ~signed:false
diff --git a/soteria/lib/bv_values/typed.ml b/soteria/lib/bv_values/typed.ml
index c786fd569..637be17d2 100644
--- a/soteria/lib/bv_values/typed.ml
+++ b/soteria/lib/bv_values/typed.ml
@@ -29,11 +29,17 @@ end
 
 type nonrec +'a t = t
 type nonrec +'a ty = ty
-type sbool = T.sbool
 
 let t_int = t_bv
 
-include Bool
+include S_bool
+
+module S_bool = struct
+  type +'a v = 'a t
+  type t = T.sbool
+
+  include S_bool
+end
 
 let[@inline] get_ty x = x.node.ty
 let[@inline] type_type x = x
@@ -65,6 +71,8 @@ module BitVec = struct
 
   let mki_nz n i =
     if i = 0 then failwith "Zero value in mki_nonzero" else mki_masked n i
+
+  let assume_not_overflowed v = v
 end
 
 module Infix = struct
diff --git a/soteria/lib/bv_values/typed.mli b/soteria/lib/bv_values/typed.mli
index 96d3d5aba..a683df078 100644
--- a/soteria/lib/bv_values/typed.mli
+++ b/soteria/lib/bv_values/typed.mli
@@ -62,7 +62,10 @@ val t_float : Svalue.FloatPrecision.t -> [> sfloat ] ty
 (** {2 Typed svalues} *)
 
 type +'a t
-type sbool = T.sbool
+
+module S_bool : Symex.Value.S_bool.S with type 'a v = 'a t and type t = sbool
+
+type sbool := T.sbool
 
 (** Basic value operations *)
 
@@ -96,12 +99,8 @@ val sem_eq : 'a t -> 'a t -> sbool t
 val sem_eq_untyped : 'a t -> 'a t -> [> sbool ] t
 val v_true : [> sbool ] t
 val v_false : [> sbool ] t
-val bool : bool -> [> sbool ] t
-val as_bool : 'a t -> bool option
-val and_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t
 val conj : [< sbool ] t list -> [> sbool ] t
 val split_ands : [< sbool ] t -> ([> sbool ] t -> unit) -> unit
-val or_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t
 val not : sbool t -> sbool t
 val distinct : 'a t list -> [> sbool ] t
 val ite : [< sbool ] t -> 'a t -> 'a t -> 'a t
@@ -135,6 +134,7 @@ module BitVec : sig
   val sub_overflows : signed:bool -> [< sint ] t -> [< sint ] t -> [> sbool ] t
   val mul_overflows : signed:bool -> [< sint ] t -> [< sint ] t -> [> sbool ] t
   val neg_overflows : [< sint ] t -> [> sbool ] t
+  val assume_not_overflowed : [< sint_ovf ] t -> [> sint ] t
 
   (* inequalities *)
   val lt : signed:bool -> [< sint ] t -> [< sint ] t -> [> sbool ] t
diff --git a/soteria/lib/c_values/analyses.ml b/soteria/lib/c_values/analyses.ml
index b95e13447..250cf90e8 100644
--- a/soteria/lib/c_values/analyses.ml
+++ b/soteria/lib/c_values/analyses.ml
@@ -10,7 +10,7 @@ module type S = sig
 
   val simplify : t -> Svalue.t -> Svalue.t
   val add_constraint : t -> Svalue.t -> Svalue.t * Var.Set.t
-  val encode : ?vars:Var.Hashset.t -> t -> Typed.sbool Typed.t Iter.t
+  val encode : ?vars:Var.Hashset.t -> t -> Typed.S_bool.t Typed.t Iter.t
 end
 
 module Merge (A1 : S) (A2 : S) : S = struct
@@ -37,7 +37,7 @@ module Merge (A1 : S) (A2 : S) : S = struct
     let v'', vars2 = A2.add_constraint a2 v' in
     (v'', Var.Set.union vars1 vars2)
 
-  let encode ?vars (a1, a2) : Typed.sbool Typed.t Iter.t =
+  let encode ?vars (a1, a2) : Typed.S_bool.t Typed.t Iter.t =
     Iter.append (A1.encode ?vars a1) (A2.encode ?vars a2)
 end
 
@@ -208,7 +208,7 @@ module Interval : S = struct
                 (if neg then "/" else "∩")
                 Range.pp range' Range.pp new_range);
           let is_ok = not (Range.is_empty range) in
-          ((Svalue.bool (is_ok <> neg), Var.Set.empty), st)
+          ((Svalue.S_bool.of_bool (is_ok <> neg), Var.Set.empty), st)
       | Some new_range -> (
           let st' = Var.Map.add var new_range st in
           log (fun m ->
@@ -221,7 +221,7 @@ module Interval : S = struct
               let eq = Svalue.int_z m ==@ mk_var var in
               (* this is hacky; we found the exact value, but we can't return the equality
                  if we're negating, since that equality will otherwise be negated. *)
-              (((if neg then Svalue.not eq else eq), Var.Set.empty), st')
+              (((if neg then Svalue.S_bool.not eq else eq), Var.Set.empty), st')
           (* The range is empty, so this cannot be true *)
           | _ when Range.is_empty new_range ->
               ((Svalue.v_false, Var.Set.empty), st')
@@ -233,7 +233,8 @@ module Interval : S = struct
           (* We could cleanly absorb the range, so the PC doesn't need to store it -- however
              we must mark this variable as dirty, as maybe the modified range still renders
              the branch infeasible, e.g. because of some additional PC assertions. *)
-          | _ -> ((Svalue.bool (not neg), Var.Set.singleton var), st'))
+          | _ -> ((Svalue.S_bool.of_bool (not neg), Var.Set.singleton var), st')
+          )
     in
     match v.node.kind with
     | Binop
@@ -260,7 +261,7 @@ module Interval : S = struct
     (* We conservatively explore negations; we're only interested in simple (in)equalities *)
     | Unop (Not, nv) ->
         let (nv', vars), st' = add_constraint ~absorb ~neg:(not neg) nv st in
-        ((Svalue.not nv', vars), st')
+        ((Svalue.S_bool.not nv', vars), st')
     (* We don't explore && and || within negations, because that becomes messy. *)
     | Binop (And, v1, v2) when not neg ->
         let (v1', vars1), st' = add_constraint ~absorb v1 st in
@@ -289,7 +290,7 @@ module Interval : S = struct
 
   (** Encode all the information relevant to the given variables and conjuncts
       them with the given accumulator. *)
-  let encode ?vars st : Typed.sbool Typed.t Iter.t =
+  let encode ?vars st : Typed.S_bool.t Typed.t Iter.t =
     let to_check =
       Option.fold ~none:(fun _ -> true) ~some:Var.Hashset.mem vars
     in
diff --git a/soteria/lib/c_values/c_solver.ml b/soteria/lib/c_values/c_solver.ml
index 98033a3d1..40267a9c2 100644
--- a/soteria/lib/c_values/c_solver.ml
+++ b/soteria/lib/c_values/c_solver.ml
@@ -16,7 +16,7 @@ struct
   end)
 
   module Solver_state = struct
-    type t = Typed.sbool Typed.t Dynarray.t Dynarray.t
+    type t = Typed.S_bool.t Typed.t Dynarray.t Dynarray.t
 
     let init () =
       let t = Dynarray.create () in
@@ -57,8 +57,8 @@ struct
 
     let iter (t : t) f = Dynarray.iter (fun t -> Dynarray.iter f t) t
 
-    let trivial_truthiness_of (t : t) (v : Typed.sbool Typed.t) =
-      let neg_v = Typed.not v in
+    let trivial_truthiness_of (t : t) (v : Typed.S_bool.t Typed.t) =
+      let neg_v = Typed.S_bool.not v in
       Dynarray.find_map
         (Dynarray.find_map (fun value ->
              if Typed.equal value v then Some true
@@ -134,7 +134,7 @@ struct
             match v.node.kind with
             | Unop (Not, e) ->
                 let e' = simplify' solver e in
-                if Svalue.equal e e' then v else Svalue.not e'
+                if Svalue.equal e e' then v else Svalue.S_bool.not e'
             | Binop (Eq, e1, e2) ->
                 if Svalue.equal e1 e2 && (not @@ Svalue.is_float e1.node.ty)
                 then Svalue.v_true
@@ -144,7 +144,7 @@ struct
                 let se1 = simplify' solver e1 in
                 let se2 = simplify' solver e2 in
                 if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v
-                else Svalue.or_ se1 se2
+                else Svalue.S_bool.or_ se1 se2
             | _ -> Analysis.simplify solver.analysis v))
 
   and simplify solver (v : 'a Typed.t) : 'a Typed.t =
@@ -199,7 +199,7 @@ struct
         instance because an auxiliary analysis has new information about it that
         is not directly in the PC. *)
     type slot_content =
-      | Asrt of Typed.sbool Typed.t [@printer Typed.ppa]
+      | Asrt of Typed.S_bool.t Typed.t [@printer Typed.ppa]
       | Dirty of Var.Set.t [@printer Fmt.(iter ~sep:comma) Var.Set.iter Var.pp]
     [@@deriving show]
 
@@ -262,8 +262,8 @@ struct
       | _ -> None
 
     (* We check if the thing contains the value itself, or its negation. *)
-    let trivial_truthiness_of (t : t) (v : Typed.sbool Typed.t) =
-      let neg_v = Typed.not v in
+    let trivial_truthiness_of (t : t) (v : Typed.S_bool.t Typed.t) =
+      let neg_v = Typed.S_bool.not v in
       Dynarray.find_map
         (Dynarray.find_map (function
           | { value = Asrt value; _ } ->
@@ -450,7 +450,7 @@ struct
             match v.node.kind with
             | Unop (Not, e) ->
                 let e' = simplify' solver e in
-                if Svalue.equal e e' then v else Svalue.not e'
+                if Svalue.equal e e' then v else Svalue.S_bool.not e'
             | Binop (Eq, e1, e2) ->
                 if Svalue.equal e1 e2 && (not @@ Svalue.is_float e1.node.ty)
                 then Svalue.v_true
@@ -460,12 +460,12 @@ struct
                 let se1 = simplify' solver e1 in
                 let se2 = simplify' solver e2 in
                 if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v
-                else Svalue.and_ se1 se2
+                else Svalue.S_bool.and_ se1 se2
             | Binop (Or, e1, e2) ->
                 let se1 = simplify' solver e1 in
                 let se2 = simplify' solver e2 in
                 if Svalue.equal se1 e1 && Svalue.equal se2 e2 then v
-                else Svalue.or_ se1 se2
+                else Svalue.S_bool.or_ se1 se2
             | Ite (g, e1, e2) ->
                 let sg = simplify' solver g in
                 let se1 = simplify' solver e1 in
@@ -557,9 +557,11 @@ struct
           Solver_state.unchecked_constraints solver.state
         in
         (* This will put the check in a somewhat-normal form, to increase cache hits. *)
-        let to_check = Dynarray.fold_left Typed.and_ Typed.v_true to_check in
         let to_check =
-          Iter.fold Typed.and_ to_check
+          Dynarray.fold_left Typed.S_bool.and_ Typed.v_true to_check
+        in
+        let to_check =
+          Iter.fold Typed.S_bool.and_ to_check
             (Analysis.encode ~vars:relevant_vars solver.analysis)
         in
         let answer = check_sat_raw_memo solver relevant_vars to_check in
diff --git a/soteria/lib/c_values/eval.ml b/soteria/lib/c_values/eval.ml
index 5517ff96e..79254d24e 100644
--- a/soteria/lib/c_values/eval.ml
+++ b/soteria/lib/c_values/eval.ml
@@ -7,8 +7,8 @@ let eval_var (v : Var.t) (ty : Svalue.ty) : t =
   Effect.perform (Eval_var (v, ty))
 
 let eval_binop : Binop.t -> t -> t -> t = function
-  | And -> and_
-  | Or -> or_
+  | And -> S_bool.and_
+  | Or -> S_bool.or_
   | Eq -> sem_eq
   | Leq -> leq
   | Lt -> lt
@@ -45,7 +45,7 @@ let eval_binop : Binop.t -> t -> t -> t = function
   | BitAShr -> BitVec.Raw.ashr
 
 let eval_unop : Unop.t -> t -> t = function
-  | Not -> not
+  | Not -> S_bool.not
   | FAbs -> Float.abs
   | GetPtrLoc -> Ptr.loc
   | GetPtrOfs -> Ptr.ofs
diff --git a/soteria/lib/c_values/svalue.ml b/soteria/lib/c_values/svalue.ml
index 2ee447faf..f2b3cf306 100644
--- a/soteria/lib/c_values/svalue.ml
+++ b/soteria/lib/c_values/svalue.ml
@@ -369,45 +369,47 @@ let rec subst subst_var sv =
 let v_true = Bool true <| TBool
 let v_false = Bool false <| TBool
 
-let as_bool t =
-  if equal t v_true then Some true
-  else if equal t v_false then Some false
-  else None
+module S_bool = struct
+  let to_bool t =
+    if equal t v_true then Some true
+    else if equal t v_false then Some false
+    else None
 
-let bool b =
-  (* avoid re-alloc and re-hashconsing *)
-  if b then v_true else v_false
+  let of_bool b =
+    (* avoid re-alloc and re-hashconsing *)
+    if b then v_true else v_false
 
-let and_ v1 v2 =
-  match (v1.node.kind, v2.node.kind) with
-  | _, _ when equal v1 v2 -> v1
-  | Bool false, _ | _, Bool false -> v_false
-  | Bool true, _ -> v2
-  | _, Bool true -> v1
-  | _ -> mk_commut_binop And v1 v2 <| TBool
-
-let or_ v1 v2 =
-  match (v1.node.kind, v2.node.kind) with
-  | Bool true, _ | _, Bool true -> v_true
-  | Bool false, _ -> v2
-  | _, Bool false -> v1
-  | _ -> mk_commut_binop Or v1 v2 <| TBool
+  let and_ v1 v2 =
+    match (v1.node.kind, v2.node.kind) with
+    | _, _ when equal v1 v2 -> v1
+    | Bool false, _ | _, Bool false -> v_false
+    | Bool true, _ -> v2
+    | _, Bool true -> v1
+    | _ -> mk_commut_binop And v1 v2 <| TBool
 
-let conj l = List.fold_left and_ v_true l
+  let or_ v1 v2 =
+    match (v1.node.kind, v2.node.kind) with
+    | Bool true, _ | _, Bool true -> v_true
+    | Bool false, _ -> v2
+    | _, Bool false -> v1
+    | _ -> mk_commut_binop Or v1 v2 <| TBool
+
+  let rec not sv =
+    if equal sv v_true then v_false
+    else if equal sv v_false then v_true
+    else
+      match sv.node.kind with
+      | Unop (Not, sv) -> sv
+      | Binop (Lt, v1, v2) -> Binop (Leq, v2, v1) <| TBool
+      | Binop (Leq, v1, v2) -> Binop (Lt, v2, v1) <| TBool
+      | Binop (BvLt s, v1, v2) -> Binop (BvLeq s, v2, v1) <| TBool
+      | Binop (BvLeq s, v1, v2) -> Binop (BvLt s, v2, v1) <| TBool
+      | Binop (Or, v1, v2) -> mk_commut_binop And (not v1) (not v2) <| TBool
+      | Binop (And, v1, v2) -> mk_commut_binop Or (not v1) (not v2) <| TBool
+      | _ -> Unop (Not, sv) <| TBool
+end
 
-let rec not sv =
-  if equal sv v_true then v_false
-  else if equal sv v_false then v_true
-  else
-    match sv.node.kind with
-    | Unop (Not, sv) -> sv
-    | Binop (Lt, v1, v2) -> Binop (Leq, v2, v1) <| TBool
-    | Binop (Leq, v1, v2) -> Binop (Lt, v2, v1) <| TBool
-    | Binop (BvLt s, v1, v2) -> Binop (BvLeq s, v2, v1) <| TBool
-    | Binop (BvLeq s, v1, v2) -> Binop (BvLt s, v2, v1) <| TBool
-    | Binop (Or, v1, v2) -> mk_commut_binop And (not v1) (not v2) <| TBool
-    | Binop (And, v1, v2) -> mk_commut_binop Or (not v1) (not v2) <| TBool
-    | _ -> Unop (Not, sv) <| TBool
+let conj l = List.fold_left S_bool.and_ v_true l
 
 let rec split_ands (sv : t) (f : t -> unit) : unit =
   match sv.node.kind with
@@ -432,11 +434,11 @@ let ite guard if_ else_ =
   | Bool true, _, _ -> if_
   | Bool false, _, _ -> else_
   | _, Bool true, Bool false -> guard
-  | _, Bool false, Bool true -> not guard
-  | _, Bool false, _ -> and_ (not guard) else_
-  | _, Bool true, _ -> or_ guard else_
-  | _, _, Bool false -> and_ guard if_
-  | _, _, Bool true -> or_ (not guard) if_
+  | _, Bool false, Bool true -> S_bool.not guard
+  | _, Bool false, _ -> S_bool.and_ (S_bool.not guard) else_
+  | _, Bool true, _ -> S_bool.or_ guard else_
+  | _, _, Bool false -> S_bool.and_ guard if_
+  | _, _, Bool true -> S_bool.or_ (S_bool.not guard) if_
   | _, Int o, Int z when Z.equal o Z.one && Z.equal z Z.zero ->
       Unop (IntOfBool, guard) <| TInt
   | _ when equal if_ else_ -> if_
@@ -445,6 +447,7 @@ let ite guard if_ else_ =
 (** {2 Integers} *)
 
 let int_z z = Int z <| TInt
+let to_z v = match v.node.kind with Int z -> Some z | _ -> None
 let int i = int_z (Z.of_int i)
 
 let nonzero_z z =
@@ -569,9 +572,8 @@ let neg v =
     to be seamlessly used on [TInt], without worrying about the underlying
     representation.*)
 module BitVec = struct
-  let bool_or = or_
-  let bool_and = and_
-  let bool_not = not
+  let bool_or = S_bool.or_
+  let bool_and = S_bool.and_
 
   (** Raw operations for values of type [TBitVector]; be careful when using
       these, so as to provide properly typed values. Prefer using [BitVec]
@@ -772,7 +774,7 @@ module BitVec = struct
              && Z.(equal r1 zero)
              && Z.(equal r2 zero) ->
           ite
-            (bool_not (mk_commut_binop Eq b1 b2 <| TBool))
+            (S_bool.not (mk_commut_binop Eq b1 b2 <| TBool))
             (mk_like v1 Z.one) (mk_like v1 Z.zero)
       | _ -> mk_commut_binop BitXor v1 v2 <| v1.node.ty
 
@@ -898,7 +900,7 @@ module BitVec = struct
       let bits = size_of_bv v1.node.ty in
       match (v1.node.kind, v2.node.kind) with
       | BitVec l, BitVec r ->
-          bool @@ Z.lt (bv_to_z signed bits l) (bv_to_z signed bits r)
+          S_bool.of_bool @@ Z.lt (bv_to_z signed bits l) (bv_to_z signed bits r)
       | _, BitVec x when Stdlib.not signed && Z.(equal x one) ->
           (* unsigned x < 1 is x == 0 *)
           mk_commut_binop Eq v1 (mk_like v1 Z.zero) <| TBool
@@ -916,7 +918,8 @@ module BitVec = struct
       let bits = size_of_bv v1.node.ty in
       match (v1.node.kind, v2.node.kind) with
       | BitVec l, BitVec r ->
-          bool @@ Z.leq (bv_to_z signed bits l) (bv_to_z signed bits r)
+          S_bool.of_bool
+          @@ Z.leq (bv_to_z signed bits l) (bv_to_z signed bits r)
       | BitVec x, _ when Z.equal (bv_to_z signed bits x) (min_for signed bits)
         ->
           v_true
@@ -1044,7 +1047,7 @@ module BitVec = struct
           { node = { kind = BitVec l; _ }; _ },
           { node = { kind = BitVec r; _ }; _ } )
       when Z.equal l Z.zero && Z.equal r Z.one ->
-        int_of_bool (not b)
+        int_of_bool (S_bool.not b)
     | Ite (b, t, e) -> ite b (to_int signed t) (to_int signed e)
     | _ -> Unop (IntOfBv signed, v) <| t_int
 
@@ -1056,7 +1059,7 @@ module BitVec = struct
   let and_ ~size ~signed v1 v2 =
     match (v1.node.kind, v2.node.kind) with
     | Int i1, Int i2 -> int_z (Z.( land ) i1 i2)
-    | Bool b1, Bool b2 -> bool (b1 && b2)
+    | Bool b1, Bool b2 -> S_bool.of_bool (b1 && b2)
     | _ ->
         let v1_bv = of_int signed size v1 in
         let v2_bv = of_int signed size v2 in
@@ -1066,7 +1069,7 @@ module BitVec = struct
   let or_ ~size ~signed v1 v2 =
     match (v1.node.kind, v2.node.kind) with
     | Int i1, Int i2 -> int_z (Z.( lor ) i1 i2)
-    | Bool b1, Bool b2 -> bool (b1 || b2)
+    | Bool b1, Bool b2 -> S_bool.of_bool (b1 || b2)
     | _ ->
         let v1_bv = of_int signed size v1 in
         let v2_bv = of_int signed size v2 in
@@ -1076,7 +1079,7 @@ module BitVec = struct
   let xor ~size ~signed v1 v2 =
     match (v1.node.kind, v2.node.kind) with
     | Int i1, Int i2 -> int_z (Z.( lxor ) i1 i2)
-    | Bool b1, Bool b2 -> bool (b1 <> b2)
+    | Bool b1, Bool b2 -> S_bool.of_bool (b1 <> b2)
     | _ ->
         let v1_bv = of_int signed size v1 in
         let v2_bv = of_int signed size v2 in
@@ -1138,12 +1141,14 @@ module Float = struct
 
   let lt v1 v2 =
     match (v1.node.kind, v2.node.kind) with
-    | Float f1, Float f2 -> bool (float_of_string f1 < float_of_string f2)
+    | Float f1, Float f2 ->
+        S_bool.of_bool (float_of_string f1 < float_of_string f2)
     | _ -> Binop (FLt, v1, v2) <| TBool
 
   let leq v1 v2 =
     match (v1.node.kind, v2.node.kind) with
-    | Float f1, Float f2 -> bool (float_of_string f1 <= float_of_string f2)
+    | Float f1, Float f2 ->
+        S_bool.of_bool (float_of_string f1 <= float_of_string f2)
     | _ -> Binop (FLeq, v1, v2) <| TBool
 
   let gt v1 v2 = lt v2 v1
@@ -1167,7 +1172,8 @@ module Float = struct
    fun sv ->
     match sv.node.kind with
     | Float f ->
-        bool (FloatClass.as_fpclass fc = classify_float (float_of_string f))
+        S_bool.of_bool
+          (FloatClass.as_fpclass fc = classify_float (float_of_string f))
     | _ -> Unop (FIs fc, sv) <| TBool
 
   let is_normal = is_floatclass Normal
@@ -1200,7 +1206,7 @@ end
 
 let rec lt v1 v2 =
   match (v1.node.kind, v2.node.kind) with
-  | Int i1, Int i2 -> bool (Z.lt i1 i2)
+  | Int i1, Int i2 -> S_bool.of_bool (Z.lt i1 i2)
   | _, _ when equal v1 v2 -> v_false
   | _, Binop (Plus, v2, v3) when equal v1 v2 -> lt zero v3
   | _, Binop (Plus, v2, v3) when equal v1 v3 -> lt zero v2
@@ -1226,14 +1232,14 @@ let rec lt v1 v2 =
       lt v1 (int_z @@ Z.sub x y)
   | Int y, Binop (Times, { node = { kind = Int x; _ }; _ }, v1')
   | Int y, Binop (Times, v1', { node = { kind = Int x; _ }; _ }) ->
-      if Z.equal Z.zero x then bool (Z.lt y Z.zero)
+      if Z.equal Z.zero x then S_bool.of_bool (Z.lt y Z.zero)
       else
         let op = if Z.divisible y x || Z.(y > zero) then lt else leq in
         if Z.(zero < x) then op (int_z Z.(y / x)) v1'
         else op v1' (int_z Z.(y / x))
   | Binop (Times, v1', { node = { kind = Int x; _ }; _ }), Int y
   | Binop (Times, { node = { kind = Int x; _ }; _ }, v1'), Int y ->
-      if Z.equal Z.zero x then bool (Z.lt Z.zero y)
+      if Z.equal Z.zero x then S_bool.of_bool (Z.lt Z.zero y)
       else
         let op = if Z.divisible y x || Z.(y < zero) then lt else leq in
         if Z.(zero < x) then op v1' (int_z Z.(y / x))
@@ -1247,7 +1253,10 @@ let rec lt v1 v2 =
   | Int z, Unop (IntOfBool, b) -> (
       match Z.(compare z zero) with 0 -> b | 1 -> v_false | _ -> v_true)
   | Unop (IntOfBool, b), Int z -> (
-      match Z.(compare z one) with 0 -> not b | 1 -> v_true | _ -> v_false)
+      match Z.(compare z one) with
+      | 0 -> S_bool.not b
+      | 1 -> v_true
+      | _ -> v_false)
   | Int _, Ite (b, t, e) -> ite b (lt v1 t) (lt v1 e)
   | Ite (b, t, e), Int _ -> ite b (lt t v2) (lt e v2)
   | _ -> (
@@ -1257,7 +1266,7 @@ let rec lt v1 v2 =
 
 and leq v1 v2 =
   match (v1.node.kind, v2.node.kind) with
-  | Int i1, Int i2 -> bool (Z.leq i1 i2)
+  | Int i1, Int i2 -> S_bool.of_bool (Z.leq i1 i2)
   | _, _ when equal v1 v2 -> v_true
   | _, Binop (Plus, v2, v3) when equal v1 v2 -> leq zero v3
   | _, Binop (Plus, v2, v3) when equal v1 v3 -> leq zero v2
@@ -1281,14 +1290,14 @@ and leq v1 v2 =
       leq v1 (int_z @@ Z.sub x y)
   | Int y, Binop (Times, { node = { kind = Int x; _ }; _ }, v1')
   | Int y, Binop (Times, v1', { node = { kind = Int x; _ }; _ }) ->
-      if Z.equal Z.zero x then bool (Z.lt y Z.zero)
+      if Z.equal Z.zero x then S_bool.of_bool (Z.lt y Z.zero)
       else
         let op = if Z.divisible y x || Z.(y < zero) then leq else lt in
         if Z.(zero < x) then op (int_z Z.(y / x)) v1'
         else op v1' (int_z Z.(y / x))
   | Binop (Times, v1', { node = { kind = Int x; _ }; _ }), Int y
   | Binop (Times, { node = { kind = Int x; _ }; _ }, v1'), Int y ->
-      if Z.equal Z.zero x then bool (Z.lt y Z.zero)
+      if Z.equal Z.zero x then S_bool.of_bool (Z.lt y Z.zero)
       else
         let op = if Z.divisible y x || Z.(y > zero) then leq else lt in
         if Z.(zero < x) then op v1' (int_z Z.(y / x))
@@ -1310,7 +1319,10 @@ and leq v1 v2 =
   | Int z, Unop (IntOfBool, b) -> (
       match Z.(compare z one) with 0 -> b | 1 -> v_false | _ -> v_true)
   | Unop (IntOfBool, b), Int z -> (
-      match Z.(compare z zero) with 0 -> not b | 1 -> v_true | _ -> v_false)
+      match Z.(compare z zero) with
+      | 0 -> S_bool.not b
+      | 1 -> v_true
+      | _ -> v_false)
   | Int _, Ite (b, t, e) -> ite b (leq v1 t) (leq v1 e)
   | Ite (b, t, e), Int _ -> ite b (leq t v2) (leq e v2)
   | _ -> (
@@ -1325,10 +1337,10 @@ let rec sem_eq v1 v2 =
   if equal v1 v2 && Stdlib.not (is_float v1.node.ty) then v_true
   else
     match (v1.node.kind, v2.node.kind) with
-    | Int z1, Int z2 -> bool (Z.equal z1 z2)
-    | Bool b1, Bool b2 -> bool (b1 = b2)
-    | Ptr (l1, o1), Ptr (l2, o2) -> and_ (sem_eq l1 l2) (sem_eq o1 o2)
-    | BitVec b1, BitVec b2 -> bool (Z.equal b1 b2)
+    | Int z1, Int z2 -> S_bool.of_bool (Z.equal z1 z2)
+    | Bool b1, Bool b2 -> S_bool.of_bool (b1 = b2)
+    | Ptr (l1, o1), Ptr (l2, o2) -> S_bool.and_ (sem_eq l1 l2) (sem_eq o1 o2)
+    | BitVec b1, BitVec b2 -> S_bool.of_bool (Z.equal b1 b2)
     | _, Binop (Plus, v2, v3) when equal v1 v2 -> sem_eq v3 zero
     | _, Binop (Plus, v2, v3) when equal v1 v3 -> sem_eq v2 zero
     | Binop (Plus, v1, v3), _ when equal v1 v2 -> sem_eq v3 zero
@@ -1353,10 +1365,11 @@ let rec sem_eq v1 v2 =
     | Int y, Binop (Times, v1, { node = { kind = Int x; _ }; _ })
     | Binop (Times, v1, { node = { kind = Int x; _ }; _ }), Int y
     | Binop (Times, { node = { kind = Int x; _ }; _ }, v1), Int y ->
-        if Z.equal Z.zero x then bool (Z.equal Z.zero y)
+        if Z.equal Z.zero x then S_bool.of_bool (Z.equal Z.zero y)
         else if Z.(equal zero (rem y x)) then sem_eq v1 (int_z Z.(y / x))
         else v_false
-    | Unop (IntOfBool, v1), Int z -> if Z.equal Z.zero z then not v1 else v1
+    | Unop (IntOfBool, v1), Int z ->
+        if Z.equal Z.zero z then S_bool.not v1 else v1
     | Unop (IntOfBool, b1), Unop (IntOfBool, b2) -> sem_eq b1 b2
     (* Reduce  (X & #x...N) = #x...M to (X & #xN) = #xM *)
     | Binop (BitAnd, _, _), _ | _, Binop (BitAnd, _, _) -> (
@@ -1413,14 +1426,14 @@ let sem_eq_untyped v1 v2 =
 let not_int_bool sv =
   match sv.node.kind with
   | Int z -> if Z.equal z Z.zero then one else zero
-  | Unop (IntOfBool, sv') -> int_of_bool (not sv')
+  | Unop (IntOfBool, sv') -> int_of_bool (S_bool.not sv')
   | _ -> int_of_bool (sem_eq sv zero)
 
 let bool_of_int sv =
   match sv.node.kind with
-  | Int z -> bool (Stdlib.not (Z.equal z Z.zero))
+  | Int z -> S_bool.of_bool (Stdlib.not (Z.equal z Z.zero))
   | Unop (IntOfBool, sv') -> sv'
-  | _ -> not (sem_eq sv zero)
+  | _ -> S_bool.not (sem_eq sv zero)
 
 (** {2 Pointers} *)
 
@@ -1472,8 +1485,8 @@ module Infix = struct
   let ( >=@ ) = geq
   let ( <@ ) = lt
   let ( <=@ ) = leq
-  let ( &&@ ) = and_
-  let ( ||@ ) = or_
+  let ( &&@ ) = S_bool.and_
+  let ( ||@ ) = S_bool.or_
   let ( +@ ) = plus
   let ( -@ ) = minus
   let ( ~- ) = neg
diff --git a/soteria/lib/c_values/typed.ml b/soteria/lib/c_values/typed.ml
index f3cf11c27..f78aa7cd3 100644
--- a/soteria/lib/c_values/typed.ml
+++ b/soteria/lib/c_values/typed.ml
@@ -26,7 +26,13 @@ end
 
 type nonrec +'a t = t
 type nonrec +'a ty = ty
-type sbool = T.sbool
+
+module S_bool = struct
+  type +'a v = 'a t
+  type t = T.sbool
+
+  include S_bool
+end
 
 let[@inline] get_ty x = x.node.ty
 let[@inline] untype_type x = x
diff --git a/soteria/lib/c_values/typed.mli b/soteria/lib/c_values/typed.mli
index 2db2d78b4..5f95bd7ba 100644
--- a/soteria/lib/c_values/typed.mli
+++ b/soteria/lib/c_values/typed.mli
@@ -50,9 +50,9 @@ val t_f128 : [> sfloat ] ty
 (** {2 Typed svalues} *)
 
 type +'a t
-type sbool = T.sbool
+type sbool := T.sbool
 
-(** Basic value operations *)
+(** {3 Basic value operations} *)
 
 val get_ty : 'a t -> Svalue.ty
 val untype_type : 'a ty -> Svalue.ty
@@ -75,24 +75,22 @@ val equal : ([< any ] as 'a) t -> 'a t -> bool
 val compare : ([< any ] as 'a) t -> 'a t -> int
 val hash : [< any ] t -> int
 
-(** Typed constructors *)
+(** {3 Typed constructors} *)
+
+module S_bool : Symex.Value.S_bool.S with type 'a v = 'a t and type t = sbool
 
 val sem_eq : 'a t -> 'a t -> sbool t
 val sem_eq_untyped : 'a t -> 'a t -> [> sbool ] t
 val v_true : [> sbool ] t
 val v_false : [> sbool ] t
-val bool : bool -> [> sbool ] t
-val as_bool : 'a t -> bool option
-val and_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t
 val conj : [< sbool ] t list -> [> sbool ] t
 val split_ands : [< sbool ] t -> ([> sbool ] t -> unit) -> unit
-val or_ : [< sbool ] t -> [< sbool ] t -> [> sbool ] t
-val not : sbool t -> sbool t
 val not_int_bool : [< sint ] t -> [> sint ] t
 val distinct : 'a t list -> [> sbool ] t
 val ite : [< sbool ] t -> 'a t -> 'a t -> 'a t
 val int_z : Z.t -> [> sint ] t
 val int : int -> [> sint ] t
+val to_z : [< sint ] t -> Z.t option
 val nonzero_z : Z.t -> [> nonzero ] t
 val nonzero : int -> [> nonzero ] t
 val int_of_bool : [< sbool ] t -> [> sint ] t
@@ -100,7 +98,7 @@ val bool_of_int : [< sint ] t -> [> sbool ] t
 val zero : [> sint ] t
 val one : [> nonzero ] t
 
-(** Integer operations *)
+(** {3 Integer operations} *)
 
 val geq : [< sint ] t -> [< sint ] t -> [> sbool ] t
 val gt : [< sint ] t -> [< sint ] t -> [> sbool ] t
diff --git a/soteria/lib/logs/logs.mli b/soteria/lib/logs/logs.mli
index 35f0af644..1ee5a9767 100644
--- a/soteria/lib/logs/logs.mli
+++ b/soteria/lib/logs/logs.mli
@@ -52,6 +52,9 @@ module Cli : sig
   val term : (Config.t, string) result Cmdliner.Term.t
 end
 
+(** [L] is the module that contains all the fonctions to actually log stuff. One
+    can access it using [Soteria.Logs.L] or by [open Soteria.Logs.Import] and
+    then using [L] directly. *)
 module L : sig
   (** [with_section ~is_branch name f] runs [f] and aggregates its log messages
       within a collapsible section of the log file (when logs are in HTML mode).
diff --git a/soteria/lib/soteria_std/channels.ml b/soteria/lib/soteria_std/channels.ml
deleted file mode 100644
index b31b16955..000000000
--- a/soteria/lib/soteria_std/channels.ml
+++ /dev/null
@@ -1,7 +0,0 @@
-let with_out_file file f =
-  let oc = open_out file in
-  Fun.protect ~finally:(fun () -> close_out oc) (fun () -> f oc)
-
-let with_in_file file f =
-  let ic = open_in file in
-  Fun.protect ~finally:(fun () -> close_in ic) (fun () -> f ic)
diff --git a/soteria/lib/soteria_std/printable.ml b/soteria/lib/soteria_std/printable.ml
new file mode 100644
index 000000000..0329558c1
--- /dev/null
+++ b/soteria/lib/soteria_std/printable.ml
@@ -0,0 +1,6 @@
+(** Describes a type that can be pretty-printed. *)
+module type S = sig
+  type t
+
+  val pp : Format.formatter -> t -> unit
+end
diff --git a/soteria/lib/sym_data/s_elt.ml b/soteria/lib/sym_data/s_elt.ml
new file mode 100644
index 000000000..c049662b0
--- /dev/null
+++ b/soteria/lib/sym_data/s_elt.ml
@@ -0,0 +1,28 @@
+(** Basic operations of symbolic abstractions *)
+
+open Symex
+
+module type S = sig
+  (** Describes something symbolic, i.e. that contains symbolic variables. *)
+
+  type t
+
+  include Soteria_std.Printable.S with type t := t
+  module Symex : Symex.Base
+
+  val subst : (Var.t -> Var.t) -> t -> t
+  val iter_vars : t -> 'a Symex.Value.ty Var.iter_vars
+end
+
+module Of_concrete
+    (Symex : Symex.Base)
+    (C : sig
+      type t
+    end) =
+struct
+  module Symex = Symex
+  include C
+
+  let subst _ x = x
+  let iter_vars _ = fun _ -> ()
+end
diff --git a/soteria/lib/sym_data/s_eq.ml b/soteria/lib/sym_data/s_eq.ml
new file mode 100644
index 000000000..329af9107
--- /dev/null
+++ b/soteria/lib/sym_data/s_eq.ml
@@ -0,0 +1,43 @@
+(** Symbolic abstractions that support equality *)
+
+module type S = sig
+  (** Defines a type that supports symbolic semantic equality. For performance
+      reasons, such a type most also support {e syntactic} equality, such that
+      syntactic equality ([equal]) implies semantic equality ([sem_eq]) *)
+
+  (** The symex world in which the type lives. *)
+  module Symex : Symex.Base
+
+  type t
+
+  (** Syntactic equality, should be fast. *)
+  val equal : t -> t -> bool
+
+  (** Symbolic semantic equality *)
+  val sem_eq : t -> t -> Symex.Value.S_bool.t Symex.Value.t
+
+  (** Receives a list of {e syntactically different} values and returns a
+      symbolic boolean corresponding to the fact that these values are also
+      {e semantically} distinct. *)
+  val distinct : t list -> Symex.Value.S_bool.t Symex.Value.t
+end
+
+module Make_syntax (S : S) = struct
+  let ( ==@ ) = S.sem_eq
+end
+
+module Of_concrete
+    (Symex : Symex.Base)
+    (C : sig
+      type t
+
+      val equal : t -> t -> bool
+    end) : S with module Symex = Symex and type t = C.t = struct
+  module Symex = Symex
+  include C
+
+  let sem_eq x y = Symex.Value.S_bool.of_bool (C.equal x y)
+
+  (* Always returns true as the input list should always be syntactically distinct *)
+  let distinct _ = Symex.Value.S_bool.of_bool true
+end
diff --git a/soteria/lib/sym_data/s_int.ml b/soteria/lib/sym_data/s_int.ml
new file mode 100644
index 000000000..6528c65f4
--- /dev/null
+++ b/soteria/lib/sym_data/s_int.ml
@@ -0,0 +1,49 @@
+(** Symbolic abstractions over integers. *)
+
+module type S = sig
+  include S_elt.S
+  include S_eq.S with module Symex := Symex and type t := t
+  include Soteria_std.Printable.S with type t := t
+
+  (** Takes an integer and creates an abstraction over it *)
+  val of_z : Z.t -> t
+
+  (** Takes a symbolic integer and returns [Some z] if this abstraction
+      describes exactly a single integer, and [None] otherwise *)
+  val to_z : t -> Z.t option
+
+  val zero : unit -> t
+  val one : unit -> t
+
+  (** {3 Arithmetic operations} *)
+
+  type sbool_v := Symex.Value.S_bool.t Symex.Value.t
+
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val lt : t -> t -> sbool_v
+  val leq : t -> t -> sbool_v
+  val sem_eq : t -> t -> sbool_v
+end
+
+module type Bounded_S = sig
+  include S
+
+  val in_bound : t -> Symex.Value.S_bool.t Symex.Value.t
+end
+
+module Make_syntax (S_int : S) = struct
+  include S_eq.Make_syntax (S_int)
+
+  let ( +@ ) = S_int.add
+  let ( -@ ) = S_int.sub
+  let ( <@ ) = S_int.lt
+  let ( <=@ ) = S_int.leq
+  let ( ==@ ) = S_int.sem_eq
+
+  module Sym_int_syntax = struct
+    let mk_nonzero x = S_int.of_z (Z.of_int x)
+    let zero = S_int.zero
+    let one = S_int.one
+  end
+end
diff --git a/soteria/lib/sym_data/s_map.ml b/soteria/lib/sym_data/s_map.ml
new file mode 100644
index 000000000..b86c25efb
--- /dev/null
+++ b/soteria/lib/sym_data/s_map.ml
@@ -0,0 +1,125 @@
+(** Symbolic key-value maps. *)
+
+module Key = struct
+  module type S = sig
+    include Stdlib.Map.OrderedType
+    include S_elt.S with type t := t
+    include S_eq.S with type t := t and module Symex := Symex
+    include Soteria_std.Printable.S with type t := t
+  end
+
+  module Of_concrete (Symex : Symex.Base) (K : Soteria_std.Ordered_type.S) =
+  struct
+    include K
+    include S_elt.Of_concrete (Symex) (K)
+
+    include
+      S_eq.Of_concrete
+        (Symex)
+        (struct
+          include K
+
+          let equal x y = compare x y = 0
+        end)
+  end
+end
+
+module type S = sig
+  (** Defines a type that is a symbolic map from [key] to value. *)
+
+  module Symex : Symex.Base
+
+  type key
+
+  module Raw_map : Stdlib.Map.S with type key = key
+
+  type 'a t = 'a Raw_map.t
+
+  (** [find_opt key map] returns a symbolic computation that yields
+      - [(key, None)] if there is no key in the map that is semantically equal
+        to [key]
+      - [(key', Some v)] if there is a binding in the map for [(key', v)] and
+        [key'] is semantically equal to [key].
+
+      In both cases, the resulting [key'] can be used to insert or update the
+      map directly without needing to search for it again. *)
+  val find_opt : key -> 'a t -> (key * 'a option) Symex.t
+end
+
+module Make (Symex : Symex.Base) (Key : Key.S with module Symex = Symex) :
+  S with type key = Key.t and module Symex = Symex = struct
+  module Symex = Symex
+  open Symex.Syntax
+  module Raw_map = Stdlib.Map.Make (Key)
+
+  type key = Key.t
+  type 'a t = 'a Raw_map.t
+
+  let find_opt (key : Key.t) (m : 'a t) : (Key.t * 'a option) Symex.t =
+    let rec find_sym s =
+      match s () with
+      | Seq.Nil -> Symex.return (key, None)
+      | Seq.Cons ((k, v), tl) ->
+          if%sat Key.sem_eq key k then Symex.return (k, Some v) else find_sym tl
+      (* TODO: Investigate: if this can be somehow made a tail-call? *)
+    in
+    match Raw_map.find_opt key m with
+    | Some v ->
+        (* We found it syntactically *)
+        Symex.return (key, Some v)
+    | None -> find_sym (Raw_map.to_seq m)
+end
+
+module Make_failfast (Symex : Symex.S) (Key : Key.S with module Symex = Symex) :
+  S with type key = Key.t and module Symex = Symex = struct
+  module Symex = Symex
+  open Symex.Syntax
+  module Raw_map = Stdlib.Map.Make (Key)
+
+  type key = Key.t
+  type 'a t = 'a Raw_map.t
+
+  let find_opt (key : Key.t) (m : 'a t) : (Key.t * 'a option) Symex.t =
+    let rec find_sym (fkey, fval) tl =
+      (* At this point, we know that the element is in the map, so if tl is empty, it has to be first. *)
+      match tl () with
+      | Seq.Nil -> Symex.return (fkey, Some fval)
+      | Seq.Cons ((skey, sval), ttl) ->
+          if%sat Key.sem_eq key fkey then Symex.return (fkey, Some fval)
+          else find_sym (skey, sval) ttl
+      (* TODO: Investigate: if this can be somehow made a tail-call? *)
+    in
+    match Raw_map.find_opt key m with
+    | Some v -> Symex.return (key, Some v)
+    | None -> (
+        let s = Raw_map.to_seq m in
+        match s () with
+        | Seq.Nil ->
+            (* If the map is empty, we know for sure that the key is not in it *)
+            Symex.return (key, None)
+        | Seq.Cons (first, tl) ->
+            let not_in_map =
+              let all_keys_plus_key =
+                let all_keys = s |> Seq.map fst |> List.of_seq in
+                key :: all_keys
+              in
+              all_keys_plus_key |> Key.distinct
+            in
+            if%sat1 not_in_map then
+              (* In the case we know all keys are different from [key], we can return immediately *)
+              Symex.return (key, None)
+            else find_sym first tl)
+end
+
+module Make_concrete (Symex : Symex.S) (K : Soteria_std.Ordered_type.S) :
+  S with type key = K.t and module Symex = Symex = struct
+  module Symex = Symex
+  module Key = Key.Of_concrete (Symex) (K)
+  module Raw_map = Stdlib.Map.Make (Key)
+
+  type key = Key.t
+  type 'a t = 'a Raw_map.t
+
+  let find_opt (key : Key.t) (m : 'a t) =
+    Symex.return (key, Raw_map.find_opt key m)
+end
diff --git a/soteria/lib/sym_data/s_range.ml b/soteria/lib/sym_data/s_range.ml
new file mode 100644
index 000000000..3cb9f4b6e
--- /dev/null
+++ b/soteria/lib/sym_data/s_range.ml
@@ -0,0 +1,42 @@
+(** Symbolic abstractions over ranges. *)
+
+module Make (S_int : S_int.S) = struct
+  module Symex = S_int.Symex
+
+  type sbool = Symex.Value.S_bool.t Symex.Value.t
+
+  (** Type of value representing the bounds of the interval *)
+  type v = S_int.t
+
+  (** A value [(a, b)] of type [t] represents the interval starting at [a]
+      {e included} and ending at [b] {e excluded}. Often denoted {m [a, b)} or
+      {m [a, b[}*)
+  type t = v * v
+
+  open S_int
+
+  let sem_eq (a1, b1) (a2, b2) =
+    Symex.Value.S_bool.and_ (S_int.sem_eq a1 a2) (S_int.sem_eq b1 b2)
+
+  (** [size (a, b)] is [b - a] *)
+  let size (a, b) = sub b a
+
+  (** [split_at (a, b) x] is [(a, x), (x, b)] *)
+  let split_at (l, h) x = ((l, x), (x, h))
+
+  (** [offset (a, b) x] is [(a + x, b + x)] *)
+  let offset (l, h) x = (add l x, add h x)
+
+  (** [subseteq r1 r2] is a symbolic boolean characterising whether [r1] is a
+      subset of [r2] *)
+  let subset_eq (a1, b1) (a2, b2) =
+    Symex.Value.S_bool.and_ (leq a2 a1) (leq b1 b2)
+
+  (** [strictly_inside (a, b) r] is [a < r < b] *)
+  let strictly_inside x (a, b) = Symex.Value.S_bool.and_ (lt a x) (lt x b)
+
+  (** [of_low_and_size a b] is [(a, a + b)]*)
+  let of_low_and_size low size = (low, add low size)
+
+  let pp fmt (a, b) = Format.fprintf fmt "[%a, %a[" S_int.pp a S_int.pp b
+end
diff --git a/soteria/lib/sym_data/sym_data.ml b/soteria/lib/sym_data/sym_data.ml
new file mode 100644
index 000000000..b7709bbf6
--- /dev/null
+++ b/soteria/lib/sym_data/sym_data.ml
@@ -0,0 +1,7 @@
+(** A collection of symbolic data structures and useful signatures. *)
+
+module S_elt = S_elt
+module S_eq = S_eq
+module S_int = S_int
+module S_range = S_range
+module S_map = S_map
diff --git a/soteria/lib/sym_states/plist.ml b/soteria/lib/sym_states/plist.ml
index b62135352..1c5448e4c 100644
--- a/soteria/lib/sym_states/plist.ml
+++ b/soteria/lib/sym_states/plist.ml
@@ -11,7 +11,7 @@ module type SInt_sig = sig
 
   include Stdlib.Map.OrderedType with type t := t
 
-  type sbool_v := Value.sbool Value.t
+  type sbool_v := Value.S_bool.t Value.t
 
   val pp : Format.formatter -> t -> unit
   val sem_eq : t -> t -> sbool_v
@@ -78,7 +78,8 @@ struct
       | None -> SInt.greater_or_equal ofs (SInt.of_int 0)
       | Some b -> SInt.in_range ofs (SInt.of_int 0, b)
     in
-    if%sat Symex.Value.not cond then Result.error `OutOfBounds else Result.ok ()
+    if%sat Symex.Value.S_bool.not cond then Result.error `OutOfBounds
+    else Result.ok ()
 
   let create (size : int) ~(new_codom : 'a) : 'a t =
     if size <= 0 then
diff --git a/soteria/lib/sym_states/pmap.ml b/soteria/lib/sym_states/pmap.ml
index 750df77d0..420e568b5 100644
--- a/soteria/lib/sym_states/pmap.ml
+++ b/soteria/lib/sym_states/pmap.ml
@@ -6,7 +6,7 @@ module type KeyS = sig
   module Symex : Symex.Base
   include Stdlib.Map.OrderedType with type t := t
 
-  type sbool_v := Symex.Value.sbool Symex.Value.t
+  type sbool_v := Symex.Value.S_bool.t Symex.Value.t
 
   val pp : Format.formatter -> t -> unit
   val sem_eq : t -> t -> sbool_v
@@ -22,10 +22,10 @@ module Mk_concrete_key (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) :
   module Symex = Symex
   include Key
 
-  let sem_eq x y = Symex.Value.bool (Key.compare x y = 0)
+  let sem_eq x y = Symex.Value.S_bool.of_bool (Key.compare x y = 0)
   let fresh () = failwith "Fresh not implemented for concrete keys"
   let simplify = Symex.return
-  let distinct _ = Symex.Value.bool true
+  let distinct _ = Symex.Value.S_bool.of_bool true
   let subst _ x = x
   let iter_vars _ = fun _ -> ()
 end
@@ -162,7 +162,6 @@ module Make (Symex : Symex.Base) (Key : KeyS with module Symex = Symex) = struct
       | (k, v) :: tl ->
           if%sat Key.sem_eq key k then Symex.return (k, Some v)
           else find_bindings tl
-      (* TODO: Investigate: this is not a tailcall, because if%sat is not an if. *)
     in
     match M'.find_opt key st with
     | Some v -> Symex.return (key, Some v)
diff --git a/soteria/lib/sym_states/pure_fun.ml b/soteria/lib/sym_states/pure_fun.ml
index b86980be2..259e2c3cc 100644
--- a/soteria/lib/sym_states/pure_fun.ml
+++ b/soteria/lib/sym_states/pure_fun.ml
@@ -13,7 +13,7 @@ module type Codom = sig
 
   val pp : Format.formatter -> t -> unit
   val fresh : unit -> t Symex.t
-  val sem_eq : t -> t -> Symex.Value.sbool Symex.Value.t
+  val sem_eq : t -> t -> Symex.Value.S_bool.t Symex.Value.t
   val subst : (Var.t -> Var.t) -> t -> t
   val iter_vars : t -> 'a Symex.Value.ty Var.iter_vars
 end
diff --git a/soteria/lib/sym_states/sym_states.ml b/soteria/lib/sym_states/sym_states.ml
new file mode 100644
index 000000000..a45cb0de1
--- /dev/null
+++ b/soteria/lib/sym_states/sym_states.ml
@@ -0,0 +1,12 @@
+(** A collection of state monad transformers for building compositional symbolic
+    execution states. *)
+
+module Bi_abd = Bi_abd
+module Excl = Excl
+module Freeable = Freeable
+module Plist = Plist
+module Pmap = Pmap
+module Pure_fun = Pure_fun
+module State_monad = State_monad
+module Tree_block = Tree_block
+module With_info = With_info
diff --git a/soteria/lib/sym_states/tree_block.ml b/soteria/lib/sym_states/tree_block.ml
index 5c646a3ab..636229388 100644
--- a/soteria/lib/sym_states/tree_block.ml
+++ b/soteria/lib/sym_states/tree_block.ml
@@ -1,4 +1,5 @@
 open Symex
+module Make_bool_syntax = Symex.Value.S_bool.Make_syntax
 open Soteria_std.Syntaxes.FunctionWrap
 
 (** A [Split_tree] is a simplified representation of a tree, that has no offset.
@@ -45,25 +46,10 @@ and node_qty = Partially | Totally
 *)
 module type MemVal = sig
   module Symex : Symex.Base
-
-  module SBoundedInt : sig
-    type +'a t = 'a Symex.Value.t
-    type sbool
-    type sint
-
-    val v_false : sbool t
-    val zero : unit -> sint t
-    val ( +@ ) : sint t -> sint t -> sint t
-    val ( -@ ) : sint t -> sint t -> sint t
-    val ( <@ ) : sint t -> sint t -> sbool t
-    val ( <=@ ) : sint t -> sint t -> sbool t
-    val ( ==@ ) : sint t -> sint t -> sbool t
-    val ( &&@ ) : sbool t -> sbool t -> sbool t
-    val in_bound : sint t -> sbool t
-  end
+  module Bounded_int : Sym_data.S_int.Bounded_S with module Symex = Symex
 
   type t
-  type sint := SBoundedInt.sint SBoundedInt.t
+  type sint := Bounded_int.t
 
   val pp : Format.formatter -> t -> unit
 
@@ -120,24 +106,21 @@ module type MemVal = sig
   val assert_exclusively_owned : t -> (unit, 'err, serialized) Symex.Result.t
 end
 
-module Make
-    (Symex : Symex.Base)
-    (MemVal :
-      MemVal
-        with module Symex = Symex
-         and type 'a SBoundedInt.t = 'a Symex.Value.t
-         and type SBoundedInt.sbool = Symex.Value.sbool) =
+module Make (Symex : Symex.Base) (MemVal : MemVal with module Symex = Symex) =
 struct
   open Compo_res
   open Symex.Syntax
   open Symex
-  open MemVal.SBoundedInt
+  open MemVal.Bounded_int
+  open Make_bool_syntax (Symex.Value.S_bool)
+  module Range = Sym_data.S_range.Make (MemVal.Bounded_int)
+  open Sym_data.S_int.Make_syntax (MemVal.Bounded_int)
 
   module Sym_int_syntax = struct
-    let zero = MemVal.SBoundedInt.zero
+    let zero = MemVal.Bounded_int.zero
   end
 
-  type nonrec sint = sint Symex.Value.t
+  type sint = MemVal.Bounded_int.t
 
   (* re-export the types to be able to use them easily *)
   type nonrec ('a, 'sint) tree = ('a, 'sint) tree = {
@@ -146,19 +129,6 @@ struct
     children : (('a, 'sint) tree * ('a, 'sint) tree) option;
   }
 
-  module Range = struct
-    type t = sint * sint
-
-    let pp ft (l, u) = Fmt.pf ft "[%a, %a[" Symex.Value.ppa l Symex.Value.ppa u
-    let sem_eq (a, c) (b, d) = a ==@ b &&@ (c ==@ d)
-    let is_inside (l1, u1) (l2, u2) = l2 <=@ l1 &&@ (u1 <=@ u2)
-    let strictly_inside x (l, u) = l <@ x &&@ (x <@ u)
-    let size (l, u) = u -@ l
-    let split_at (l, h) x = ((l, x), (x, h))
-    let offset (l, u) off = (l +@ off, u +@ off)
-    let of_low_and_size low size = (low, low +@ size)
-  end
-
   module Split_tree = Split_tree
 
   module Node = struct
@@ -335,7 +305,7 @@ struct
       else if Option.is_none t.children then return (t, None)
       else
         let left, right = Option.get t.children in
-        if%sat Range.is_inside range left.range then
+        if%sat Range.subset_eq range left.range then
           let* extracted, new_left = extract left range in
           let+ new_self =
             match new_left with
@@ -452,7 +422,7 @@ struct
                   in
                   frame_inside ~replace_node ~rebuild_parent new_self range
               else
-                if%sat Range.is_inside range left.range then
+                if%sat Range.subset_eq range left.range then
                   let** node, left =
                     frame_inside ~replace_node ~rebuild_parent left range
                   in
@@ -511,7 +481,8 @@ struct
 
   type t = {
     root : Tree.t;
-    bound : sint option; [@printer Fmt.(option ~none:(any "⊥") Symex.Value.ppa)]
+    bound : sint option;
+        [@printer Fmt.(option ~none:(any "⊥") MemVal.Bounded_int.pp)]
   }
   [@@deriving show { with_path = false }]
 
@@ -523,7 +494,7 @@ struct
     let () =
       Option.iter
         (fun b ->
-          let range_str = Fmt.str "[%a; ∞[" Symex.Value.ppa b in
+          let range_str = Fmt.str "[%a; ∞[" MemVal.Bounded_int.pp b in
           r := [ (range_str, text "OOB") ])
         t.bound
     in
@@ -539,11 +510,12 @@ struct
 
   type serialized_atom =
     | MemVal of {
-        offset : sint; [@printer Symex.Value.ppa]
-        len : sint; [@printer Symex.Value.ppa]
+        offset : MemVal.Bounded_int.t;
+        len : MemVal.Bounded_int.t;
         v : MemVal.serialized;
       }
-    | Bound of sint [@printer fun f v -> Fmt.pf f "Bound(%a)" Symex.Value.ppa v]
+    | Bound of MemVal.Bounded_int.t
+        [@printer fun f v -> Fmt.pf f "Bound(%a)" MemVal.Bounded_int.pp v]
   [@@deriving show { with_path = false }]
 
   type serialized = serialized_atom list
@@ -617,7 +589,7 @@ struct
   (** Logic *)
 
   let subst_serialized subst_var (serialized : serialized) =
-    let v_subst v = Symex.Value.subst subst_var v in
+    let v_subst v = MemVal.Bounded_int.subst subst_var v in
     let subst_atom = function
       | MemVal { offset; len; v } ->
           let v = MemVal.subst_serialized subst_var v in
@@ -630,10 +602,10 @@ struct
     List.iter
       (function
         | MemVal { offset; len; v } ->
-            Symex.Value.iter_vars offset f;
-            Symex.Value.iter_vars len f;
+            MemVal.Bounded_int.iter_vars offset f;
+            MemVal.Bounded_int.iter_vars len f;
             MemVal.iter_vars_serialized v f
-        | Bound v -> Symex.Value.iter_vars v f)
+        | Bound v -> MemVal.Bounded_int.iter_vars v f)
       serialized
 
   let pp_serialized = Fmt.Dump.list pp_serialized_atom
@@ -670,7 +642,7 @@ struct
         Ok (to_opt { bound = None; root })
 
   let produce_bound bound t =
-    let* () = Symex.assume [ MemVal.SBoundedInt.in_bound bound ] in
+    let* () = Symex.assume [ MemVal.Bounded_int.in_bound bound ] in
     match t with
     | None ->
         Symex.return
@@ -681,7 +653,7 @@ struct
 
   let produce_mem_val offset len v t =
     let ((_, high) as range) = Range.of_low_and_size offset len in
-    let* () = Symex.assume [ MemVal.SBoundedInt.in_bound high ] in
+    let* () = Symex.assume [ MemVal.Bounded_int.in_bound high ] in
     let t =
       match t with
       | Some t -> t
diff --git a/soteria/lib/symex/solver.ml b/soteria/lib/symex/solver.ml
index 1c77a367b..95da98169 100644
--- a/soteria/lib/symex/solver.ml
+++ b/soteria/lib/symex/solver.ml
@@ -6,7 +6,7 @@ module type Mutable_incremental = sig
   include Reversible.Mutable
   module Value : Value.S
 
-  type sbool_v := Value.sbool Value.t
+  type sbool_v := Value.S_bool.t Value.t
 
   (** Adds constraints to the solver state. The [simplified] flag indicates if
       {!simplify} was already applied to the constraints, and is [false] by
@@ -24,8 +24,10 @@ module type In_place_incremental = sig
   include Reversible.In_place
   module Value : Value.S
 
+  type sbool_v := Value.S_bool.t Value.t
+
   (** simplified indicates if constraits were already simplified *)
-  val add_constraints : ?simplified:bool -> Value.sbool Value.t list -> unit
+  val add_constraints : ?simplified:bool -> sbool_v list -> unit
 
   val sat : unit -> bool
 
diff --git a/soteria/lib/symex/symex.ml b/soteria/lib/symex/symex.ml
index ad2c5ae25..2b3698def 100644
--- a/soteria/lib/symex/symex.ml
+++ b/soteria/lib/symex/symex.ml
@@ -57,11 +57,11 @@ module type Base = sig
       Use this instead of [`Lfail] directly in type signatures to avoid
       potential typos such as [`LFail] which will take precious time to debug...
       trust me. *)
-  type lfail = [ `Lfail of Value.sbool Value.t ]
+  type lfail = [ `Lfail of Value.S_bool.t Value.t ]
 
   type 'a v := 'a Value.t
   type 'a vt := 'a Value.ty
-  type sbool := Value.sbool
+  type sbool := Value.S_bool.t
 
   val assume : sbool v list -> unit t
   val vanish : unit -> 'a t
@@ -217,7 +217,7 @@ module type Base = sig
     val ( let+? ) : ('a, 'b, 'c) Result.t -> ('c -> 'd) -> ('a, 'b, 'd) Result.t
 
     module Symex_syntax : sig
-      type sbool_v := Value.sbool Value.t
+      type sbool_v := Value.S_bool.t Value.t
 
       val branch_on :
         ?left_branch_name:string ->
@@ -250,7 +250,7 @@ module type S = sig
   include Base
 
   type 'a v := 'a Value.t
-  type sbool := Value.sbool
+  type sbool := Value.S_bool.t
 
   (** [run ~fuel  p] actually performs symbolic execution of the symbolic
       process [p] and returns a list of obtained branches which capture the
@@ -293,14 +293,14 @@ module type S = sig
       ?fuel:Fuel_gauge.t ->
       mode:Approx.t ->
       ('ok, 'err, 'fix) t ->
-      (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.sbool Value.t list)
+      (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.S_bool.t Value.t list)
       list
 
     val run_with_stats :
       ?fuel:Fuel_gauge.t ->
       mode:Approx.t ->
       ('ok, 'err, 'fix) t ->
-      (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.sbool Value.t list)
+      (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.S_bool.t Value.t list)
       list
       Stats.with_stats
 
@@ -308,7 +308,7 @@ module type S = sig
       ?fuel:Fuel_gauge.t ->
       mode:Approx.t ->
       ('ok, 'err, 'fix) t ->
-      (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.sbool Value.t list)
+      (('ok, 'err Or_gave_up.t, 'fix) Compo_res.t * Value.S_bool.t Value.t list)
       list
   end
 end
@@ -352,7 +352,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
   end
 
   type 'a t = 'a Iter.t
-  type lfail = [ `Lfail of Value.sbool Value.t ]
+  type lfail = [ `Lfail of Value.S_bool.t Value.t ]
 
   module Symex_state : Reversible.In_place = struct
     let backtrack_n n =
@@ -383,7 +383,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
           f ()
       | l :: ls -> (
           let l = Solver.simplify l in
-          match Value.as_bool l with
+          match Value.S_bool.to_bool l with
           | Some true -> aux acc ls
           | Some false ->
               L.trace (fun m -> m "Assuming false, stopping this branch")
@@ -396,7 +396,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
       side-effects at the wrong time. *)
   let assert_raw value : bool =
     let value = Solver.simplify value in
-    match Value.as_bool value with
+    match Value.S_bool.to_bool value with
     | Some true -> true
     | Some false -> false
     | None ->
@@ -404,7 +404,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
           L.with_section (Fmt.str "Checking entailment for %a" Value.ppa value)
         in
         Symex_state.save ();
-        Solver.add_constraints [ Value.(not value) ];
+        Solver.add_constraints [ Value.S_bool.not value ];
         let sat_result = Solver.sat () in
         let () =
           L.debug (fun m ->
@@ -428,7 +428,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
 
   let consume_false () f =
     if Approx.As_ctx.is_ux () then ()
-    else f (Compo_res.Error (`Lfail (Value.bool false)))
+    else f (Compo_res.Error (`Lfail (Value.S_bool.of_bool false)))
 
   let nondet ty f =
     let v = Solver.fresh_var ty in
@@ -443,7 +443,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
       ~(else_ : unit -> 'a Iter.t) : 'a Iter.t =
    fun f ->
     let guard = Solver.simplify guard in
-    match Value.as_bool guard with
+    match Value.S_bool.to_bool guard with
     (* [then_] and [else_] could be ['a t] instead of [unit -> 'a t],
        if we remove the Some true and Some false optimisation. *)
     | Some true -> then_ () f
@@ -459,7 +459,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
             else L.trace (fun m -> m "Branch is not feasible"));
         Symex_state.backtrack_n 1;
         L.with_section ~is_branch:true right_branch_name (fun () ->
-            Solver.add_constraints [ Value.(not guard) ];
+            Solver.add_constraints [ Value.S_bool.not guard ];
             if !left_unsat then
               (* Right must be sat since left was not! We didn't branch so we don't consume the counter *)
               else_ () f
@@ -478,14 +478,14 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
       ~(then_ : unit -> 'a Iter.t) ~(else_ : unit -> 'a Iter.t) : 'a Iter.t =
    fun f ->
     let guard = Solver.simplify guard in
-    match Value.as_bool guard with
+    match Value.S_bool.to_bool guard with
     (* [then_] and [else_] could be ['a t] instead of [unit -> 'a t],
        if we remove the Some true and Some false optimisation. *)
     | Some true -> then_ () f
     | Some false -> else_ () f
     | None ->
         Symex_state.save ();
-        Solver.add_constraints ~simplified:true [ Value.(not guard) ];
+        Solver.add_constraints ~simplified:true [ Value.S_bool.not guard ];
         let neg_unsat = Solver_result.is_unsat (Solver.sat ()) in
         if neg_unsat then then_ () f;
         Symex_state.backtrack_n 1;
@@ -499,7 +499,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
       ~then_ ~else_ : 'a Iter.t =
    fun f ->
     let guard = Solver.simplify guard in
-    match Value.as_bool guard with
+    match Value.S_bool.to_bool guard with
     | Some true -> then_ () f
     | Some false -> else_ () f
     | None ->
@@ -509,7 +509,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
         if left_sat then then_ () f;
         Symex_state.backtrack_n 1;
         if not left_sat then (
-          Solver.add_constraints [ Value.(not guard) ];
+          Solver.add_constraints [ Value.S_bool.not guard ];
           else_ () f)
 
   let branch_on_take_one ?left_branch_name ?right_branch_name guard ~then_
@@ -520,8 +520,7 @@ module Make (Meta : Meta.S) (Sol : Solver.Mutable_incremental) :
     else branch_on ?left_branch_name ?right_branch_name guard ~then_ ~else_ f
 
   let assert_or_error guard err =
-    branch_on
-      Value.(not guard)
+    branch_on (Value.S_bool.not guard)
       ~then_:(fun () -> return (Compo_res.Error err))
       ~else_:(fun () -> return (Compo_res.Ok ()))
 
diff --git a/soteria/lib/symex/value.ml b/soteria/lib/symex/value.ml
index adb19f54d..1d6726cc2 100644
--- a/soteria/lib/symex/value.ml
+++ b/soteria/lib/symex/value.ml
@@ -1,13 +1,30 @@
+module S_bool = struct
+  module type S = sig
+    type +'a v
+    type t
+
+    val not : t v -> t v
+    val and_ : t v -> t v -> t v
+    val or_ : t v -> t v -> t v
+    val to_bool : t v -> bool option
+    val of_bool : bool -> t v
+  end
+
+  module Make_syntax (S_bool : S) = struct
+    let ( &&@ ) = S_bool.and_
+    let ( ||@ ) = S_bool.or_
+    let not = S_bool.not
+  end
+end
+
 module type S = sig
   type +'a t
   type +'a ty
-  type sbool
 
-  val not : sbool t -> sbool t
+  module S_bool : S_bool.S with type 'a v = 'a t
+
   val ppa : Format.formatter -> 'a t -> unit
   val iter_vars : 'a t -> 'b ty Var.iter_vars
   val subst : (Var.t -> Var.t) -> 'a t -> 'a t
   val mk_var : Var.t -> 'a ty -> 'a t
-  val as_bool : 'a t -> bool option
-  val bool : bool -> sbool t
 end
diff --git a/soteria/lib/terminal/diagnostic.ml b/soteria/lib/terminal/diagnostic.ml
index 14a666624..6d4520eca 100644
--- a/soteria/lib/terminal/diagnostic.ml
+++ b/soteria/lib/terminal/diagnostic.ml
@@ -42,7 +42,7 @@ let utf8_to_byte_offset str idx =
 
 let real_index (file : string) ((line, col) : pos) =
   let open Syntaxes.FunctionWrap in
-  let@ ic = Channels.with_in_file file in
+  let@ ic = In_channel.with_open_text file in
   let current_index = ref 0 in
   let current_line = ref 0 in
   while !current_line <= line do
diff --git a/soteria/tests/symex/run_twice.ml b/soteria/tests/symex/run_twice.ml
index 59329a87e..74df4fb80 100644
--- a/soteria/tests/symex/run_twice.ml
+++ b/soteria/tests/symex/run_twice.ml
@@ -21,7 +21,7 @@ let fn () =
   let open Typed.Infix in
   let* v = nondet Typed.t_int in
   let* () = assume [ v ==@ Typed.zero ] in
-  if%sat Typed.not (v ==@ Typed.one) then return true else return false
+  if%sat Typed.S_bool.not (v ==@ Typed.one) then return true else return false
 
 let do_test () =
   let pp =
diff --git a/soteria/tutorial/core_symex.mld b/soteria/tutorial/core_symex.mld
index 316c2301d..1c17c0d5a 100644
--- a/soteria/tutorial/core_symex.mld
+++ b/soteria/tutorial/core_symex.mld
@@ -37,7 +37,7 @@ Executing a symbolic process is done using the {{!Soteria.Symex.S.run}run} funct
 # Symex.run
 - : ?fuel:Symex.Fuel_gauge.t ->
     mode:Symex.Approx.t ->
-    'a Symex.t -> ('a * Symex.Value.sbool Typed.t list) list
+    'a Symex.t -> ('a * Symex.Value.S_bool.t Typed.t list) list
 = <fun>
 ]}
 
@@ -47,7 +47,7 @@ For instance, let's execute the symbolic process we just created, using the {{!S
 
 {@ocaml[
 # Symex.return 0 |> Symex.run ~mode:OX;;
-- : (int * Symex.Value.sbool Typed.t list) list = [(0, [])]]}
+- : (int * Symex.Value.S_bool.t Typed.t list) list = [(0, [])]]}
 ]}
 
 As expected the result of the symbolic process is a single branch with the value [0] and an empty path condition [[]], which means that there is no condition for taking this branch, i.e., it is always taken.
@@ -67,7 +67,7 @@ Let's run this process:
 
 {@ocaml[
 # Symex.nondet Typed.t_int |> Symex.run ~mode:OX;;
-- : ([> Typed.T.sint ] Typed.t * Symex.Value.sbool Typed.t list) list =
+- : ([> Typed.T.sint ] Typed.t * Symex.Value.S_bool.t Typed.t list) list =
 [(V|1|, [])]
 ]}
 
@@ -108,7 +108,8 @@ Running this symbolic process yields a single branch with no path condition:
 
 {@ocaml[
 # Symex.run ~mode:OX process;;
-- : (([> Typed.T.sint ] as '_weak1) Typed.t * Symex.Value.sbool Typed.t list)
+- : (([> Typed.T.sint ] as '_weak1) Typed.t *
+     Symex.Value.S_bool.t Typed.t list)
     list
 = [((V|1| + 2), [])]
 ]}
@@ -124,7 +125,7 @@ For instance, we can create a symbolic process that introduces a nondeterministi
 val process : bool Symex.t = <abstr>
 
 # Symex.run ~mode:OX process;;
-- : (bool * Symex.Value.sbool Typed.t list) list = [(false, [])]
+- : (bool * Symex.Value.S_bool.t Typed.t list) list = [(false, [])]
 ]}
 
 This process returns a single branch with the value [false], as it is not *always* guaranteed that the symbolic integer [x] is positive. Now, if we add an assumption that, say, [x] is greater than 10, we get a different result:
@@ -137,7 +138,8 @@ This process returns a single branch with the value [false], as it is not *alway
 val process : bool Symex.t = <abstr>
 
 # Symex.run ~mode:OX process;;
-- : (bool * Symex.Value.sbool Typed.t list) list = [(true, [(11 <= V|1|)])]
+- : (bool * Symex.Value.S_bool.t Typed.t list) list =
+[(true, [(11 <= V|1|)])]
 ]} 
 
 This time, the assertion is satisfied, and the symbolic process returns a single branch with value [true], and a path condition that corresponds to the assumption we made, i.e. that [V|1|] (the symbolic integer) is greater than or equal to 11 (which is equivalent to the assumption we wrote).
@@ -156,7 +158,7 @@ A more interesting symbolic process is one that introduces conditional branching
 val process : string Symex.t = <abstr>
 
 # Symex.run ~mode:OX process;;
-- : (string * Symex.Value.sbool Typed.t list) list =
+- : (string * Symex.Value.S_bool.t Typed.t list) list =
 [("V|1| is even", [(0 == (V|1| mod 2))]);
  ("V|1| is odd", [(0 != (V|1| mod 2))])]
 ]}
diff --git a/soteria/tutorial/index.mld b/soteria/tutorial/index.mld
index 416c09bca..0d6ddb61d 100644
--- a/soteria/tutorial/index.mld
+++ b/soteria/tutorial/index.mld
@@ -11,6 +11,7 @@
 {!modules: Soteria}
 {!modules:
   Soteria.Symex
+  Soteria.Sym_data
   Soteria.Sym_states
   Soteria.Logs
   Soteria.C_values