From eefde76bd4a1b71d0316f4f644ad8d0f24df170a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Jul 2021 13:54:00 -0700 Subject: [PATCH] na --- src/smt/smt_model_generator.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 9422c2963..dcdb9a198 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -389,8 +389,7 @@ namespace smt { if (fid == null_family_id) return !m_hidden_ufs.contains(f); if (fid == m.get_basic_family_id()) return false; theory * th = m_context->get_theory(fid); - if (!th) return true; - return th->include_func_interp(f); + return !th || th->include_func_interp(f); } /**