[sledge] Improve test in Context.propagate1

Summary:
Currently `not Theory.is_interpreted` is used to terms should be added
to classes, or delayed to pending equations. This diff changes this to
use `Theory.is_noninterpreted` instead. They only differ on `Z _ | Q _
| Concat [||]`, which do not make it to this test, and
`is_noninterpreted` is more correct since classes may only contain
solvables.

Reviewed By: jvillard

Differential Revision: D25883706

fbshipit-source-id: 3b7b94065

sledge/src/fol/context.ml

@@ -448,8 +448,8 @@ let propagate1 (a, a') x =
           |> Option.value ~default:(Cls.empty, x.cls)
         in
         let b0'_cls, pnd =
-          if Theory.is_interpreted b0' then (b0'_cls, (b0', b') :: x.pnd)
+          if Theory.is_noninterpreted b0' then (Cls.add b0' b0'_cls, x.pnd)
-          else (Cls.add b0' b0'_cls, x.pnd)
+          else (b0'_cls, (b0', b') :: x.pnd)
         in
         let rep =
           Cls.fold b0'_cls x.rep ~f:(fun c rep ->