From 94ddbc957727b6a71064a608a869405d49eb9dcb Mon Sep 17 00:00:00 2001
From: Roland Coeurjoly <rolandcoeurjoly@gmail.com>
Date: Wed, 26 Jun 2024 19:45:54 +0200
Subject: [PATCH] Fix reduce_or

---
 backends/functional/smtlib.cc | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/backends/functional/smtlib.cc b/backends/functional/smtlib.cc
index 671b3a763..2ece98d89 100644
--- 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) {