Use context of X.make

src/lib/reasoners/adt.ml

@@ -169,16 +169,16 @@ module Shostak (X : ALIEN) = struct
     assert (not @@ Options.get_disable_adts ());
     Log.debug (fun k -> k "make %a" E.print t);
     let { E.f; xs; ty; _ } = E.term_view t in
-    let sx, ctx =
+    let ssx, ctx =
       List.fold_left
         (fun (args, ctx) s ->
            let rs, ctx' = X.make s in
            rs :: args, List.rev_append ctx' ctx
         )([], []) xs
     in
-    let xs = List.rev sx in
-    match f, xs, ty with
-    | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) ->
+    let xxs = List.rev ssx in
+    match f, ty with
+    | Sy.Op Sy.Constr hs, Ty.Tadt (name, params) ->
       let cases = Ty.type_body name params in
       let case_hs =
         try Ty.assoc_destrs hs cases with Not_found -> assert false
@@ -188,12 +188,22 @@ module Shostak (X : ALIEN) = struct
           List.rev @@
           List.fold_left2
             (fun c_args v (lbl, _) -> (lbl, v) :: c_args)
-            [] xs case_hs
+            [] xxs case_hs
         with Invalid_argument _ -> assert false
       in
+      let ctx =
+        match cases with
+        | [{ destrs; _ }] ->
+          List.fold_left2
+            (fun ctx x (d, d_ty) ->
+               let access = E.mk_term (Sy.destruct d) [t] d_ty in
+               E.mk_eq ~iff:false x access :: ctx
+            ) ctx xs destrs
+        | _ -> ctx
+      in
       is_mine @@ Constr {c_name = hs; c_ty = ty; c_args}, ctx
 
-    | Sy.Op Sy.Destruct _, [_], _ -> X.term_embed t, ctx
+    | Sy.Op Sy.Destruct _, _ -> X.term_embed t, ctx
     (* No risk !
          if equal sel (embed sel_x) then X.term_embed t, ctx
          else sel_x, ctx (* canonization OK *)

src/lib/reasoners/adt_rel.ml

@@ -472,12 +472,12 @@ let build_constr_eq r c =
         in
         let xs = List.map (fun (_, ty) -> E.fresh_name ty) ds in
         let cons = E.mk_constr c xs ty in
-        let r', ctx = X.make cons in
+        let r', _ctx = X.make cons in
         (* In the current implementation of `X.make`, we produce
            a nonempty context only for interpreted semantic values
            of the `Arith` and `Records` theories. The semantic
            values `cons` never involves such values. *)
-        assert (Compat.List.is_empty ctx);
+        (*         assert (Compat.List.is_empty ctx); *)
         let eq = Shostak.L.(view @@ mk_eq r r') in
         Some (eq, E.mk_constr c xs ty)
 

src/lib/reasoners/shostak.ml

@@ -27,6 +27,9 @@
 
 (*** Combination module of Shostak theories ***)
 
+module E = Expr
+module Sy = Symbols
+
 [@@@ocaml.warning "-60"]
 module rec CX : sig
   include Sig.X