diff --git a/BugList.md b/BugList.md index feb185225..93101986d 100644 --- a/BugList.md +++ b/BugList.md @@ -88,6 +88,7 @@ Please contact us or submit a PR if something is missing or inaccurate. 81. InstCombine introduces UB when moving rem instructions (https://llvm.org/PR60906) 82. SimpleLoopUnswitch reverses branch condition incorrectly (https://llvm.org/PR63962) 83. Vectorization of loop reduction introduces an aligned store incorrectly (https://llvm.org/PR65212) +84. InstCombine: incorrect sink of FP math through select changes NaN payload (https://llvm.org/PR74297) ### Bugs found in Z3 diff --git a/smt/expr.cpp b/smt/expr.cpp index 45116166a..ed266e108 100644 --- a/smt/expr.cpp +++ b/smt/expr.cpp @@ -1797,6 +1797,10 @@ expr expr::concat(const expr &rhs) const { l == h2+1 && c.eq(d)) return a.concat(c.extract(h, l2)); + // (concat const (concat const2 x)) + if (isConst() && rhs.isConcat(a, b) && a.isConst()) + return concat(a).concat(b); + return binop_fold(rhs, Z3_mk_concat); } @@ -2042,12 +2046,21 @@ expr expr::mkIf(const expr &cond, const expr &then, const expr &els) { expr lhs, rhs; // (ite (= x 1) 1 0) -> x - if (then.isBV() && then.bits() == 1 && then.isOne() && els.isZero() && - cond.isEq(lhs, rhs) && lhs.isBV() && lhs.bits() == 1) { - if (lhs.isOne()) - return rhs; - if (rhs.isOne()) - return lhs; + // (ite (= x 1) 0 1) -> (not x) + if (then.isBV() && then.bits() == 1 && cond.isEq(lhs, rhs) && + lhs.isBV() && lhs.bits() == 1) { + if (then.isOne() && els.isZero()) { + if (lhs.isOne()) + return rhs; + if (rhs.isOne()) + return lhs; + } + if (then.isZero() && els.isOne()) { + if (lhs.isOne()) + return ~rhs; + if (rhs.isOne()) + return ~lhs; + } } // (ite c a (ite c2 a b)) -> (ite (or c c2) a b)