Fix reduce_or

This commit is contained in:
Roland Coeurjoly 2024-06-26 19:45:54 +02:00 committed by Emily Schmidt
parent b98210d8ac
commit 94ddbc9577
1 changed files with 4 additions and 1 deletions

View File

@ -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) {