diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index ecd9ee5cb..87a386251 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -1683,7 +1683,8 @@ namespace datalog {
         for (unsigned i = 0; i < rules.size(); ++i) {            
             out << (use_fixedpoint_extensions?"(rule ":"(assert ");
             expr* r = rules[i].get();
-            if (symbol::null != names[i]) {
+            symbol nm = names[i];
+            if (symbol::null != nm) {
                 out << "(! ";
             }
             if (use_fixedpoint_extensions) {
@@ -1692,8 +1693,13 @@ namespace datalog {
             else {
                 out << mk_smt_pp(r, m);
             }
-            if (symbol::null != names[i]) {
-                out << " :named " << names[i] << ")";
+            if (symbol::null != nm) {
+                while (fresh_names.contains(nm)) {
+                    std::ostringstream s;
+                    s << nm << "!";
+                    nm = symbol(s.str().c_str());
+                }
+                out << " :named " << nm << ")";
             }
             out << ")\n";
         }
diff --git a/src/muz_qe/model2expr.h b/src/muz_qe/model2expr.h
index 9a63d6b8c..2c1ed8d15 100644
--- a/src/muz_qe/model2expr.h
+++ b/src/muz_qe/model2expr.h
@@ -36,6 +36,7 @@ public:
     mk_fresh_name(): m_char('A'), m_num(0) {}
     void add(ast* a);
     symbol next();
+    bool contains(symbol const& s) const { return m_symbols.contains(s); }
 };