[sledge] Relax 'no new subexps' invariant for Xor expressions

Summary:
Boolean Xor expressions are treated directly by the solver, so the 'no
new subexps' invariant for congruence closure is not needed.

Reviewed By: mbouaziz

Differential Revision: D15098817

fbshipit-source-id: d118c5881

sledge/src/llair/exp.ml

@@ -1140,7 +1140,7 @@ let app1 ?(partial = false) op arg =
   |> check (fun e ->
          (* every App subexp of output appears in input *)
          match op with
-         | App {op= Eq | Dq} -> ()
+         | App {op= Eq | Dq | Xor} -> ()
          | _ -> (
            match e with
            | App {op= App {op= App {op= Conditional}}} -> ()