fix: multiplication of power-products can be either bitvector or real

SRI-CSL · Jan 4, 2021 · 37860ea · 37860ea
1 parent 0f2b8b3
commit 37860ea
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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: