Fix issue 1212

During model extraction, we only should store accesses to arrays whose the
representative elements are names. Indeed, if the representative is not
a name, this array cannot appear in a model.

The embedded case is correctly managed because we generate fresh names
that will become the representative elements.

src/lib/reasoners/uf.ml

@@ -1158,11 +1158,12 @@ end
 
 type cache = {
   array_selects: Expr.t E.Table.t E.Table.t;
-  (** Stores all the get accesses to arrays. *)
+  (** Stores all the get accesses to array names. *)
 
   abstracts: Expr.t Shostak.HX.t;
   (** Stores all the abstract values generated. This cache is necessary
-      to ensure we don't generate twice an abstract value for a given symbol. *)
+      to ensure we do not generate twice an abstract value for a given
+      symbol. *)
 }
 
 let is_destructor = function
@@ -1224,8 +1225,13 @@ let compute_concrete_model_of_val cache =
 
         | Sy.Op Sy.Get, [a; i], _ ->
           begin
-            store_array_select a i ret_rep;
-            acc
+            let E.{ f = fa; _ } = E.term_view a in
+            match fa with
+            | Sy.Name _ ->
+              store_array_select a i ret_rep;
+              acc
+            | _ ->
+              acc
           end
 
         | Sy.Name { hs = id; _ }, _, _ ->
@@ -1273,8 +1279,7 @@ let extract_concrete_model cache =
             | Sy.Name { hs; ns = User; _ } -> hs, true
             | Sy.Name { hs; _ } -> hs, false
             | _ ->
-              (* We only store array declarations as keys in the cache
-                 [array_selects]. *)
+              (* Excluded in [compute_concrete_model_of_val] *)
               assert false
           in
           let mdl =

tests/issues/1212.default.expected

@@ -0,0 +1,6 @@
+
+unknown
+(
+  (define-fun a () (Array Int Int) (as @a3 (Array Int Int)))
+  (define-fun b () (Array Int Int) (as @a2 (Array Int Int)))
+)

tests/issues/1212.default.smt2

@@ -0,0 +1,7 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const a (Array Int Int))
+(declare-const b (Array Int Int))
+(assert (= (store a 0 0) (store b 0 0)))
+(check-sat)
+(get-model)