diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 4049634cf..0d94864e6 100644 --- a/src/lib/reasoners/uf.ml +++ b/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 = diff --git a/tests/issues/1212.default.expected b/tests/issues/1212.default.expected new file mode 100644 index 000000000..a424dc7f6 --- /dev/null +++ b/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))) +) diff --git a/tests/issues/1212.default.smt2 b/tests/issues/1212.default.smt2 new file mode 100644 index 000000000..481c10d0e --- /dev/null +++ b/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)