diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f27d8e681..a1e7a4745 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1053,7 +1053,6 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
     func_decls fs;
     if (!m_func_decls.find(s, fs)) {
         if (num_args == 0) {
-            //UNREACHABLE();
             throw cmd_exception("unknown constant ", s);
         }
         else
@@ -1065,7 +1064,6 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
             throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disumbiguate ", s);
         func_decl * f = fs.first();
         if (f == 0) {
-            //UNREACHABLE();
             throw cmd_exception("unknown constant ", s);
         }
         if (f->get_arity() != 0)
@@ -1075,8 +1073,20 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
     else {
         func_decl * f = fs.find(m(), num_args, args, range);
         if (f == 0) {
-            //UNREACHABLE();
-            throw cmd_exception("unknown constant ", s);
+            std::ostringstream buffer;
+            buffer << "unknown constant " << s << " ";
+            buffer << " (";
+            bool first = true;
+            for (unsigned i = 0; i < num_args; ++i, first = false) {
+                if (!first) buffer << " ";
+                buffer << mk_pp(m().get_sort(args[i]), m());
+            }            
+            buffer << ") ";
+            if (range) buffer << mk_pp(range, m()) << " ";
+            for (unsigned i = 0; i < fs.get_num_entries(); ++i) {
+                buffer << "\ndeclared: " << mk_pp(fs.get_entry(i), m()) << " ";
+            }
+            throw cmd_exception(buffer.str().c_str());
         }
         if (well_sorted_check_enabled())
             m().check_sort(f, num_args, args);
diff --git a/src/util/container_util.h b/src/util/container_util.h
index 7bbc3fb08..3b287ad51 100644
--- a/src/util/container_util.h
+++ b/src/util/container_util.h
@@ -31,7 +31,7 @@ Revision History:
 template<class Set1, class Set2>
     void set_intersection(Set1 & tgt, const Set2 & src) {
     svector<typename Set1::data> to_remove;
-    for (Set1::data itm : tgt) 
+    for (auto const& itm : tgt) 
         if (!src.contains(itm)) 
             to_remove.push_back(itm);
     while (!to_remove.empty()) {