From 46abb011cbedcb834e07c281b4e3b65b0f5cb288 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sun, 25 Oct 2020 16:01:15 -0700
Subject: [PATCH] [sledge] Do not reverse Map.to_iter

Summary:
Preceding commit reversed Map.to_iter to match the previous behavior
of to_list.

Reviewed By: jvillard

Differential Revision: D24306051

fbshipit-source-id: aad12e434
---
 sledge/nonstdlib/map.ml          |   2 +-
 sledge/src/test/equality_test.ml |  22 ++--
 sledge/src/test/fol_test.ml      | 178 +++++++++++++++----------------
 sledge/src/test/sh_test.ml       |   6 +-
 sledge/src/test/solver_test.ml   |  40 +++----
 sledge/src/test/term_test.ml     |  63 +++++------
 6 files changed, 156 insertions(+), 155 deletions(-)

diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml
index 4fd91df2c..83346078b 100644
--- a/sledge/nonstdlib/map.ml
+++ b/sledge/nonstdlib/map.ml
@@ -161,7 +161,7 @@ end) : S with type key = Key.t = struct
   let fold m ~init ~f = M.fold (fun key data acc -> f ~key ~data acc) m init
   let keys = M.keys
   let values = M.values
-  let to_iter m = Iter.rev (M.to_iter m)
+  let to_iter = M.to_iter
 
   let to_iter2 l r =
     let seq = ref Iter.empty in
diff --git a/sledge/src/test/equality_test.ml b/sledge/src/test/equality_test.ml
index b92bdb557..b1e4faf91 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= [[0 ↦ ];
-             [-1 ↦ ];
-             [(%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];
+       rep= [[%t_1 ↦ ];
              [%u_2 ↦ %t_1];
-             [%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];
+             [-1 ↦ ];
+             [0 ↦ ]]} |}]
 
     let%test _ = implies_eq r3 t z
 
@@ -83,7 +83,7 @@ let%test_module _ =
       pp r15 ;
       [%expect
         {|
-          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [(%x_5 ≠ 0) ↦ -1]; [%x_5 ↦ 1]]} |}]
+          {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     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 32e8acd31..31ef18d97 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= [[0 ↦ ]; [-1 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
 
     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= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     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= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     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= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}]
+        {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     let t1 = of_eqs [(!1, !1)]
 
@@ -109,7 +109,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw r0 ;
-      [%expect {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]]} |}]
+      [%expect {| {sat= true; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
 
     let%expect_test _ =
       pp r0 ;
@@ -128,7 +128,7 @@ let%test_module _ =
 
         %x_5 = %y_6
 
-      {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}]
+      {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     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= [[0 ↦ ];
-             [-1 ↦ ];
-             [%x_5^ ↦ %x_5];
-             [%z_7 ↦ %x_5];
+       rep= [[%x_5 ↦ ];
              [%y_6 ↦ %x_5];
-             [%x_5 ↦ ]]} |}]
+             [%z_7 ↦ %x_5];
+             [%x_5^ ↦ %x_5];
+             [-1 ↦ ];
+             [0 ↦ ]]} |}]
 
     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= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %w_4]; [%y_6 ↦ %w_4]; [%w_4 ↦ ]]}
+         rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]; [-1 ↦ ]; [0 ↦ ]]}
 
         {sat= true;
-         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %x_5]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]}
+         rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]}
 
-        {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}]
+        {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     let%test _ =
       let r = of_eqs [(w, y); (y, z)] in
@@ -189,21 +189,21 @@ let%test_module _ =
       pp_raw r3 ;
       [%expect
         {|
-        (1 × (%z_7 × %y_6^2)) = %t_1
-      ∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (1 × (%z_7 × %y_6))
+        %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (1 × (%y_6 × %z_7))
+      ∧ (1 × (%y_6^2 × %z_7)) = %t_1
 
       {sat= true;
-       rep= [[0 ↦ ];
-             [-1 ↦ ];
-             [(%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];
+       rep= [[%t_1 ↦ (%y_6^2 × %z_7)];
              [%u_2 ↦ %z_7];
-             [%t_1 ↦ (%z_7 × %y_6^2)]]} |}]
+             [%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) ↦ ];
+             [-1 ↦ ];
+             [0 ↦ ]]} |}]
 
     let%test _ = not (implies_eq r3 t z) (* incomplete *)
     let%test _ = implies_eq r3 x z
