<div dir="ltr">Why cannot prove analyzer that only the true case is feasible for the following example?<br>```<br><span style="font-family:monospace">ProgramStateRef StInBound  = state->assumeInBound(Idx, Size, true);<br>ProgramStateRef StOutBound = state->assumeInBound(Idx, Size, false);</span><br>```<br><br>Given that we know:<br>SVals:<br><span style="font-family:monospace">  Idx.dump():  (conj_$8{int, LC1, S2294, #1}) - 1U<br>  Size.dump(): extent_$5{SymRegion{reg_$4<</span><span style="font-family:monospace">char * dst>}}</span><br><br>Range constraints according to the exploded graph nodes:<br><span style="font-family:monospace">  extent_$5{SymRegion{reg_$4<</span><span style="font-family:monospace">char * dst>}}  {[10,18446...]}<br>  conj_$8{int, LC1, S2294, #1}              {[1,9]}</span><br><br>Does the `<span style="font-family:monospace">Idx < Size</span>` hold for all possible values of <span style="font-family:monospace">`Idx`</span> and `<span style="font-family:monospace">Size</span>`?<br>IMO yes, since <span style="font-family:monospace">[0-8] < [10,18446...]</span>, but the analyzer returns <u>non-null</u> states for both of the <span style="font-family:monospace">`assumeInBound</span>` calls, but why?<br><br>Balazs</div>