From 9989ef65539d1fa5cc2a9941cb02a96773f38370 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Jun 2021 20:58:32 -0700
Subject: [PATCH] #5324

---
 src/sat/smt/euf_model.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 85cf24021..ce0fc29a7 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -77,12 +77,12 @@ namespace euf {
     }
 
     bool solver::include_func_interp(func_decl* f) {
-        if (f->is_skolem())
-            return false;
         if (f->get_family_id() == null_family_id)
             return true;
         if (f->get_family_id() == m.get_basic_family_id())
             return false;
+        if (f->is_skolem())
+            return false;
         euf::th_model_builder* mb = func_decl2solver(f);
         return mb && mb->include_func_interp(f);
     }
@@ -190,7 +190,7 @@ namespace euf {
             if (!is_app(e))
                 continue;
             app* a = to_app(e);
-            func_decl* f = a->get_decl();            
+            func_decl* f = a->get_decl();       
             if (!include_func_interp(f))
                 continue;
             if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(f))