@@ -216,17 +216,17 @@ let%test_module _ =
       pp_raw r4 ;
       [%expect
         {|
-        (1 × (%z_7) + 8) = %x_5
-      ∧ (1 × (%z_7) + 3) = %w_4
-      ∧ (1 × (%z_7) + -4) = %y_6
+        (-4 + 1 × (%z_7)) = %y_6
+      ∧ (3 + 1 × (%z_7)) = %w_4
+      ∧ (8 + 1 × (%z_7)) = %x_5
 
       {sat= true;
-       rep= [[0 ↦ ];
-             [-1 ↦ ];
+       rep= [[%w_4 ↦ (%z_7 + 3)];
+             [%x_5 ↦ (%z_7 + 8)];
+             [%y_6 ↦ (%z_7 + -4)];
              [%z_7 ↦ ];
-             [%y_6 ↦ (-4 + %z_7)];
-             [%x_5 ↦ (8 + %z_7)];
-             [%w_4 ↦ (3 + %z_7)]]} |}]
+             [-1 ↦ ];
+             [0 ↦ ]]} |}]
 
     let%test _ = implies_eq r4 x (w + !5)
     let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
@@ -244,7 +244,7 @@ let%test_module _ =
         {|
         1 = %x_5 = %y_6
 
-      {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ 1]; [%x_5 ↦ 1]]} |}]
+      {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     let%test _ = implies_eq r6 x y
 
@@ -257,25 +257,25 @@ let%test_module _ =
       pp (add_eq x z r7) ;
       [%expect
         {|
-          %w_4 = %y_6 = %z_7 ∧ %v_3 = %x_5
+          %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
     
         {sat= true;
-         rep= [[0 ↦ ];
-               [-1 ↦ ];
-               [%z_7 ↦ %w_4];
-               [%y_6 ↦ %w_4];
-               [%x_5 ↦ %v_3];
+         rep= [[%v_3 ↦ ];
                [%w_4 ↦ ];
-               [%v_3 ↦ ]]}
+               [%x_5 ↦ %v_3];
+               [%y_6 ↦ %w_4];
+               [%z_7 ↦ %w_4];
+               [-1 ↦ ];
+               [0 ↦ ]]}
 
         {sat= true;
-         rep= [[0 ↦ ];
-               [-1 ↦ ];
-               [%z_7 ↦ %v_3];
-               [%y_6 ↦ %v_3];
-               [%x_5 ↦ %v_3];
+         rep= [[%v_3 ↦ ];
                [%w_4 ↦ %v_3];
-               [%v_3 ↦ ]]}
+               [%x_5 ↦ %v_3];
+               [%y_6 ↦ %v_3];
+               [%z_7 ↦ %v_3];
+               [-1 ↦ ];
+               [0 ↦ ]]}
 
           %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
 
@@ -301,13 +301,13 @@ let%test_module _ =
         %v_3 = %w_4 = %x_5 = %y_6 = %z_7
 
       {sat= true;
-       rep= [[0 ↦ ];
-             [-1 ↦ ];
-             [%z_7 ↦ %v_3];
-             [%y_6 ↦ %v_3];
-             [%x_5 ↦ %v_3];
+       rep= [[%v_3 ↦ ];
              [%w_4 ↦ %v_3];
-             [%v_3 ↦ ]]} |}]
+             [%x_5 ↦ %v_3];
+             [%y_6 ↦ %v_3];
+             [%z_7 ↦ %v_3];
+             [-1 ↦ ];
+             [0 ↦ ]]} |}]
 
     let%test _ = normalize r7' w |> Term.equal v
 
@@ -324,10 +324,10 @@ let%test_module _ =
       pp_raw r8 ;
       [%expect
         {|
-        (13 × (%z_7)) = %x_5 ∧ 14 = %y_6
+        14 = %y_6 ∧ (13 × (%z_7)) = %x_5
     
       {sat= true;
-       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%y_6 ↦ 14]; [%x_5 ↦ (13 × %z_7)]]} |}]
+       rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     let%test _ = implies_eq r8 y !14
 
@@ -339,10 +339,10 @@ let%test_module _ =
       [%expect
         {|
       {sat= true;
-       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
+       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
 
       {sat= true;
-       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]} |}]
+       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
 
@@ -358,16 +358,16 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
+         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
 
         {sat= true;
-         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
+         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
 
-        (1 × (%z_7) + -1 × (%x_5) + -8)
+        (-8 + -1 × (%x_5) + 1 × (%z_7))
 
         8
 
-        (-1 × (%z_7) + 1 × (%x_5) + 8)
+        (8 + 1 × (%x_5) + -1 × (%z_7))
 
         -8 |}]
 
