<table border="1" cellspacing="0" cellpadding="8">
    <tr>
        <th>Issue</th>
        <td>
            <a href=https://github.com/llvm/llvm-project/issues/89365>89365</a>
        </td>
    </tr>

    <tr>
        <th>Summary</th>
        <td>
            verify-scev fails with "Trip Count for Loop ... Changed!"
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            new issue
      </td>
    </tr>

    <tr>
      <th>Assignees</th>
      <td>
      </td>
    </tr>

    <tr>
      <th>Reporter</th>
      <td>
          bjope
      </td>
    </tr>
</table>

<pre>
    Given this input
```
define void @foo() {
entry:
  br label %for.outer

for.outer.again:
  %phi3.lcssa = phi i16 [ %phi3, %for.cond3 ]
  br label %for.outer

for.outer:
  %.pre = phi i16 [ 0, %entry ], [ %phi3.lcssa, %for.outer.again ]
  %step.outer = add i16 %.pre, 2
 %cmp0 = icmp ult i16 %step.outer, 17
  br i1 %cmp0, label %for.cond1, label %end

for.cond1:
  %phi1 = phi i16 [ %step.1, %for.body1 ], [ %step.outer, %for.outer ]
  %step.1 = add i16 %phi1, 1
  %cmp1 = icmp ne i16 %step.1, 8
  br i1 %cmp1, label %for.body1, label %for.cond2.preheader

for.body1:
  br label %for.cond1

for.cond2.preheader:
  %phi1.lcssa = phi i16 [ %phi1, %for.cond1 ]
  %cmpnew = icmp uge i16 %phi1.lcssa, 8
  br i1 %cmpnew, label %for.cond2, label %end

for.cond2:
  %phi2 = phi i16 [ %step.2, %for.body2 ], [ %phi1.lcssa, %for.cond2.preheader ]
  %step.2 = add i16 %phi2, -1
  %cmp2 = icmp ugt i16 %phi2, 8
  br i1 %cmp2, label %for.body2, label %for.cond3.preheader

for.body2:
  br label %for.cond2

for.cond3.preheader:
  %step.2.lcssa = phi i16 [ %step.2, %for.cond2 ]
  br label %for.cond3

for.cond3:
  %phi3 = phi i16 [ %step.3, %for.body3 ], [ %step.2.lcssa, %for.cond3.preheader ]
 %step.3 = add i16 %phi3, 1
  %cmp3 = icmp ne i16 %phi3, 20
  br i1 %cmp3, label %for.body3, label %for.outer.again

for.body3:
  br label %for.cond3

end:
  ret void
}

```
when running `opt -passes="print<scalar-evolution>,no-op-loop,print<scalar-evolution>,verify<scalar-evolution>" -o /dev/null` the first print says:
```
Classifying expressions for: @foo
  %phi3.lcssa = phi i16 [ %phi3, %for.cond3 ]
  -->  {{{(1 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2>,+,1}<nw><%for.cond3> U: full-set S: full-set  -->  20 U: [20,21) S: [20,21)                Exits: 20 LoopDispositions: { %for.outer: Variant, %for.cond1: Variant, %for.cond2: Variant, %for.cond3: Computable }
  %.pre = phi i16 [ 0, %entry ], [ %phi3.lcssa, %for.outer.again ]
  -->  %.pre U: full-set S: full-set            Exits: <<Unknown>>              LoopDispositions: { %for.outer: Variant, %for.cond1: Invariant, %for.cond2: Invariant, %for.cond3: Invariant }
  %step.outer = add i16 %.pre, 2
  -->  (2 + %.pre) U: full-set S: full-set              Exits: <<Unknown>> LoopDispositions: { %for.outer: Variant, %for.cond1: Invariant, %for.cond2: Invariant, %for.cond3: Invariant }
  %phi1 = phi i16 [ %step.1, %for.body1 ], [ %step.outer, %for.outer ]
  -->  {(2 + %.pre),+,1}<%for.cond1> U: full-set S: full-set            Exits: 7                LoopDispositions: { %for.cond1: Computable, %for.outer: Variant }
  %step.1 = add i16 %phi1, 1
  -->  {(3 + %.pre),+,1}<%for.cond1> U: full-set S: full-set Exits: 8                LoopDispositions: { %for.cond1: Computable, %for.outer: Variant }
  %phi1.lcssa = phi i16 [ %phi1, %for.cond1 ]
 -->  {(2 + %.pre),+,1}<%for.cond1> U: full-set S: full-set  -->  7 U: [7,8) S: [7,8)          Exits: 7                LoopDispositions: { %for.outer: Variant, %for.cond1: Computable, %for.cond2: Invariant, %for.cond3: Invariant }
  %phi2 = phi i16 [ %step.2, %for.body2 ], [ %phi1.lcssa, %for.cond2.preheader ]
  -->  {{(2 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2> U: full-set S: full-set  --> {7,+,-1}<nw><%for.cond2> U: [7,8) S: [7,8)            Exits: 7 LoopDispositions: { %for.cond2: Computable, %for.outer: Variant }
 %step.2 = add i16 %phi2, -1
  -->  {{(1 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2> U: full-set S: full-set  --> {6,+,-1}<nw><%for.cond2> U: [6,7) S: [6,7)            Exits: 6 LoopDispositions: { %for.cond2: Computable, %for.outer: Variant }
 %step.2.lcssa = phi i16 [ %step.2, %for.cond2 ]
  -->  {{(1 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2> U: full-set S: full-set  -->  6 U: [6,7) S: [6,7)           Exits: 6                LoopDispositions: { %for.outer: Variant, %for.cond1: Variant, %for.cond2: Computable, %for.cond3: Invariant }
  %phi3 = phi i16 [ %step.3, %for.body3 ], [ %step.2.lcssa, %for.cond3.preheader ]
  -->  {{{(1 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2>,+,1}<nw><%for.cond3> U: full-set S: full-set  -->  {6,+,1}<nw><%for.cond3> U: [6,21) S: [6,21) Exits: 20               LoopDispositions: { %for.cond3: Computable, %for.outer: Variant }
  %step.3 = add i16 %phi3, 1
  -->  {{{(2 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2>,+,1}<nw><%for.cond3> U: full-set S: full-set  -->  {7,+,1}<nw><%for.cond3> U: [7,22) S: [7,22) Exits: 21               LoopDispositions: { %for.cond3: Computable, %for.outer: Variant }
Determining loop execution counts for: @foo
Loop %for.cond1: backedge-taken count is (5 + (-1 * %.pre))
Loop %for.cond1: constant max backedge-taken count is i16 -1
Loop %for.cond1: symbolic max backedge-taken count is (5 + (-1 * %.pre))
Loop %for.cond1: Trip multiple is 1
Loop %for.cond2: backedge-taken count is i16 0
Loop %for.cond2: constant max backedge-taken count is i16 0
Loop %for.cond2: symbolic max backedge-taken count is i16 0
Loop %for.cond2: Trip multiple is 1
Loop %for.cond3: backedge-taken count is i16 14
Loop %for.cond3: constant max backedge-taken count is i16 14
Loop %for.cond3: symbolic max backedge-taken count is i16 14
Loop %for.cond3: Trip multiple is 15
Loop %for.outer: <multiple exits> Unpredictable backedge-taken count.
  exit count for for.outer: ***COULDNOTCOMPUTE***
  exit count for for.cond2.preheader: i1 false
Loop %for.outer: constant max backedge-taken count is i1 false
Loop %for.outer: symbolic max backedge-taken count is i1 false
  symbolic max exit count for for.outer: ***COULDNOTCOMPUTE***
  symbolic max exit count for for.cond2.preheader: i1 false

```
and then the second one says:
```
Classifying expressions for: @foo
  %phi3.lcssa = phi i16 [ %phi3, %for.cond3 ]
 -->  {{{(1 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2>,+,1}<nw><%for.cond3> U: full-set S: full-set  -->  19 U: [19,20) S: [19,20)                Exits: 19 LoopDispositions: { %for.outer: Variant, %for.cond1: Variant, %for.cond2: Variant, %for.cond3: Computable }
  %.pre = phi i16 [ 0, %entry ], [ %phi3.lcssa, %for.outer.again ]
  -->  %.pre U: full-set S: full-set            Exits: <<Unknown>>              LoopDispositions: { %for.outer: Variant, %for.cond1: Invariant, %for.cond2: Invariant, %for.cond3: Invariant }
  %step.outer = add i16 %.pre, 2
  -->  (2 + %.pre) U: full-set S: full-set              Exits: <<Unknown>> LoopDispositions: { %for.outer: Variant, %for.cond1: Invariant, %for.cond2: Invariant, %for.cond3: Invariant }
  %phi1 = phi i16 [ %step.1, %for.body1 ], [ %step.outer, %for.cond1.preheader ]
  -->  {(2 + %.pre),+,1}<%for.cond1> U: full-set S: full-set            Exits: 7 LoopDispositions: { %for.cond1: Computable, %for.outer: Variant }
 %step.1 = add i16 %phi1, 1
  -->  {(3 + %.pre),+,1}<%for.cond1> U: full-set S: full-set            Exits: 8                LoopDispositions: { %for.cond1: Computable, %for.outer: Variant }
  %phi1.lcssa = phi i16 [ %phi1, %for.cond1 ]
  -->  {(2 + %.pre),+,1}<%for.cond1> U: full-set S: full-set  -->  7 U: [7,8) S: [7,8)          Exits: 7 LoopDispositions: { %for.outer: Variant, %for.cond1: Computable, %for.cond2: Invariant, %for.cond3: Invariant }
  %phi2 = phi i16 [ %step.2, %for.body2 ], [ %phi1.lcssa, %for.cond2.preheader1 ]
  -->  {{(2 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2> U: full-set S: full-set  --> {7,+,-1}<nw><%for.cond2> U: [7,8) S: [7,8)            Exits: 7 LoopDispositions: { %for.cond2: Computable, %for.outer: Variant }
 %step.2 = add i16 %phi2, -1
  -->  {{(1 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2> U: full-set S: full-set  --> {6,+,-1}<nw><%for.cond2> U: [6,7) S: [6,7)            Exits: 6 LoopDispositions: { %for.cond2: Computable, %for.outer: Variant }
 %step.2.lcssa = phi i16 [ %step.2, %for.cond2 ]
  -->  {{(1 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2> U: full-set S: full-set  -->  6 U: [6,7) S: [6,7)           Exits: 6                LoopDispositions: { %for.outer: Variant, %for.cond1: Variant, %for.cond2: Computable, %for.cond3: Invariant }
  %phi3 = phi i16 [ %step.3, %for.body3 ], [ %step.2.lcssa, %for.cond3.preheader ]
  -->  {{{(1 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2>,+,1}<nw><%for.cond3> U: full-set S: full-set  -->  {6,+,1}<nw><%for.cond3> U: [6,20) S: [6,20) Exits: 19               LoopDispositions: { %for.cond3: Computable, %for.outer: Variant }
  %step.3 = add i16 %phi3, 1
  -->  {{{(2 + %.pre),+,1}<%for.cond1>,+,-1}<nw><%for.cond2>,+,1}<nw><%for.cond3> U: full-set S: full-set  -->  {7,+,1}<nw><%for.cond3> U: [7,21) S: [7,21) Exits: 20               LoopDispositions: { %for.cond3: Computable, %for.outer: Variant }
Determining loop execution counts for: @foo
Loop %for.cond1: backedge-taken count is (5 + (-1 * %.pre))
Loop %for.cond1: constant max backedge-taken count is i16 -1
Loop %for.cond1: symbolic max backedge-taken count is (5 + (-1 * %.pre))
Loop %for.cond1: Trip multiple is 1
Loop %for.cond2: backedge-taken count is i16 0
Loop %for.cond2: constant max backedge-taken count is i16 0
Loop %for.cond2: symbolic max backedge-taken count is i16 0
Loop %for.cond2: Trip multiple is 1
Loop %for.cond3: backedge-taken count is i16 13
Loop %for.cond3: constant max backedge-taken count is i16 13
Loop %for.cond3: symbolic max backedge-taken count is i16 13
Loop %for.cond3: Trip multiple is 14
Loop %for.outer: <multiple exits> Unpredictable backedge-taken count.
  exit count for for.outer: ***COULDNOTCOMPUTE***
  exit count for for.cond2.preheader: i1 false
Loop %for.outer: constant max backedge-taken count is i1 false
Loop %for.outer: symbolic max backedge-taken count is i1 false
  symbolic max exit count for for.outer: ***COULDNOTCOMPUTE***
  symbolic max exit count for for.cond2.preheader: i1 false

```
So we can for example see that Exsits has changed for `%phi3` and  `%step.3`, and the max backedge-taken counts for %for.cond3 goes from 14 to 13.

