From 9150290abed40f414835a172164664358a7c401a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 1 Jul 2021 12:26:45 -0700 Subject: [PATCH] [sledge] Minor improvement of Sh printing Summary: The output generated for `pp_raw` was incorrectly less raw for disjuncts than for their parent formulas. Differential Revision: D29441156 fbshipit-source-id: 3e4b42fe3 --- sledge/src/sh.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index dbfa495f8..ce66ebbe7 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -171,7 +171,7 @@ let pp_heap x ?pre ctx fs heap = && Term.equal s1.len s2.len && Context.implies ctx (Formula.eq (Term.add s1.loc s1.siz) s2.loc) in - let heap = List.map heap ~f:(map_seg ~f:(Context.normalize ctx)) in + let heap = List.map ~f:(map_seg ~f:(Context.normalize ctx)) heap in let blocks = List.group_succ ~eq (List.sort ~cmp heap) in List.pp ?pre "@ * " (pp_block x) fs blocks @@ -227,7 +227,7 @@ let rec pp_ ?var_strength ?vs ancestor_xs parent_ctx fs (pp_djn ?var_strength (Var.Set.union vs (Var.Set.union us xs)) (Var.Set.union ancestor_xs xs) - ctx) + (if Option.is_some var_strength then ctx else emp.ctx)) fs djns ) ; Format.pp_close_box fs ()