@@ -380,13 +380,13 @@ let%test_module _ =
 
     let%expect_test _ =
       pp r11 ;
-      [%expect {| (1 × (%z_7) + -16) = %x_5 |}]
+      [%expect {| (-16 + 1 × (%z_7)) = %x_5 |}]
 
     let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)]
 
     let%expect_test _ =
       pp r12 ;
-      [%expect {| (1 × (%z_7) + -16) = %x_5 |}]
+      [%expect {| (-16 + 1 × (%z_7)) = %x_5 |}]
 
     let r13 =
       of_eqs
@@ -397,7 +397,7 @@ let%test_module _ =
     let%expect_test _ =
       pp_raw r13 ;
       [%expect
-        {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}]
+        {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     let%test _ = not (is_unsat r13) (* incomplete *)
 
@@ -408,7 +408,7 @@ let%test_module _ =
       pp_raw r14 ;
       [%expect
         {|
-          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}]
+          {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
 
@@ -420,12 +420,12 @@ let%test_module _ =
       [%expect
         {|
           {sat= true;
-           rep= [[0 ↦ ];
-                 [-1 ↦ ];
-                 [(%y_6 ≠ 0) ↦ -1];
-                 [(%x_5 ≠ 0) ↦ -1];
+           rep= [[%x_5 ↦ 1];
                  [%y_6 ↦ ];
-                 [%x_5 ↦ 1]]} |}]
+                 [(%x_5 ≠ 0) ↦ -1];
+                 [(%y_6 ≠ 0) ↦ -1];
+                 [-1 ↦ ];
+                 [0 ↦ ]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
     let%test _ = implies_eq r14 b (Formula.inject Formula.tt)
@@ -437,7 +437,7 @@ let%test_module _ =
       pp_raw r15 ;
       [%expect
         {|
-          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}]
+          {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     (* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *)
     let r16 =
@@ -448,12 +448,12 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[0 ↦ ];
-             [-1 ↦ ];
-             [(-1 + %x_5)^ ↦ (3 + %y_6)];
-             [%y_6^ ↦ (-2 + %y_6)];
+       rep= [[%x_5 ↦ (%y_6 + 1)];
              [%y_6 ↦ ];
-             [%x_5 ↦ (1 + %y_6)]]} |}]
+             [%y_6^ ↦ (%y_6 + -2)];
+             [(%x_5 + -1)^ ↦ (%y_6 + 3)];
+             [-1 ↦ ];
+             [0 ↦ ]]} |}]
 
     let%test _ = is_unsat r16
 
@@ -465,12 +465,12 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[0 ↦ ];
-             [-1 ↦ ];
-             [%y_6^ ↦ (-1 + %x_5)];
-             [%x_5^ ↦ %x_5];
+       rep= [[%x_5 ↦ ];
              [%y_6 ↦ %x_5];
-             [%x_5 ↦ ]]} |}]
+             [%x_5^ ↦ %x_5];
+             [%y_6^ ↦ (%x_5 + -1)];
+             [-1 ↦ ];
+             [0 ↦ ]]} |}]
 
     let%test _ = is_unsat r17
 
@@ -481,14 +481,14 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[0 ↦ ];
-               [-1 ↦ ];
-               [%y_6^ ↦ (-1 + %y_6)];
-               [%x_5^ ↦ %x_5];
+         rep= [[%x_5 ↦ ];
                [%y_6 ↦ ];
-               [%x_5 ↦ ]]}
+               [%x_5^ ↦ %x_5];
+               [%y_6^ ↦ (%y_6 + -1)];
+               [-1 ↦ ];
+               [0 ↦ ]]}
 
-          (1 × (%y_6) + -1) = %y_6^ ∧ %x_5 = %x_5^ |}]
+          %x_5 = %x_5^ ∧ (-1 + 1 × (%y_6)) = %y_6^ |}]
 
     let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
 
