From 429ddee9f516b02f2bd91cd0a2a914f4ea68504c Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 20 Oct 2020 11:42:15 -0700
Subject: [PATCH] [sledge] Add test for chunking segments when printing Sh

Reviewed By: ngorogiannis

Differential Revision: D24306042

fbshipit-source-id: d4748a95d
---
 sledge/src/test/sh_test.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml
index 51898fd95..ecd2335f5 100644
--- a/sledge/src/test/sh_test.ml
+++ b/sledge/src/test/sh_test.ml
@@ -24,6 +24,7 @@ let%test_module _ =
     let pp_djn = Format.printf "@\n%a@." pp_djn
     let ( ~$ ) = Var.Set.of_list
     let ( ! ) i = Term.integer (Z.of_int i)
+    let ( + ) = Term.add
     let ( - ) = Term.sub
     let ( = ) = Formula.eq
     let f = Term.splat (* any uninterpreted function *)
@@ -53,6 +54,14 @@ let%test_module _ =
     let of_eqs l =
       List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Formula.eq a b) q) l
 
+    let%expect_test _ =
+      pp
+        (star
+           (seg {loc= x; bas= x; len= !16; siz= !8; seq= a})
+           (seg {loc= x + !8; bas= x; len= !16; siz= !8; seq= b})) ;
+      [%expect {|
+          %x_6 -[)-> ⟨8,%a_1⟩^⟨8,%b_2⟩ |}]
+
     let%expect_test _ =
       let p = exists ~$[x_] (extend_us ~$[x_] emp) in
       let q = pure (x = !0) in