diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml
index 91791740c..9acfab4b4 100644
--- a/sledge/nonstdlib/map.ml
+++ b/sledge/nonstdlib/map.ml
@@ -11,24 +11,39 @@ include Map_intf
 module Make (Key : sig
   type t [@@deriving compare, sexp_of]
 end) : S with type key = Key.t = struct
-  module KeyMap = Core.Map.Make_plain (Key)
-  module Key = KeyMap.Key
+  module M = CCMap.Make (Key)
 
   type key = Key.t
-
-  include KeyMap.Tree
-
-  let compare = compare_direct
-
-  let to_map t =
-    Core.Map.Using_comparator.of_tree ~comparator:Key.comparator t
-
-  let of_map m = Base.Map.Using_comparator.to_tree m
-
-  let merge_skewed x y ~combine =
-    of_map (Core.Map.merge_skewed (to_map x) (to_map y) ~combine)
-
-  let map_endo t ~f = map_endo map t ~f
+  type 'a t = 'a M.t [@@deriving compare, equal]
+
+  let sexp_of_t sexp_of_data m =
+    M.to_list m
+    |> Sexplib.Conv.sexp_of_list
+         (Sexplib.Conv.sexp_of_pair Key.sexp_of_t sexp_of_data)
+
+  module Provide_of_sexp (Key : sig
+    type t = key [@@deriving of_sexp]
+  end) =
+  struct
+    let t_of_sexp data_of_sexp s =
+      s
+      |> Sexplib.Conv.list_of_sexp
+           (Sexplib.Conv.pair_of_sexp Key.t_of_sexp data_of_sexp)
+      |> M.of_list
+  end
+
+  let empty = M.empty
+  let singleton = M.singleton
+  let add_exn m ~key ~data = M.add key data m
+  let set m ~key ~data = M.add key data m
+
+  let add_multi m ~key ~data =
+    M.update key
+      (function Some vs -> Some (data :: vs) | None -> Some [data])
+      m
+
+  let remove m key = M.remove key m
+  let merge l r ~f = M.merge_safe l r ~f:(fun key -> f ~key)
 
   let merge_endo t u ~f =
     let change = ref false in
@@ -43,49 +58,107 @@ end) : S with type key = Key.t = struct
     in
     if !change then t' else t
 
-  let fold_until m ~init ~f ~finish =
-    let fold m ~init ~f =
-      let f ~key ~data s = f s (key, data) in
-      fold m ~init ~f
-    in
-    let f s (k, v) = f ~key:k ~data:v s in
-    Container.fold_until ~fold ~init ~f ~finish m
-
-  let root_key_exn m =
-    let@ {return} = with_return in
-    binary_search_segmented m `Last_on_left ~segment_of:(fun ~key ~data:_ ->
-        return key )
-    |> ignore ;
-    raise (Not_found_s (Atom __LOC__))
-
-  let choose_exn m =
-    let@ {return} = with_return in
-    binary_search_segmented m `Last_on_left ~segment_of:(fun ~key ~data ->
-        return (key, data) )
-    |> ignore ;
-    raise (Not_found_s (Atom __LOC__))
+  let merge_skewed x y ~combine =
+    M.union (fun key v1 v2 -> Some (combine ~key v1 v2)) x y
 
-  let choose m = try Some (choose_exn m) with Not_found_s _ -> None
-  let pop m = choose m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k))
+  let union x y ~f = M.union f x y
+  let is_empty = M.is_empty
 
-  let pop_min_elt m =
-    min_elt m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k))
+  let root_key m =
+    let exception Found in
+    let found = ref None in
+    try
+      M.find_first
+        (fun key ->
+          found := Some key ;
+          raise Found )
+        m
+      |> ignore ;
+      None
+    with
+    | Found -> !found
+    | Not_found -> None
+
+  let root_binding m =
+    let exception Found in
+    let found = ref None in
+    try
+      M.for_all
+        (fun key data ->
+          found := Some (key, data) ;
+          raise Found )
+        m
+      |> ignore ;
+      None
+    with
+    | Found -> !found
+    | Not_found -> None
 
   let is_singleton m =
