diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index f0c0ec48e..fe85359e0 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -395,7 +395,7 @@ module Var = struct Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range -> Set.add range data ) - let apply sub v = try Map.find_exn sub v with Caml.Not_found -> v + let apply sub v = Map.find sub v |> Option.value ~default:v let apply_set sub vs = Map.fold sub ~init:vs ~f:(fun ~key ~data vs -> diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index f911211b6..b1e34fcb2 100644 --- a/sledge/src/symbheap/equality.ml +++ b/sledge/src/symbheap/equality.ml @@ -107,7 +107,7 @@ let invariant r = let true_ = {sat= true; rep= empty_map} |> check invariant (** apply a subst to a term *) -let apply s a = try Map.find_exn s a with Caml.Not_found -> a +let apply s a = Map.find s a |> Option.value ~default:a (** apply a subst to maximal non-interpreted subterms *) let rec norm s a =