Normalize ADT in assume

Fix issue #1096

src/lib/reasoners/adt_rel.ml

@@ -431,6 +431,8 @@ let assume_literals la uf env =
        match lit with
        | Eq (r1, r2) as l, _, ex, Th_util.Subst when is_adt r1 ->
          Debug.assume l;
+         let r1, _ = Uf.find_r uf r1 in
+         let r2, _ = Uf.find_r uf r2 in
          (* Needed for models generation because fresh terms are not added with
             the function add. *)
          let env = add_rec r1 uf env in
@@ -439,6 +441,8 @@ let assume_literals la uf env =
 
        | Distinct (false, [r1; r2]) as l, _, ex, _ when is_adt r2 ->
          Debug.assume l;
+         let r1, _ = Uf.find_r uf r1 in
+         let r2, _ = Uf.find_r uf r2 in
          (* Needed for models generation because fresh terms are not added with
             the function add. *)
          let env = add_rec r1 uf env in
@@ -447,10 +451,12 @@ let assume_literals la uf env =
 
        | Builtin (true, Sy.IsConstr c, [r]) as l, _, ex, _ ->
          Debug.assume l;
+         let r, _ = Uf.find_r uf r in
          assume_is_constr ~ex r c env
 
        | Builtin (false, Sy.IsConstr c, [r]) as l, _, ex, _ ->
          Debug.assume l;
+         let r, _ = Uf.find_r uf r in
          assume_not_is_constr ~ex r c env
 
        | _ ->