diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 5ac8e7caa..be4c824b3 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -178,6 +178,10 @@ namespace euf {
                 mbS->add_value(n, *mdl, m_values);
             else if (auto* mbE = expr2solver(e))
                 mbE->add_value(n, *mdl, m_values);
+            else if (is_app(e) && to_app(e)->get_family_id() != m.get_basic_family_id()) {
+                m_values.set(id, e);
+                IF_VERBOSE(1, verbose_stream() << "creating self-value for " << mk_pp(e, m) << "\n");
+            }
             else {
                 IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
             }                
@@ -212,9 +216,10 @@ namespace euf {
                 args.reset();                
                 for (expr* arg : *a) {
                     enode* earg = get_enode(arg); 
-                    args.push_back(m_values.get(earg->get_root_id()));                
-                    CTRACE("euf", !args.back(), tout << "no value for " << bpp(earg) << "\n";);
-                    SASSERT(args.back());
+                    expr* val = m_values.get(earg->get_root_id());
+                    args.push_back(val);                
+                    CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";);
+                    SASSERT(val);
                 }
                 SASSERT(args.size() == arity);
                 if (!fi->get_entry(args.data()))