Then the verification complains:
```
Trip Count for Loop at depth 2 containing: %for.cond3<header><exiting>,%for.body3<latch>
 Changed!
Old: 13
New: 14
Delta: -1
```

Some things that I've noticed:
1) no-op-loop will result in running LoopSimplify, which will add a pre-header for the for.cond1 loop. This should not really change anything from the perspective of SCEV, but I figure we do forget some SCEV values/dispositions in the process.

2) If modifying LoopSimplify like this
```
@@ -881,6 +929,17 @@ PreservedAnalyses LoopSimplifyPass::run(Function &F,
     MSSAU = std::make_unique<MemorySSAUpdater>(MSSA);
   }
 
+ SE->print(dbgs());
+  SE->forgetAllLoops();
+  SE->print(dbgs());
+ SE->verify();
 
   // Note that we don't preserve LCSSA in the new PM, if you need it run LCSSA
   // after simplifying the loops. MemorySSA is preserved if it exists.
  for (auto *L : *LI)
    Changed |=
 simplifyLoop(L, DT, LI, SE, AC, MSSAU.get(), /*PreserveLCSSA*/ false);
```
we can see that doing forgetAllLoops() and then re-calculating SCEV gives the same behavior. So this is not really related to LoopSimplify or the pass manager. But it seems a bit weird that the SCEV result changes after doing forgetAllLoops!?!?

