diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp
index 446d1a49c..573873c89 100644
--- a/src/tactic/ufbv/ufbv_rewriter.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter.cpp
@@ -322,8 +322,27 @@ bool ufbv_rewriter::rewrite_visit_children(app * a) {
     while (j > 0) {
         expr * e = a->get_arg(--j);
         if (!m_rewrite_cache.contains(e) || !m_rewrite_cache.get(e).second) {
-            m_rewrite_todo.push_back(e);
-            res = false;
+            bool recursive = false;
+            unsigned sz = m_rewrite_todo.size();
+            expr * v = e;
+            if (m_rewrite_cache.contains(e)) {
+                expr_bool_pair const & ebp = m_rewrite_cache.get(e);
+                if (ebp.second)
+                    v = ebp.first;
+            }
+            for (unsigned i = sz; i > 0; i--) {
+                if (m_rewrite_todo[i - 1] == v) {
+                    recursive = true;
+                    TRACE("demodulator", tout << "Detected demodulator cycle: " <<
+                        mk_pp(a, m_manager) << " --> " << mk_pp(v, m_manager) << std::endl;);
+                    m_rewrite_cache.insert(e, expr_bool_pair(v, true));
+                    break;
+                }
+            }
+            if (!recursive) {
+                m_rewrite_todo.push_back(e);
+                res = false;
+            }
         }
     }
     return res;
@@ -347,7 +366,8 @@ expr * ufbv_rewriter::rewrite(expr * n) {
     while (!m_rewrite_todo.empty()) {
         TRACE("demodulator_stack", tout << "STACK: " << std::endl;
               for ( unsigned i = 0; i<m_rewrite_todo.size(); i++)
-                  tout << std::dec << i << ": " << std::hex << (size_t)m_rewrite_todo[i] << std::endl;
+                  tout << std::dec << i << ": " << std::hex << (size_t)m_rewrite_todo[i] <<
+                  " = " << mk_pp(m_rewrite_todo[i], m_manager) << std::endl;
               );
 
         expr * e = m_rewrite_todo.back();