@@ -497,7 +497,7 @@ let%test_module _ =
       [%expect
         {|
           {sat= true;
-           rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ 0]; [%y_6 ↦ 0]; [%x_5 ↦ 0]]} |}]
+           rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [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 63554468c..0cd44a65f 100644
--- a/sledge/src/test/sh_test.ml
+++ b/sledge/src/test/sh_test.ml
@@ -154,11 +154,11 @@ let%test_module _ =
       pp q' ;
       [%expect
         {|
-        ∃ %x_6 .   (1 × (%y_7) + -1) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp
+        ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + 1 × (%y_7)) = %y_7^ ∧ emp
 
-          (tt ∧ ((1 × (%y_7) + -1) = %y_7^)) ∧ emp
+          (tt ∧ ((-1 + 1 × (%y_7)) = %y_7^)) ∧ emp
 
-          (1 × (%y_7) + -1) = %y_7^ ∧ emp |}]
+          (-1 + 1 × (%y_7)) = %y_7^ ∧ emp |}]
 
     let%expect_test _ =
       let q =
diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml
index 279858d40..e4edc9da3 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:   (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ %a_2 = _ ∧ emp |}]
+        ) infer_frame:   %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 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:
-            (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}]
+            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 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:
-            (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}]
+            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -194,10 +194,10 @@ let%test_module _ =
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
-            (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+            %a_2 = %a0_10
           ∧ 16 = %m_8 = %n_9
-          ∧ %a_2 = %a0_10
-          ∧ (1 × (%k_5) + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+          ∧ (16 + 1 × (%k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
       infer_frame
@@ -216,10 +216,10 @@ let%test_module _ =
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
-            (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+            %a_2 = %a0_10
           ∧ 16 = %m_8 = %n_9
-          ∧ %a_2 = %a0_10
-          ∧ (1 × (%k_5) + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+          ∧ (16 + 1 × (%k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
       Sh.star
@@ -238,7 +238,7 @@ let%test_module _ =
         {|
         ( infer_frame:
             %l_6
-              -[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(-8 × (%n_9) + 16),%a_3⟩
+              -[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(16 + -8 × (%n_9)),%a_3⟩
           * ( (  1 = %n_9 ∧ emp)
             ∨ (  0 = %n_9 ∧ emp)
             ∨ (  2 = %n_9 ∧ emp)
@@ -246,19 +246,19 @@ let%test_module _ =
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame:
-            ( (  (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
-               ∧ 16 = %m_8
+            ( (  %a_3 = _
                ∧ 1 = %n_9
-               ∧ %a_3 = _
+               ∧ 16 = %m_8
+               ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ emp)
-            ∨ (  16 = %m_8
+            ∨ (  %a_1 = %a_2
                ∧ 2 = %n_9
-               ∧ %a_1 = %a_2
-               ∧ (1 × (%l_6) + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
-            ∨ (  (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
                ∧ 16 = %m_8
+               ∧ (16 + 1 × (%l_6)) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
+            ∨ (  %a_3 = _
                ∧ 0 = %n_9
-               ∧ %a_3 = _
+               ∧ 16 = %m_8
+               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
                ∧ emp)
             ) |}]
 
@@ -271,9 +271,9 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (0 ≥ (1 × (%n_9) + -2))
+            (0 ≥ (-2 + 1 × (%n_9)))
           ∧ %l_6
-              -[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(-8 × (%n_9) + 16),%a_3⟩
+              -[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(16 + -8 × (%n_9)),%a_3⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame: |}]
diff --git a/sledge/src/test/term_test.ml b/sledge/src/test/term_test.ml
index 5d7b659fc..532a1e588 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 {| (55 + %z_2) |}]
+      [%expect {| (%z_2 + 55) |}]
 
     let%expect_test _ =
       pp (z + !42 + !(-42)) ;
@@ -62,15 +62,15 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (z * y) ;
-      [%expect {| (%z_2 × %y_1) |}]
+      [%expect {| (%y_1 × %z_2) |}]
 
     let%expect_test _ =
       pp (y * z * y) ;
-      [%expect {| (%z_2 × %y_1^2) |}]
+      [%expect {| (%y_1^2 × %z_2) |}]
 
     let%expect_test _ =
       pp ((!2 * z * z) + (!3 * z) + !4) ;
-      [%expect {| (4 + 2 × (%z_2^2) + 3 × %z_2) |}]
+      [%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}]
 
     let%expect_test _ =
       pp
@@ -85,8 +85,9 @@ let%test_module _ =
         + (!9 * z * z * z) ) ;
       [%expect
         {|
-         (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) |}]
+         (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) |}]
 
     let%expect_test _ =
       pp (!0 * z * y) ;
@@ -94,19 +95,19 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (!1 * z * y) ;
-      [%expect {| (%z_2 × %y_1) |}]
+      [%expect {| (%y_1 × %z_2) |}]
 
     let%expect_test _ =
       pp (!7 * z * (!2 * y)) ;
-      [%expect {| (14 × (%z_2 × %y_1)) |}]
+      [%expect {| (14 × (%y_1 × %z_2)) |}]
 
     let%expect_test _ =
       pp (!13 + (!42 * z)) ;
-      [%expect {| (13 + 42 × %z_2) |}]
+      [%expect {| (42 × %z_2 + 13) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42) ;
-      [%expect {| (42 + 13 × %z_2) |}]
+      [%expect {| (13 × %z_2 + 42) |}]
 
     let%expect_test _ =
       pp ((!2 * z) - !3 + ((!(-2) * z) + !3)) ;
@@ -114,31 +115,31 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!3 * y) + (!13 * z) + !42) ;
-      [%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}]
+      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y)) ;
-      [%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}]
+      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!2 * z)) ;
-      [%expect {| (42 + 15 × %z_2 + 3 × %y_1) |}]
+      [%expect {| (3 × %y_1 + 15 × %z_2 + 42) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!(-13) * z)) ;
-      [%expect {| (42 + 3 × %y_1) |}]
+      [%expect {| (3 × %y_1 + 42) |}]
 
     let%expect_test _ =
       pp (z + !42 + ((!3 * y) + (!(-1) * z))) ;
-      [%expect {| (42 + 3 × %y_1) |}]
+      [%expect {| (3 × %y_1 + 42) |}]
 
     let%expect_test _ =
       pp (!(-1) * (z + (!(-1) * y))) ;
-      [%expect {| (-1 × %z_2 + %y_1) |}]
+      [%expect {| (%y_1 + -1 × %z_2) |}]
 
     let%expect_test _ =
       pp (((!3 * y) + !2) * (!4 + (!5 * z))) ;
-      [%expect {| (8 + 15 × (%z_2 × %y_1) + 10 × %z_2 + 12 × %y_1) |}]
+      [%expect {| (12 × %y_1 + 10 × %z_2 + 15 × (%y_1 × %z_2) + 8) |}]
 
     let%expect_test _ =
       pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ;
@@ -146,7 +147,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!13 * z) + !42 - ((!3 * y) + (!13 * z))) ;
-      [%expect {| (42 + -3 × %y_1) |}]
+      [%expect {| (-3 × %y_1 + 42) |}]
 
     let%expect_test _ =
       pp (z = y) ;
@@ -182,47 +183,47 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (y - (!(-3) * y) + !4) ;
-      [%expect {| (4 + 4 × %y_1) |}]
+      [%expect {| (4 × %y_1 + 4) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 - y) ;
-      [%expect {| (4 + -4 × %y_1) |}]
+      [%expect {| (-4 × %y_1 + 4) |}]
 
     let%expect_test _ =
       pp (y = (!(-3) * y) + !4) ;
-      [%expect {| (%y_1 = (4 + -3 × %y_1)) |}]
+      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 = y) ;
-      [%expect {| (%y_1 = (4 + -3 × %y_1)) |}]
+      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
 
     let%expect_test _ =
       pp (sub true_ (z = !4)) ;
-      [%expect {| (-1 + -1 × (%z_2 = 4)) |}]
+      [%expect {| (-1 × (%z_2 = 4) + -1) |}]
 
     let%expect_test _ =
       pp (add true_ (z = !4) = (z = !4)) ;
-      [%expect {| ((%z_2 = 4) = (-1 + (%z_2 = 4))) |}]
+      [%expect {| ((%z_2 = 4) = ((%z_2 = 4) + -1)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + 3 × %y_1) = (42 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 13 × %z_2)) |}]
+      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 10 × %z_2)) |}]
+      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (10 × %z_2 + 42)) |}]
 
     let%expect_test _ =
       pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
-      [%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}]
+      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
 
     let%expect_test _ =
       pp ~~(!2 < y && z <= !3) ;
@@ -251,7 +252,7 @@ let%test_module _ =
       pp (z1_2 * z1_2) ;
       [%expect
         {|
-        (1 + (%z_2^2) + 2 × %z_2)
+        (2 × %z_2 + (%z_2^2) + 1)
 
-        (1 + (%z_2^4) + 4 × (%z_2^3) + 6 × (%z_2^2) + 4 × %z_2) |}]
+        (4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}]
   end )