Skip to content

Commit c00c699

Browse files
authored
Avoid loss of sharing when pushing bitvector equality under ite (#105)
1 parent 84685ad commit c00c699

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

what4/src/What4/Expr/Builder.hs

+2
Original file line numberDiff line numberDiff line change
@@ -2301,11 +2301,13 @@ instance IsExprBuilder (ExprBuilder t st fs) where
23012301
-- Push some equalities under if/then/else
23022302
| SemiRingLiteral _ _ _ <- x
23032303
, Just (BaseIte _ _ c a b) <- asApp y
2304+
, isJust (asBV a) || isJust (asBV b) -- avoid loss of sharing
23042305
= join (itePred sym c <$> bvEq sym x a <*> bvEq sym x b)
23052306

23062307
-- Push some equalities under if/then/else
23072308
| Just (BaseIte _ _ c a b) <- asApp x
23082309
, SemiRingLiteral _ _ _ <- y
2310+
, isJust (asBV a) || isJust (asBV b) -- avoid loss of sharing
23092311
= join (itePred sym c <$> bvEq sym a y <*> bvEq sym b y)
23102312

23112313
| Just (Some flv) <- inSameBVSemiRing x y

0 commit comments

Comments
 (0)