[pulse][arith] eval constant terms before other simplifications

Summary:
The simplifications done by `simplify_shallow` are all taken care of by
`eval_const_shallow` as well, they just also happen to help when not
*all* of the term is a constant. However, they might be less
precise/efficient than in the constant case, in particular in the next
diff that translates `x << c` into `x * 2^c` when `c` is constant.

Reviewed By: skcho

Differential Revision: D27464805

fbshipit-source-id: 452bc6ab1

infer/src/pulse/PulseFormula.ml

@@ -968,7 +968,7 @@ module Atom = struct
   let rec eval_term t =
     let t =
       Term.map_direct_subterms ~f:eval_term t
-      |> Term.simplify_shallow |> Term.eval_const_shallow |> Term.linearize |> Term.simplify_linear
+      |> Term.eval_const_shallow |> Term.simplify_shallow |> Term.linearize |> Term.simplify_linear
     in
     match atom_of_term t with
     | Some atom ->