-    try
-      let l, _, r = split m (root_key_exn m) in
-      is_empty l && is_empty r
-    with Not_found_s _ -> false
+    match root_key m with
+    | Some k ->
+        let l, _, r = M.split k m in
+        is_empty l && is_empty r
+    | None -> false
+
+  let length = M.cardinal
+  let choose_key = root_key
+  let choose = root_binding
+  let choose_exn m = CCOpt.get_exn (choose m)
+  let min_binding = M.min_binding_opt
+  let mem m k = M.mem k m
+  let find_exn m k = M.find k m
+  let find m k = M.find_opt k m
+
+  let find_multi m k =
+    match M.find_opt k m with None -> [] | Some vs -> vs
 
   let find_and_remove m k =
     let found = ref None in
     let m =
-      change m k ~f:(fun v ->
+      M.update k
+        (fun v ->
           found := v ;
           None )
+        m
     in
     Option.map ~f:(fun v -> (v, m)) !found
 
+  let pop m = choose m |> CCOpt.map (fun (k, v) -> (k, v, remove m k))
+
+  let pop_min_binding m =
+    min_binding m |> CCOpt.map (fun (k, v) -> (k, v, remove m k))
+
+  let change m key ~f = M.update key f m
+  let update m k ~f = M.update k (fun v -> Some (f v)) m
+  let map m ~f = M.map f m
+  let mapi m ~f = M.mapi (fun key data -> f ~key ~data) m
+  let map_endo t ~f = map_endo map t ~f
+  let filter_mapi m ~f = M.filter_map (fun key data -> f ~key ~data) m
+  let iter m ~f = M.iter (fun _ data -> f data) m
+  let iteri m ~f = M.iter (fun key data -> f ~key ~data) m
+  let existsi m ~f = M.exists (fun key data -> f ~key ~data) m
+  let for_alli m ~f = M.for_all (fun key data -> f ~key ~data) m
+  let fold m ~init ~f = M.fold (fun key data acc -> f ~key ~data acc) m init
+  let to_alist ?key_order:_ = M.to_list
+  let data m = Iter.to_list (M.values m)
+
+  let to_iter2 l r =
+    let seq = ref Iter.empty in
+    M.merge_safe l r ~f:(fun k vv ->
+        seq := Iter.cons (k, vv) !seq ;
+        None )
+    |> ignore ;
+    !seq
+
+  let symmetric_diff ~data_equal l r =
+    Iter.filter_map (to_iter2 l r) ~f:(fun (k, vv) ->
+        match vv with
+        | `Both (lv, rv) when data_equal lv rv -> None
+        | `Both vv -> Some (k, `Unequal vv)
+        | `Left lv -> Some (k, `Left lv)
+        | `Right rv -> Some (k, `Right rv) )
+
   let pp pp_k pp_v fs m =
     Format.fprintf fs "@[<1>[%a]@]"
       (List.pp ",@ " (fun fs (k, v) ->
@@ -101,7 +174,7 @@ end) : S with type key = Key.t = struct
       | k, `Unequal vv ->
           Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_diff_val vv
     in
-    let sd = Sequence.to_list (symmetric_diff ~data_equal x y) in
+    let sd = Iter.to_list (symmetric_diff ~data_equal x y) in
     if not (List.is_empty sd) then
       Format.fprintf fs "[@[<hv>%a@]];@ " (List.pp ";@ " pp_diff_elt) sd
 end
diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml
index 8966cfdb1..89026a1f4 100644
--- a/sledge/nonstdlib/map_intf.ml
+++ b/sledge/nonstdlib/map_intf.ml
@@ -7,60 +7,127 @@
 
 open NS0
 
+exception Not_found = Stdlib.Not_found
+
 module type S = sig
   type key
+  type +'a t [@@deriving compare, equal, sexp_of]
 
-  module Key : sig
-    type t = key
-
-    include Comparator.S with type t := t
+  module Provide_of_sexp (_ : sig
+    type t = key [@@deriving of_sexp]
+  end) : sig
+    val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t
   end
 
-  include Core_kernel.Map_intf.Make_S_plain_tree(Key).S
+  (** {1 Construct} *)
 
-  val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
-  val is_singleton : 'a t -> bool
+  val empty : 'a t
+  val singleton : key -> 'a -> 'a t
+  val add_exn : 'a t -> key:key -> data:'a -> 'a t
+  val set : 'a t -> key:key -> data:'a -> 'a t
+  val add_multi : 'a list t -> key:key -> data:'a -> 'a list t
+  val remove : 'a t -> key -> 'a t
 
-  val map_endo : 'a t -> f:('a -> 'a) -> 'a t
-  (** Like map, but specialized to require [f] to be an endofunction, which
-      enables preserving [==] if [f] preserves [==] of every element. *)
+  val merge :
+       'a t
+    -> 'b t
+    -> f:
+         (   key:key
+          -> [`Left of 'a | `Both of 'a * 'b | `Right of 'b]
+          -> 'c option)
+    -> 'c t
 
   val merge_endo :
        'a t
     -> 'b t
     -> f:
          (   key:key
-          -> [`Both of 'a * 'b | `Left of 'a | `Right of 'b]
+          -> [`Left of 'a | `Both of 'a * 'b | `Right of 'b]
           -> 'a option)
     -> 'a t
   (** Like merge, but specialized to require [f] to preserve the type of the
       left argument, which enables preserving [==] if [f] preserves [==] of
-      every element. *)
+      every value. *)
 
   val merge_skewed :
     'a t -> 'a t -> combine:(key:key -> 'a -> 'a -> 'a) -> 'a t
 
-  val fold_until :
-       'v t
-    -> init:'a
-    -> f:(key:key -> data:'v -> 'a -> ('a, 'r) Continue_or_stop.t)
-    -> finish:('a -> 'r)
-    -> 'r
+  val union : 'a t -> 'a t -> f:(key -> 'a -> 'a -> 'a option) -> 'a t
 
-  val choose_exn : 'a t -> key * 'a
-  (** Find an unspecified element. [O(1)]. *)
+  (** {1 Query} *)
+
+  val is_empty : 'a t -> bool
+  val is_singleton : 'a t -> bool
+  val length : 'a t -> int
+
+  val choose_key : 'a t -> key option
+  (** Find an unspecified key. Different keys may be chosen for equivalent
+      maps. [O(1)]. *)
 
   val choose : 'a t -> (key * 'a) option
-  (** Find an unspecified element. [O(1)]. *)
+  (** Find an unspecified binding. Different bindings may be chosen for
+      equivalent maps. [O(1)]. *)
 
-  val pop : 'a t -> (key * 'a * 'a t) option
-  (** Find and remove an unspecified element. [O(1)]. *)
+  val choose_exn : 'a t -> key * 'a
+  (** Find an unspecified binding. Different bindings may be chosen for
+      equivalent maps. [O(1)]. *)
 
-  val pop_min_elt : 'a t -> (key * 'a * 'a t) option
-  (** Find and remove minimum element. [O(log n)]. *)
+  val min_binding : 'a t -> (key * 'a) option
+  val mem : 'a t -> key -> bool
+  val find : 'a t -> key -> 'a option
+  val find_exn : 'a t -> key -> 'a
+  val find_multi : 'a list t -> key -> 'a list
 
   val find_and_remove : 'a t -> key -> ('a * 'a t) option
-  (** Find and remove an element. *)
+  (** Find and remove the binding for a key. *)
+
+  val pop : 'a t -> (key * 'a * 'a t) option
+  (** Find and remove an unspecified binding. Different bindings may be
+      chosen for equivalent maps. [O(1)]. *)
+
+  val pop_min_binding : 'a t -> (key * 'a * 'a t) option
+  (** Find and remove binding with minimum key. [O(log n)]. *)
+
+  (** {1 Transform} *)
+
+  val change : 'a t -> key -> f:('a option -> 'a option) -> 'a t
+  val update : 'a t -> key -> f:('a option -> 'a) -> 'a t
+  val map : 'a t -> f:('a -> 'b) -> 'b t
+  val mapi : 'a t -> f:(key:key -> data:'a -> 'b) -> 'b t
+
+  val map_endo : 'a t -> f:('a -> 'a) -> 'a t
+  (** Like map, but specialized to require [f] to be an endofunction, which
+      enables preserving [==] if [f] preserves [==] of every value. *)
+
+  val filter_mapi : 'a t -> f:(key:key -> data:'a -> 'b option) -> 'b t
+
+  (** {1 Traverse} *)
+
+  val iter : 'a t -> f:('a -> unit) -> unit
+  val iteri : 'a t -> f:(key:key -> data:'a -> unit) -> unit
+  val existsi : 'a t -> f:(key:key -> data:'a -> bool) -> bool
+  val for_alli : 'a t -> f:(key:key -> data:'a -> bool) -> bool
+  val fold : 'a t -> init:'b -> f:(key:key -> data:'a -> 'b -> 'b) -> 'b
+
+  (** {1 Convert} *)
+
+  val to_alist :
+    ?key_order:[`Increasing | `Decreasing] -> 'a t -> (key * 'a) list
+
+  val data : 'a t -> 'a list
+
+  val to_iter2 :
+       'a t
+    -> 'b t
+    -> (key * [`Left of 'a | `Both of 'a * 'b | `Right of 'b]) iter
+
+  val symmetric_diff :
+       data_equal:('a -> 'b -> bool)
+    -> 'a t
+    -> 'b t
+    -> (key * [> `Left of 'a | `Unequal of 'a * 'b | `Right of 'b]) iter
+
+  (** {1 Pretty-print} *)
 
   val pp : key pp -> 'a pp -> 'a t pp
 
diff --git a/sledge/nonstdlib/qset.ml b/sledge/nonstdlib/qset.ml
index b1ff1f006..50f584178 100644
--- a/sledge/nonstdlib/qset.ml
+++ b/sledge/nonstdlib/qset.ml
@@ -80,8 +80,8 @@ struct
   let choose = M.choose
   let choose_exn = M.choose_exn
   let pop = M.pop
-  let min_elt = M.min_elt
-  let pop_min_elt = M.pop_min_elt
+  let min_elt = M.min_binding
+  let pop_min_elt = M.pop_min_binding
 
   let classify s =
     match pop s with
diff --git a/sledge/src/test/equality_test.ml b/sledge/src/test/equality_test.ml
index 7b803b2e1..f822e7d02 100644
--- a/sledge/src/test/equality_test.ml
+++ b/sledge/src/test/equality_test.ml
@@ -62,17 +62,17 @@ let%test_module _ =
         = (%y_6 rem %t_1)
 
       {sat= true;
-       rep= [[%t_1 ↦ ];
-             [%u_2 ↦ %t_1];
-             [%v_3 ↦ %t_1];
-             [%w_4 ↦ %t_1];
-             [%x_5 ↦ %t_1];
-             [%y_6 ↦ ];
-             [%z_7 ↦ %t_1];
-             [(%y_6 rem %v_3) ↦ %t_1];
-             [(%y_6 rem %z_7) ↦ %t_1];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [(%y_6 rem %z_7) ↦ %t_1];
+             [(%y_6 rem %v_3) ↦ %t_1];
+             [%z_7 ↦ %t_1];
+             [%y_6 ↦ ];
+             [%x_5 ↦ %t_1];
+             [%w_4 ↦ %t_1];
+             [%v_3 ↦ %t_1];
+             [%u_2 ↦ %t_1];
+             [%t_1 ↦ ]]} |}]
 
     let%test _ = implies_eq r3 t z
 
@@ -83,7 +83,7 @@ let%test_module _ =
       pp r15 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [(%x_5 ≠ 0) ↦ -1]; [%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r15 b (Term.signed 1 !1)
     let%test _ = implies_eq r15 (Term.unsigned 1 b) !1
diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml
index 314f4159b..6818497f4 100644
--- a/sledge/src/test/fol_test.ml
+++ b/sledge/src/test/fol_test.ml
@@ -66,7 +66,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f1 ;
-      [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]]} |}]
 
     let%test _ = is_unsat (add_eq !1 !1 f1)
 
@@ -76,7 +76,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f2 ;
-      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}]
 
     let f3 = of_eqs [(x + !0, x + !1)]
 
@@ -84,7 +84,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f3 ;
-      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}]
 
     let f4 = of_eqs [(x, y); (x + !0, y + !1)]
 
@@ -93,7 +93,7 @@ let%test_module _ =
     let%expect_test _ =
       pp_raw f4 ;
       [%expect
-        {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
+        {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}]
 
     let t1 = of_eqs [(!1, !1)]
 
@@ -109,7 +109,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw r0 ;
-      [%expect {| {sat= true; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]]} |}]
 
     let%expect_test _ =
       pp r0 ;
@@ -128,7 +128,7 @@ let%test_module _ =
 
         %x_5 = %y_6
 
-      {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}]
 
     let%test _ = implies_eq r1 x y
 
@@ -142,12 +142,12 @@ let%test_module _ =
         %x_5 = %y_6 = %z_7 = %x_5^
 
       {sat= true;
-       rep= [[%x_5 ↦ ];
-             [%y_6 ↦ %x_5];
-             [%z_7 ↦ %x_5];
-             [%x_5^ ↦ %x_5];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%x_5^ ↦ %x_5];
+             [%z_7 ↦ %x_5];
+             [%y_6 ↦ %x_5];
+             [%x_5 ↦ ]]} |}]
 
     let%test _ = implies_eq r2 x z
     let%test _ = implies_eq (inter r1 r2) x y
@@ -169,12 +169,12 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]; [-1 ↦ ]; [0 ↦ ]]}
+         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %w_4]; [%y_6 ↦ %w_4]; [%w_4 ↦ ]]}
 
         {sat= true;
-         rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]}
+         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %x_5]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]}
 
-        {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
+        {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}]
 
     let%test _ =
       let r = of_eqs [(w, y); (y, z)] in
@@ -189,21 +189,21 @@ let%test_module _ =
       pp_raw r3 ;
       [%expect
         {|
-        %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%z_7 × %y_6)
-      ∧ (%z_7 × (%y_6 × %y_6)) = %t_1
+        (%z_7 × (%y_6 × %y_6)) = %t_1
+      ∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%z_7 × %y_6)
 
       {sat= true;
-       rep= [[%t_1 ↦ (%y_6^2 × %z_7)];
-             [%u_2 ↦ %z_7];
-             [%v_3 ↦ %z_7];
-             [%w_4 ↦ %z_7];
-             [%x_5 ↦ %z_7];
-             [%y_6 ↦ ];
-             [%z_7 ↦ ];
-             [(%y_6 × %z_7) ↦ %z_7];
-             [(%y_6^2 × %z_7) ↦ ];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [(%z_7 × %y_6^2) ↦ ];
+             [(%z_7 × %y_6) ↦ %z_7];
+             [%z_7 ↦ ];
+             [%y_6 ↦ ];
+             [%x_5 ↦ %z_7];
+             [%w_4 ↦ %z_7];
+             [%v_3 ↦ %z_7];
+             [%u_2 ↦ %z_7];
+             [%t_1 ↦ (%z_7 × %y_6^2)]]} |}]
 
     let%test _ = not (implies_eq r3 t z) (* incomplete *)
     let%test _ = implies_eq r3 x z
@@ -216,15 +216,15 @@ let%test_module _ =
       pp_raw r4 ;
       [%expect
         {|
-        (-4 + %z_7) = %y_6 ∧ (3 + %z_7) = %w_4 ∧ (8 + %z_7) = %x_5
+        (8 + %z_7) = %x_5 ∧ (3 + %z_7) = %w_4 ∧ (-4 + %z_7) = %y_6
 
       {sat= true;
-       rep= [[%w_4 ↦ (%z_7 + 3)];
-             [%x_5 ↦ (%z_7 + 8)];
-             [%y_6 ↦ (%z_7 + -4)];
-             [%z_7 ↦ ];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%z_7 ↦ ];
+             [%y_6 ↦ (-4 + %z_7)];
+             [%x_5 ↦ (8 + %z_7)];
+             [%w_4 ↦ (3 + %z_7)]]} |}]
 
     let%test _ = implies_eq r4 x (w + !5)
     let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
@@ -242,7 +242,7 @@ let%test_module _ =
         {|
         1 = %x_5 = %y_6
 
-      {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ 1]; [%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r6 x y
 
@@ -255,25 +255,25 @@ let%test_module _ =
       pp (add_eq x z r7) ;
       [%expect
         {|
-          %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
+          %w_4 = %y_6 = %z_7 ∧ %v_3 = %x_5
     
         {sat= true;
-         rep= [[%v_3 ↦ ];
-               [%w_4 ↦ ];
-               [%x_5 ↦ %v_3];
-               [%y_6 ↦ %w_4];
-               [%z_7 ↦ %w_4];
+         rep= [[0 ↦ ];
                [-1 ↦ ];
-               [0 ↦ ]]}
+               [%z_7 ↦ %w_4];
+               [%y_6 ↦ %w_4];
+               [%x_5 ↦ %v_3];
+               [%w_4 ↦ ];
+               [%v_3 ↦ ]]}
 
         {sat= true;
-         rep= [[%v_3 ↦ ];
-               [%w_4 ↦ %v_3];
-               [%x_5 ↦ %v_3];
-               [%y_6 ↦ %v_3];
-               [%z_7 ↦ %v_3];
+         rep= [[0 ↦ ];
                [-1 ↦ ];
-               [0 ↦ ]]}
+               [%z_7 ↦ %v_3];
+               [%y_6 ↦ %v_3];
+               [%x_5 ↦ %v_3];
+               [%w_4 ↦ %v_3];
+               [%v_3 ↦ ]]}
 
           %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
 
@@ -299,13 +299,13 @@ let%test_module _ =
         %v_3 = %w_4 = %x_5 = %y_6 = %z_7
 
       {sat= true;
-       rep= [[%v_3 ↦ ];
-             [%w_4 ↦ %v_3];
-             [%x_5 ↦ %v_3];
-             [%y_6 ↦ %v_3];
-             [%z_7 ↦ %v_3];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%z_7 ↦ %v_3];
+             [%y_6 ↦ %v_3];
+             [%x_5 ↦ %v_3];
+             [%w_4 ↦ %v_3];
+             [%v_3 ↦ ]]} |}]
 
     let%test _ = normalize r7' w |> Term.equal v
 
@@ -322,10 +322,10 @@ let%test_module _ =
       pp_raw r8 ;
       [%expect
         {|
-        14 = %y_6 ∧ (13 × %z_7) = %x_5
+        (13 × %z_7) = %x_5 ∧ 14 = %y_6
     
       {sat= true;
-       rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%y_6 ↦ 14]; [%x_5 ↦ (13 × %z_7)]]} |}]
 
     let%test _ = implies_eq r8 y !14
 
@@ -337,10 +337,10 @@ let%test_module _ =
       [%expect
         {|
       {sat= true;
-       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
 
       {sat= true;
-       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]} |}]
 
     let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
 
@@ -356,10 +356,10 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
 
         {sat= true;
-         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
 
         (%z_7 - (%x_5 + 8))
 
@@ -395,7 +395,7 @@ let%test_module _ =
     let%expect_test _ =
       pp_raw r13 ;
       [%expect
-        {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
+        {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}]
 
     let%test _ = not (is_unsat r13) (* incomplete *)
 
@@ -406,7 +406,7 @@ let%test_module _ =
       pp_raw r14 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
 
@@ -418,12 +418,12 @@ let%test_module _ =
       [%expect
         {|
           {sat= true;
-           rep= [[%x_5 ↦ 1];
-                 [%y_6 ↦ ];
-                 [(%x_5 ≠ 0) ↦ -1];
-                 [(%y_6 ≠ 0) ↦ -1];
+           rep= [[0 ↦ ];
                  [-1 ↦ ];
-                 [0 ↦ ]]} |}]
+                 [(%y_6 ≠ 0) ↦ -1];
+                 [(%x_5 ≠ 0) ↦ -1];
+                 [%y_6 ↦ ];
+                 [%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
     let%test _ = implies_eq r14 b (Formula.inject Formula.tt)
@@ -435,7 +435,7 @@ let%test_module _ =
       pp_raw r15 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}]
 
     (* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *)
     let r16 =
@@ -446,12 +446,12 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[%x_5 ↦ (%y_6 + 1)];
-             [%y_6 ↦ ];
-             [%y_6^ ↦ (%y_6 + -2)];
-             [(%x_5 + -1)^ ↦ (%y_6 + 3)];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [(-1 + %x_5)^ ↦ (3 + %y_6)];
+             [%y_6^ ↦ (-2 + %y_6)];
+             [%y_6 ↦ ];
+             [%x_5 ↦ (1 + %y_6)]]} |}]
 
     let%test _ = is_unsat r16
 
@@ -463,12 +463,12 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[%x_5 ↦ ];
-             [%y_6 ↦ %x_5];
-             [%x_5^ ↦ %x_5];
-             [%y_6^ ↦ (%x_5 + -1)];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%y_6^ ↦ (-1 + %x_5)];
+             [%x_5^ ↦ %x_5];
+             [%y_6 ↦ %x_5];
+             [%x_5 ↦ ]]} |}]
 
     let%test _ = is_unsat r17
 
@@ -479,14 +479,14 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[%x_5 ↦ ];
-               [%y_6 ↦ ];
-               [%x_5^ ↦ %x_5];
-               [%y_6^ ↦ (%y_6 + -1)];
+         rep= [[0 ↦ ];
                [-1 ↦ ];
-               [0 ↦ ]]}
+               [%y_6^ ↦ (-1 + %y_6)];
+               [%x_5^ ↦ %x_5];
+               [%y_6 ↦ ];
+               [%x_5 ↦ ]]}
 
-          %x_5 = %x_5^ ∧ (-1 + %y_6) = %y_6^ |}]
+          (-1 + %y_6) = %y_6^ ∧ %x_5 = %x_5^ |}]
 
     let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
 
@@ -495,7 +495,7 @@ let%test_module _ =
       [%expect
         {|
           {sat= true;
-           rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}]
+           rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ 0]; [%y_6 ↦ 0]; [%x_5 ↦ 0]]} |}]
 
     let%test _ = implies_eq r19 z !0
 
diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml
index b70ce7e8c..392a51b48 100644
--- a/sledge/src/test/sh_test.ml
+++ b/sledge/src/test/sh_test.ml
@@ -145,7 +145,7 @@ let%test_module _ =
       pp q' ;
       [%expect
         {|
-        ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp
+        ∃ %x_6 .   (-1 + %y_7) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp
     
           ((-1 + %y_7) = %y_7^) ∧ emp
 
diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml
index 26663f1ba..8c096db4e 100644
--- a/sledge/src/test/solver_test.ml
+++ b/sledge/src/test/solver_test.ml
@@ -143,7 +143,7 @@ let%test_module _ =
         {|
         ( infer_frame:
             %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 .   %l_6 -[)-> ⟨16,%a_3⟩
-        ) infer_frame:   %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+        ) infer_frame:   (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ %a_2 = _ ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -159,7 +159,7 @@ let%test_module _ =
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
         ) infer_frame:
-            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+            (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -175,7 +175,7 @@ let%test_module _ =
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩
         ) infer_frame:
-            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+            (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -194,9 +194,9 @@ let%test_module _ =
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
-            %a_2 = %a0_10
+            (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+          ∧ %a_2 = %a0_10
           ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
@@ -216,9 +216,9 @@ let%test_module _ =
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
-            %a_2 = %a0_10
+            (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+          ∧ %a_2 = %a0_10
           ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
@@ -246,19 +246,19 @@ let%test_module _ =
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame:
-            ( (  %a_1 = %a_2
+            ( (  16 = %m_8
                ∧ 2 = %n_9
-               ∧ 16 = %m_8
+               ∧ %a_1 = %a_2
                ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
-            ∨ (  %a_3 = _
-               ∧ 1 = %n_9
+            ∨ (  (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ 16 = %m_8
-               ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
+               ∧ 1 = %n_9
+               ∧ %a_3 = _
                ∧ emp)
-            ∨ (  %a_3 = _
-               ∧ 0 = %n_9
+            ∨ (  (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
                ∧ 16 = %m_8
-               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
+               ∧ 0 = %n_9
+               ∧ %a_3 = _
                ∧ emp)
             ) |}]
 
diff --git a/sledge/src/test/term_test.ml b/sledge/src/test/term_test.ml
index 532a1e588..5d7b659fc 100644
--- a/sledge/src/test/term_test.ml
+++ b/sledge/src/test/term_test.ml
@@ -54,7 +54,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (z + !42 + !13) ;
-      [%expect {| (%z_2 + 55) |}]
+      [%expect {| (55 + %z_2) |}]
 
     let%expect_test _ =
       pp (z + !42 + !(-42)) ;
@@ -62,15 +62,15 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (z * y) ;
-      [%expect {| (%y_1 × %z_2) |}]
+      [%expect {| (%z_2 × %y_1) |}]
 
     let%expect_test _ =
       pp (y * z * y) ;
-      [%expect {| (%y_1^2 × %z_2) |}]
+      [%expect {| (%z_2 × %y_1^2) |}]
 
     let%expect_test _ =
       pp ((!2 * z * z) + (!3 * z) + !4) ;
-      [%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}]
+      [%expect {| (4 + 2 × (%z_2^2) + 3 × %z_2) |}]
 
     let%expect_test _ =
       pp
@@ -85,9 +85,8 @@ let%test_module _ =
         + (!9 * z * z * z) ) ;
       [%expect
         {|
-         (3 × %y_1 + 2 × %z_2 + 6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2)
-           + 5 × (%y_1^2) + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3)
-           + 1) |}]
+         (1 + 9 × (%z_2^3) + 4 × (%z_2^2) + 7 × (%z_2 × %y_1^2) + 5 × (%y_1^2)
+           + 8 × (%z_2^2 × %y_1) + 6 × (%z_2 × %y_1) + 2 × %z_2 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp (!0 * z * y) ;
@@ -95,19 +94,19 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (!1 * z * y) ;
-      [%expect {| (%y_1 × %z_2) |}]
+      [%expect {| (%z_2 × %y_1) |}]
 
     let%expect_test _ =
       pp (!7 * z * (!2 * y)) ;
-      [%expect {| (14 × (%y_1 × %z_2)) |}]
+      [%expect {| (14 × (%z_2 × %y_1)) |}]
 
     let%expect_test _ =
       pp (!13 + (!42 * z)) ;
-      [%expect {| (42 × %z_2 + 13) |}]
+      [%expect {| (13 + 42 × %z_2) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42) ;
-      [%expect {| (13 × %z_2 + 42) |}]
+      [%expect {| (42 + 13 × %z_2) |}]
 
     let%expect_test _ =
       pp ((!2 * z) - !3 + ((!(-2) * z) + !3)) ;
@@ -115,31 +114,31 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!3 * y) + (!13 * z) + !42) ;
-      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
+      [%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y)) ;
-      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
+      [%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!2 * z)) ;
-      [%expect {| (3 × %y_1 + 15 × %z_2 + 42) |}]
+      [%expect {| (42 + 15 × %z_2 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!(-13) * z)) ;
-      [%expect {| (3 × %y_1 + 42) |}]
+      [%expect {| (42 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp (z + !42 + ((!3 * y) + (!(-1) * z))) ;
-      [%expect {| (3 × %y_1 + 42) |}]
+      [%expect {| (42 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp (!(-1) * (z + (!(-1) * y))) ;
-      [%expect {| (%y_1 + -1 × %z_2) |}]
+      [%expect {| (-1 × %z_2 + %y_1) |}]
 
     let%expect_test _ =
       pp (((!3 * y) + !2) * (!4 + (!5 * z))) ;
-      [%expect {| (12 × %y_1 + 10 × %z_2 + 15 × (%y_1 × %z_2) + 8) |}]
+      [%expect {| (8 + 15 × (%z_2 × %y_1) + 10 × %z_2 + 12 × %y_1) |}]
 
     let%expect_test _ =
       pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ;
@@ -147,7 +146,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!13 * z) + !42 - ((!3 * y) + (!13 * z))) ;
-      [%expect {| (-3 × %y_1 + 42) |}]
+      [%expect {| (42 + -3 × %y_1) |}]
 
     let%expect_test _ =
       pp (z = y) ;
@@ -183,47 +182,47 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (y - (!(-3) * y) + !4) ;
-      [%expect {| (4 × %y_1 + 4) |}]
+      [%expect {| (4 + 4 × %y_1) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 - y) ;
-      [%expect {| (-4 × %y_1 + 4) |}]
+      [%expect {| (4 + -4 × %y_1) |}]
 
     let%expect_test _ =
       pp (y = (!(-3) * y) + !4) ;
-      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
+      [%expect {| (%y_1 = (4 + -3 × %y_1)) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 = y) ;
-      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
+      [%expect {| (%y_1 = (4 + -3 × %y_1)) |}]
 
     let%expect_test _ =
       pp (sub true_ (z = !4)) ;
-      [%expect {| (-1 × (%z_2 = 4) + -1) |}]
+      [%expect {| (-1 + -1 × (%z_2 = 4)) |}]
 
     let%expect_test _ =
       pp (add true_ (z = !4) = (z = !4)) ;
-      [%expect {| ((%z_2 = 4) = ((%z_2 = 4) + -1)) |}]
+      [%expect {| ((%z_2 = 4) = (-1 + (%z_2 = 4))) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
+      [%expect {| ((13 × %z_2 + 3 × %y_1) = (42 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
+      [%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
+      [%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (10 × %z_2 + 42)) |}]
+      [%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 10 × %z_2)) |}]
 
     let%expect_test _ =
       pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
+      [%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ~~(!2 < y && z <= !3) ;
@@ -252,7 +251,7 @@ let%test_module _ =
       pp (z1_2 * z1_2) ;
       [%expect
         {|
-        (2 × %z_2 + (%z_2^2) + 1)
+        (1 + (%z_2^2) + 2 × %z_2)
 
-        (4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}]
+        (1 + (%z_2^4) + 4 × (%z_2^3) + 6 × (%z_2^2) + 4 × %z_2) |}]
   end )