[sledge] Tighten test for uninterp terms in Context.solve_uninterp_eqs

Summary:
Context.solve_uninterp_eqs uses `not Theory.is_interpreted` where
`Theory.is_noninterpreted` is more correct, since it operates on terms
that are class elements, which cannot be `Z _ | Q _ | Concat [||]`.

Reviewed By: jvillard

Differential Revision: D25883732

fbshipit-source-id: 5d060b338

sledge/src/fol/context.ml

@@ -995,7 +995,7 @@ type cls_solve_state =
 let dom_trm e =
   match (e : Trm.t) with
   | Sized {seq= Var _ as v} -> Some v
-  | _ when not (Theory.is_interpreted e) -> Some e
+  | _ when Theory.is_noninterpreted e -> Some e
   | _ -> None
 
 (** move equations from [cls] (which is assumed to be normalized by [subst])