3) When doing the second `print<scalar-evolution>` the function ScalarEvolution::howManyGreaterThans is involved. But it isn't involved the first time.

4) ( @fhahn : Bi-secting pointed at this starting to happen after commit 7019624ee124 "[SCEV] Strengthen nowrap flags via ranges for ARs on construction.". But maybe that is a co-incidence. )
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJzsW1tv2zoS_jXMy8CGRPn6kIdESQ4KpBes07OPC1oaWzyVSK1IOfW_Xwwl27IsX7JNc1qcFIELk8Mh55urRqYwRi4V4jUb3rLh3ZUobaKL6_lfOseruY7X13_IFSqwiTQgVV5a5t0x74aNvPrPfY1xIRXCSssY2MBbaM34hPEpsPFtRYHKFmsW3FTfAOYFpGKOKTA-XOiir0uLRc3bfW4H-2IppGosZXyYJzLop5ExAlhwB3kiQfojYMPbzSzj4YZ1pFUcABvevXzv_V37eYEH-3n1Tk5Atwt93x2kOmbjOA2hmodifGgs5tW020XEcbVLtTOx4DU148Moyz1HJqMshzK1G9odF1rhjxtSS3-zkqb2MCCQ_L1RVHEbk4qorQm_SwfuFH5DbDImv4XP_lGb-HQh47dRob2djA3KKMv9HSwK91Bx1JMuQPwDQNx5O2HipI0ERXxoNNWi41ZeAdiBapPnAb4nLd1vWbrfgi7KcoXPDUtZYhO_nXl24qLwuRuDS0yFH4jCj5oKb5kKP3Ql_8CVWsh1GQ3vMBq3V69lNbwJkW1Td4LDO43mcNQFoNNGw88YDe_CNzhmNJXkx83mAHG3xakQ6bbrPMNhYD66Y9DScdAVDninloNOLW8Zdyg56IgMQVdk2NByr0vHQaeOD0ebqapDv8EZ_e5hS-60Iy_QusRaU4zvmqStPPycoIKiVEqqJbCRp3MLvVwYg4YFd4zzvJDKsiA0kUhF0cOVTksrtWLBPeOh0j2d91Ktc8bD06QrLORifWyaQ08D4w8xrhh_UGWaspEHNkFYyMJYcLzBiLXZCtqSJEypNFmsSRD8nhdojNTKwEKTrW-KjNeqCHo9FtyDq1aqPz4hA7jd5d4p4yHjt4yHPqkgCPciuoOkmu7V8-qZRvfoeJPuOFlAZ_lKUi7KNO0ZtDDb-7Y5LvcqMja85ZTRuU8l1-xwqPXv_ru0BDwxeNQ6v5Mm10aS9twwG9_ul0bBDfwpCimUbSeb41P8-BQ5A4Q6y0sr5inC1qZ_fpW1UXS9zUmUOwAjRQXhV_VN6Wdn6cSs-e8V4PygVscBPTYZ7E22EL28rtzhM-Et-78UqzNo_ZIAvUER24gwh9ieiS0vNtNx2-PPoL6FdueUbVkaOumyrvO1-R4AwSsCsJV68pZS_1Bd_vOMoeY83iaGMePhpJkWtgM_bjaXOGsntj_srW_3HLFfGbxYW5eWBZdolY2d8l7A7zL971nABT7D_x-fecHzWBvyn1SJXQj56MWQ04pxE_LtQBfko58P-Y88CP5CyoDRiyBuIPz6Ye1EzXs04p0Lam_44PybPvDsueMl_GrL2H8w2o00H4ReXDoEP1QwnW9ZdKjoJyWfV1bR-KUqogWct5NUNbJTkf82KrpDi0UmXQcl1ToH_I6R62xApEtlO1sQdJaDGDEX0TeMl9iz4hvWq0Eaerga1oqc9MjrbvZUOj3BMtLKWDpuJr4f5U8GtcmmnVzMOpvrVEYnufzAKZ8KmUNWplbmKRKvI4fhp1AiKbwT6y6G4hSTi5A4x-RScYNz4vqDEwsvlvckl4sFPsnlUOLhIfXWxVgQbmmxcud7-KryAmMZVR2grpP0N4GQ1tSHW-gC9nnzm-ov_Pz18e7T56fw88cvX5_ut-MnmBy-dwHpw0KkBk9Ic6EezvK5UBNNPrC_6FVwOcfxLEid3VuhYrCJe2-MYJCYgFb463R8f8_6x59uc6ZP5-NeM2k2hlr_tknUn743fN8bvu8N39dv-LrDnn3WeovW78_qev4Crd4ugX-fru-v2_b9h_Z5jynnvdH73uh9b_S-N3rfG72_XaPXO2j0entdRL_9bPTe6H3rRq9_0Oj9e3rx743e90bv39XoDV6l0XuKy-WN3lNcDiXuaAu_N3r_uY3emYZnhEgoxwe_i4yUbxDBJsLC_XcjrYFEGIgSoZYYOzpaXifCkQdCxVAP1UXQyHX_6ibyUdxMxavZ4F1qNLAodAb-AKwGP-g3D_-0aUm7Xy_LSNTRPstTIdXRzrTzgnCLltOysBBjbhPgZChWuDxSKaTpQuEGTUqLhLqjqhLxrspjQZgKGyU0U6krrNBivA4xn9PYlS-1s37CZ_d1sEllqRU0sMkGLQE2uspILVItTaWdD4yPVwhKWxnh7ifnLh3vfgoOzzJNoUDj7hjtfl5OMMxklqdysSZ1PScySipiqnYE5AX26oKUYHO__t62RYhzH54SacAkukxjOgYUKNJ0XdsKCLV2x600SutzLEyOkZUrBL2AWXj_J209Ly18gIVclgWSPcaadlqiBUMyExmsRFqiYfwhbpQSJI_jW-gIjdkzFvf6-cMCMh3XbyWaEkMqvzk0TTfiA48NPOhNJj7jIdV9t1NXxvljqOe-FGiwWGF8o0S6Nmj2-H8RxtljcFOUivHJQ6kiZ62Mjx7IfGq3BoCPs9nNV1dlGhtXazLxDf9TKvnfElkQfsRMF2uiymNhK2vkE1pG6T243fJqPFJWUvBbmN1TvVddBuCTeL401dW-5lKiqwkr3G_SlITZkHbQnWdY0dX3DPb5wO7E_IHxB_ikbR1xnPYV42NL9ucAhsdwNrvZqFrhM3z5SFYjF7DWJSjEGKQlu64o28zFwmIBplYMGQLxIQM2fdhiS1F8s2NMvKWlMGus2ea3KlxNRGk1xe1HqAP444dtmUX6rH0f2DhkwUYhm-0f3eWMySMJcPdEn7Q6hBnFFLgJ6dMZRH-JdgNsWIlyszG5SkxKDw91hG9i37pSUoX3bUiPtfPIDjXD9q1fgb1IpFGZCop3lf8t5QpN9T5QZAhzTMRK6qIPM13fLjXNEFBgKizGFMT33K4OJLkwBjKhxBKLPtyWluA2iJkBAXNJdiCLuDox0bsj1DGsii6m1mu3PD4LHurPRkgISMp_k4TVqsbbTTbyTl2Y2dx-2XjxzNHc70jIaxP9_FGo9R8Fkpc-JUI5VKRa6XSF8VZOaSoD30w0LtZYmeFeFBu4W7h84p5iEpEoZ3S3smcojKol5FoqAtoBRdHYisJNWA2JyHNUNVCRzjJpYez50xEfIPp8AIxzNrx1YXh4BzNboFo6C1D6uRA5LFKxNLCSAooKc3KBm38ZcGlXGVuUDo8-47wSLxPreW1pknQZ6Z5UkYxRRdgHxqdX8XUQT4OpuMJrf-wHQ-4PfP8quUY_Rs6nw2AY4HgivPlwyL0Jn0ZTPgpGw8mVvOYeH3gDf-p7vuf7fTEPRvP5cBQEuBhhELGBh5mQaT9NV1lfF8sraUyJ15NpMBpeuTtbxl2U5pyiiJt0CNxdFde0pjcvl4YNvNS5_ZaLlTbF6yqS9UyEK1gImRp4ljYhCLvqi36_3ywCOL8qi_Q6sTZ3acFFpqW0STnvRzpj_IF2q__r5YX-CyPL-IM7I2U9J8P_AgAA__9Oy6n4">