diff --git a/sledge/lib/domain_sh.ml b/sledge/lib/domain_sh.ml
index 11fb9eed6..280c652dc 100644
--- a/sledge/lib/domain_sh.ml
+++ b/sledge/lib/domain_sh.ml
@@ -130,9 +130,9 @@ let localize_entry globals actuals formals freturn locals subst pre entry =
   let foot = Sh.exists formals_set function_summary_pre in
   let xs, foot = Sh.bind_exists ~wrt:pre.Sh.us foot in
   let frame =
-    Option.value_exn
-      (Solver.infer_frame pre xs foot)
-      ~message:"Solver couldn't infer frame of a garbage-collected pre"
+    try Option.value_exn (Solver.infer_frame pre xs foot)
+    with _ ->
+      fail "Solver couldn't infer frame of a garbage-collected pre" ()
   in
   let q'' =
     Sh.extend_us freturn_locals (and_eqs subst formals actuals foot)
diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index b4918b276..f4965e29b 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -107,14 +107,14 @@ end = struct
   (** compose a substitution with a mapping *)
   let compose1 ~key ~data s =
     if Term.equal key data then s
-    else compose s (Term.Map.set Term.Map.empty ~key ~data)
+    else compose s (Term.Map.singleton key data)
 
   (** add an identity entry if the term is not already present *)
   let extend e s =
     let exception Found in
     match
       Term.Map.update s e ~f:(function
-        | Some _ -> Exn.raise_without_backtrace Found
+        | Some _ -> raise_notrace Found
         | None -> e )
     with
     | exception Found -> None
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 37d73fb4f..51948c2f6 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -624,7 +624,7 @@ let rec simp_and x y =
   | Integer {data= i}, Integer {data= j} -> integer (Z.logand i j)
   (* e && true ==> e *)
   | (Integer {data}, e | e, Integer {data}) when Z.is_true data -> e
-  (* e && false ==> 0 *)
+  (* e && false ==> false *)
   | ((Integer {data} as f), _ | _, (Integer {data} as f))
     when Z.is_false data ->
       f