diff --git a/patronus-egraphs/src/arithmetic.rs b/patronus-egraphs/src/arithmetic.rs index 80ed019..b4bd9bd 100644 --- a/patronus-egraphs/src/arithmetic.rs +++ b/patronus-egraphs/src/arithmetic.rs @@ -58,7 +58,8 @@ pub fn create_rewrites() -> Vec { arith_rewrite!("merge-left-shift"; // we require that b, c and (b + c) are all unsigned // we do not want (b + c) to wrap, because in that case the result would always be zero - "(<< ?wo ?wab unsign (<< ?wab ?wa ?sa ?a ?wb unsign ?b) ?wc unsign ?c)" => + // the value being shifted has to be consistently signed or unsigned + "(<< ?wo ?wab ?sa (<< ?wab ?wa ?sa ?a ?wb unsign ?b) ?wc unsign ?c)" => "(<< ?wo ?wa ?sa ?a (max+1 ?wb ?wc) unsign (+ (max+1 ?wb ?wc) ?wb unsign ?b ?wc unsign ?c))"; // wab >= wo if["?wo", "?wab"], |w| w[1] >= w[0]),