steakhal wrote:
> > When asked some AI to confirm that this is NFC, it told me that there might
> > be an issue:
> > > Previously, when both `StateTrue` and `StateFalse` were `null` (the
> > > symbolic condition is unsatisfiable in the current state), `Pred`
> > > remained in the Frontier/Dst because `NodeBuilder::generateNode` was
> > > never called and could never erase it. With this patch, that path is
> > > dropped: no `Dst.insert(Pred)` runs.
> >
> >
> > I'm not sure, but AFAIK `StateTrue` and `StateFalse` could be null at the
> > same time, so this sounds plausible to me.
>
> Actually, `StateTrue` and `StateFalse` cannot be both null at the same time,
> because this the corner case when `ConstraintManager::assumeDualImpl`
> introduces PosteriorlyOverconstrained states instead of returning `{nullptr,
> nullptr}`. Therefore my conversion happens to be NFC.
>
> (By the way, this was a helpful review comment, because I didn't think about
> this corner case. Without the PosteriorlyOverconstrained hack the old code
> would be logically incorrect – in that one very rare case – and the new would
> be the logically correct transition.)
This is what I figured, and wanted to surface this.
https://github.com/llvm/llvm-project/pull/204371
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
