From 2be566a09b38f8aa025981b286d3cc6f7e9efb13 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 2 Mar 2020 08:42:58 -0800 Subject: [PATCH] [sledge] Fix Solver tracing Reviewed By: ngorogiannis Differential Revision: D20120273 fbshipit-source-id: b84e885ab --- sledge/src/symbheap/solver.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index ca2f0c7a0..40984a749 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -578,14 +578,14 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = List.fold_option dnf_minuend ~init:(Sh.false_ (Set.union minuend.us xs)) ~f:(fun remainders minuend -> - [%Trace.call fun {pf} -> pf "@[<2>minuend@ %a@]" Sh.pp minuend] + ([%Trace.call fun {pf} -> pf "@[<2>minuend@ %a@]" Sh.pp minuend] ; let ys, min = Sh.bind_exists minuend ~wrt:xs in let us = min.us in let com = Sh.emp in let+ remainder = List.find_map dnf_subtrahend ~f:(fun sub -> - [%Trace.call fun {pf} -> pf "@[<2>subtrahend@ %a@]" Sh.pp sub] + ([%Trace.call fun {pf} -> pf "@[<2>subtrahend@ %a@]" Sh.pp sub] ; let sub = Sh.extend_us us sub in let ws, sub = Sh.bind_exists sub ~wrt:xs in @@ -595,13 +595,13 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = let+ remainder = excise {us; com; min; xs; sub; zs; pgs= true} in - Sh.exists (Set.union ys ws) remainder + Sh.exists (Set.union ys ws) remainder) |> - [%Trace.retn fun {pf} -> pf "%a" Sh.pp] ) + [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)] ) in - Sh.or_ remainders remainder + Sh.or_ remainders remainder) |> - [%Trace.retn fun {pf} -> pf "%a" Sh.pp] ) + [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)] ) let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = fun minuend xs subtrahend ->