Fixpoint not reached with Octagons and assume_overflow = None

[michael-schwarz]

For #1417, I came across an issue in dump1090 where the fixpoint is not reached.
With creduce, I reduced it to the following example:

// SKIP PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none
#include<pthread.h>

int main() {
  int d = 1;
  while (d < 6) {
    if (0)
      return 0;
    d++;
  }

  return 0;
}

[Error] Fixpoint not reached at L:node 16 "0" on tests/regression/46-apron2/84-fix.c:7:9-7:10
 Solver computed:
 HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
                                                                                                                 mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
                                                                                                                 base:({
                                                                                                                         Local {
                                                                                                                           d ->   (Not {0}([-31,31]))
                                                                                                                         }
                                                                                                                       }, {}, {}, {}),
                                                                                                                 threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
                                                                                                                 threadflag:Singlethreaded,
                                                                                                                 threadreturn:True,
                                                                                                                 escape:{},
                                                                                                                 mutexEvents:(),
                                                                                                                 access:(),
                                                                                                                 mutex:(lockset:{}, multiplicity:{}),
                                                                                                                 race:(),
                                                                                                                 mhp:(),
                                                                                                                 assert:(),
                                                                                                                 apron:([|d#987-1.>=0; -d#987+5.>=0|] (env: [|0> d#987:int|]), ())], map:{})}
 Right-Hand-Side:
 HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
                                                                                                                 mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
                                                                                                                 base:({
                                                                                                                         Local {
                                                                                                                           d ->   ⊤
                                                                                                                         }
                                                                                                                       }, {}, {}, {}),
                                                                                                                 threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
                                                                                                                 threadflag:Singlethreaded,
                                                                                                                 threadreturn:True,
                                                                                                                 escape:{},
                                                                                                                 mutexEvents:(),
                                                                                                                 access:(),
                                                                                                                 mutex:(lockset:{}, multiplicity:{}),
                                                                                                                 race:(),
                                                                                                                 mhp:(),
                                                                                                                 assert:(),
                                                                                                                 apron:([|d#987-1.>=0; -d#987+5.>=0|] (env: [|0> d#987:int|]), ())], map:{})}
 Difference: Map: [mutex:(lockset:{}, multiplicity:{}),
                   apron:()] = [base:Map: d = (Unknown int([-31,31])) instead of (Not {0}([-31,31]))]

[michael-schwarz]

For some reason, this happens on #1417 only.

[michael-schwarz]

The issue was present on d8be117 on master, so it must have been fixed between then and now on master.

[michael-schwarz]

The bisect points at 24760f5, which was part of https://github.com/goblint/analyzer/pull/1413/files.

[michael-schwarz]

Fixed by #1413