Fix reduce_or

YosysHQ · Jun 26, 2024 · 44518eb · 44518eb
1 parent 8e3e5f5
commit 44518eb
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/backends/functional/smtlib.cc b/backends/functional/smtlib.cc
@@ -152,7 +152,10 @@ struct SmtPrintVisitor {
   }
 
   std::string reduce_or(Node, Node a, int) {
-    return format("(distinct %0 #b0)", np(a));
+    std::stringstream ss;
+    // We use ite to set the result to bit vector, to ensure appropriate type
+    ss << "(ite (= " << np(a) << " #b" << std::string(a.width(), '0') << ") #b0 #b1)";
+    return ss.str();
   }
 
   std::string reduce_xor(Node, Node a, int) {