diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index 86717c807..e8763475b 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -112,7 +112,7 @@ class dt2bv_tactic : public tactic {
                 unsigned idx = m_t.m_dt.get_constructor_idx(f);
                 result = m_t.m_bv.mk_numeral(idx, bv_size);
             }
-            else {
+            else if (is_uninterp_const(a)) {
                 // create a fresh variable, add bounds constraints for it.
                 unsigned nc = m_t.m_dt.get_datatype_num_constructors(s);
                 result = m.mk_fresh_const(f->get_name().str().c_str(), m_t.m_bv.mk_sort(bv_size));
@@ -130,6 +130,9 @@ class dt2bv_tactic : public tactic {
                 m_t.m_ext->insert(f, f_def);
                 m_t.m_filter->insert(to_app(result)->get_decl());
             }
+            else {
+                return false;
+            }
             m_cache.insert(a, result);
             ++m_t.m_num_translated;
             return true;