diff --git a/src/expr/term_manager.cpp b/src/expr/term_manager.cpp
index 4f8a95c..07ed0c4 100644
--- a/src/expr/term_manager.cpp
+++ b/src/expr/term_manager.cpp
@@ -884,6 +884,10 @@ bool term_manager::is_array_type(term_ref t) const {
   return d_tm->is_array_type(t);
 }
 
+bool term_manager::is_bitvector_type(term_ref t) const {
+  return d_tm->is_bitvector_type(t);
+}
+
 bool term_manager::is_integer_type(term_ref t) const {
   return d_tm->is_integer_type(t);
 }
diff --git a/src/expr/term_manager.h b/src/expr/term_manager.h
index 7ed84a3..64dd8da 100644
--- a/src/expr/term_manager.h
+++ b/src/expr/term_manager.h
@@ -444,6 +444,9 @@ class term_manager {
   /** Check if t is an array type */
   bool is_array_type(term_ref t) const;
 
+  /** Check if t is a bitvector type */
+  bool is_bitvector_type(term_ref t) const;
+
   /** Check if t is an integer type */
   bool is_integer_type(term_ref t) const;
 
diff --git a/src/smt/yices2/yices2_internal.cpp b/src/smt/yices2/yices2_internal.cpp
index fa3c34c..1b4d366 100644
--- a/src/smt/yices2/yices2_internal.cpp
+++ b/src/smt/yices2/yices2_internal.cpp
@@ -1077,7 +1077,11 @@ class to_term_visitor {
           pow_children.push_back(d_conversion_cache.get_term_cache(p_t));
         }
       }
-      result = d_tm.mk_term(expr::TERM_BV_MUL, pow_children);
+      if (yices_term_is_bitvector(yices_term)) {
+        result = d_tm.mk_term(expr::TERM_BV_MUL, pow_children);
+      } else {
+        result = d_tm.mk_term(expr::TERM_MUL, pow_children);
+      }
       break;
     }
     default: