From ea08fcf65c75283da4c8dc11da3dd3a993a45047 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 15:15:48 -0700
Subject: [PATCH] invalid model regression

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_evaluator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 24b971590..54eeab216 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -172,7 +172,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             if (!m_model_completion)
                 return BR_FAILED;
 
-            if (!m_ar.is_as_array(f, g) || g->get_family_id() == null_family_id) {
+            if (!m_ar.is_as_array(f)) {
                 sort * s   = f->get_range();
                 expr * val = m_model.get_some_value(s);
                 m_model.register_decl(f, val);