Fixpoint not reached for 14 new tasks

[michael-schwarz]

#1733 causes 14 new instances where the fixpoint is not reached

One instances boils down to

Solver computed:
 HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
                                                                                                                 base:({
                                                                                                                         Local {
                                                                                                                           A ->   (Unknown int([-31,31]),[-2147483645,2147483645],not {} ([-31,31]),1+2ℤ)
                                                                                                                           R ->   (Unknown int([-31,31]),[-2147483647,2147483646],not {} ([-31,31]),ℤ)
                                                                                                                           u ->   (Unknown int([-63,63]),[-4294967285,9223372036854775807],not {} ([-63,63]),1+2ℤ)
                                                                                                                           v ->   (Not {0}([-63,63]),[1,4611686016279905794],not {0} ([0,63]),1+2ℤ)
                                                                                                                           r ->   (Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]),ℤ)
                                                                                                                         }
                                                                                                                         Temp {
                                                                                                                           tmp ->   1
                                                                                                                           tmp___0 ->   1
                                                                                                                         }
                                                                                                                       }, {}, {}, {}),
                                                                                                                 threadflag:Singlethreaded,
                                                                                                                 mutexEvents:(),
                                                                                                                 access:(),
                                                                                                                 mutex:(lockset:{}, multiplicity:{}),
                                                                                                                 escape:{},
                                                                                                                 expRelation:(),
                                                                                                                 assert:(),
                                                                                                                 var_eq:{},
                                                                                                                 abortUnless:false,
                                                                                                                 apron:([|A#322+2147483647.>=0; -A#322+2147483646.>=0; -A#322+R#323+4294967293.>=0; A#322+R#323+4294967294.>=0; R#323+2147483647.>=0; -A#322-R#323+4294967292.>=0; A#322-R#323+4294967293.>=0; -R#323+2147483646.>=0; -A#322+r#326+9.22337203901e+18>=0; A#322+r#326+9.22337203901e+18>=0; -R#323+r#326+9.22337203901e+18>=0; R#323+r#326+9.22337203901e+18>=0; r#326+9.22337203686e+18>=0; -A#322-r#326+9.22337203901e+18>=0; A#322-r#326+9.22337203901e+18>=0; -R#323-r#326+9.22337203901e+18>=0; R#323-r#326+9.22337203901e+18>=0; -r#326+9.22337203686e+18>=0; -A#322+tmp#327+2147483645.>=0; A#322+tmp#327+2147483646.>=0; -R#323+tmp#327+2147483645.>=0; R#323+tmp#327+2147483646.>=0; -r#326+tmp#327+9.22337203686e+18>=0; r#326+tmp#327+9.22337203686e+18>=0; tmp#327-1.>=0; -A#322-tmp#327+2147483647.>=0; A#322-tmp#327+2147483648.>=0; -R#323-tmp#327+2147483647.>=0; R#323-tmp#327+2147483648.>=0; -r#326-tmp#327+9.22337203686e+18>=0; r#326-tmp#327+9.22337203686e+18>=0; -tmp#327+1.>=0; -A#322+tmp___0#329+2147483645.>=0; A#322+tmp___0#329+2147483646.>=0; -R#323+tmp___0#329+2147483645.>=0; R#323+tmp___0#329+2147483646.>=0; -r#326+tmp___0#329+9.22337203686e+18>=0; r#326+tmp___0#329+9.22337203686e+18>=0; -tmp#327+tmp___0#329>=0; tmp#327+tmp___0#329-2.>=0; tmp___0#329-1.>=0; -A#322-tmp___0#329+2147483647.>=0; A#322-tmp___0#329+2147483648.>=0; -R#323-tmp___0#329+2147483647.>=0; R#323-tmp___0#329+2147483648.>=0; -r#326-tmp___0#329+9.22337203686e+18>=0; r#326-tmp___0#329+9.22337203686e+18>=0; -tmp#327-tmp___0#329+2.>=0; tmp#327-tmp___0#329>=0; -tmp___0#329+1.>=0; -A#322+u#324+6442450931.>=0; A#322+u#324+6442450932.>=0; -R#323+u#324+2147483638.>=0; R#323+u#324+6442450932.>=0; -r#326+u#324-3.>=0; r#326+u#324+9.22337204115e+18>=0; -tmp#327+u#324+4294967286.>=0; tmp#327+u#324+4294967284.>=0; -tmp___0#329+u#324+4294967286.>=0; tmp___0#329+u#324+4294967284.>=0; u#324+4294967285.>=0; -A#322-u#324+9.22337203901e+18>=0; A#322-u#324+9.22337203901e+18>=0; -R#323-u#324+9.22337203901e+18>=0; R#323-u#324+9.22337203901e+18>=0; -r#326-u#324+1.84467440738e+19>=0; r#326-u#324+1.84467440738e+19>=0; -tmp#327-u#324+9.22337203686e+18>=0; tmp#327-u#324+9.22337203686e+18>=0; -tmp___0#329-u#324+9.22337203686e+18>=0; tmp___0#329-u#324+9.22337203686e+18>=0; -u#324+9.22337203686e+18>=0; -A#322+v#325+2147483645.>=0; A#322+v#325+2147483646.>=0; -R#323+v#325+2147483645.>=0; R#323+v#325+2147483646.>=0; -r#326+v#325+9.22337203686e+18>=0; r#326+v#325+9.22337203686e+18>=0; -tmp#327+v#325>=0; tmp#327+v#325-2.>=0; -tmp___0#329+v#325>=0; tmp___0#329+v#325-2.>=0; -u#324+v#325+9.22337203686e+18>=0; u#324+v#325+4294967284.>=0; v#325-1.>=0; -A#322-v#325+7.90574746109e+18>=0; A#322-v#325+7.90574746109e+18>=0; -R#323-v#325+7.90574746109e+18>=0; R#323-v#325+7.90574746109e+18>=0; -r#326-v#325+1.71291194958e+19>=0; r#326-v#325+1.71291194958e+19>=0; -tmp#327-v#325+7.90574745894e+18>=0; tmp#327-v#325+7.90574745894e+18>=0; -tmp___0#329-v#325+7.90574745894e+18>=0; tmp___0#329-v#325+7.90574745894e+18>=0; -u#324-v#325+1.71291194958e+19>=0; u#324-v#325+7.90574746323e+18>=0; -v#325+7.90574745894e+18>=0|] (env: [|0> A#322:int; 1> R#323:int; 2> r#326:int; 3> tmp#327:int; 4> tmp___0#329:int; 5> u#324:int; 6> v#325:int|]), ())], map:{})}
 Right-Hand-Side:
 HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
                                                                                                                 base:({
                                                                                                                         Local {
                                                                                                                           A ->   (Unknown int([-31,31]),[-2147483645,2147483645],not {} ([-31,31]),1+2ℤ)
                                                                                                                           R ->   (Unknown int([-31,31]),[-2147483647,2147483646],not {} ([-31,31]),ℤ)
                                                                                                                           u ->   (Unknown int([-63,63]),[-4294967285,9223372036854775807],not {} ([-63,63]),1+2ℤ)
                                                                                                                           v ->   (Not {0}([-63,63]),[1,4611686016279905794],not {0} ([0,63]),1+2ℤ)
                                                                                                                           r ->   (Unknown int([-63,63]),[-9223372036854775808,9223372036854775806],not {} ([-63,63]),ℤ)
                                                                                                                         }
                                                                                                                         Temp {
                                                                                                                           tmp ->   1
                                                                                                                           tmp___0 ->   1
                                                                                                                         }
                                                                                                                       }, {}, {}, {}),
                                                                                                                 threadflag:Singlethreaded,
                                                                                                                 mutexEvents:(),
                                                                                                                 access:(),
                                                                                                                 mutex:(lockset:{}, multiplicity:{}),
                                                                                                                 escape:{},
                                                                                                                 expRelation:(),
                                                                                                                 assert:(),
                                                                                                                 var_eq:{},
                                                                                                                 abortUnless:false,
                                                                                                                 apron:([|A#322+2147483647.>=0; -A#322+2147483646.>=0; -A#322+R#323+4294967293.>=0; A#322+R#323+4294967294.>=0; R#323+2147483647.>=0; -A#322-R#323+4294967292.>=0; A#322-R#323+4294967293.>=0; -R#323+2147483646.>=0; -A#322+r#326+9.22337203901e+18>=0; A#322+r#326+9.22337203901e+18>=0; -R#323+r#326+9.22337203901e+18>=0; R#323+r#326+9.22337203901e+18>=0; r#326+9.22337203686e+18>=0; -A#322-r#326+9.22337203901e+18>=0; A#322-r#326+9.22337203901e+18>=0; -R#323-r#326+9.22337203901e+18>=0; R#323-r#326+9.22337203901e+18>=0; -r#326+9.22337203686e+18>=0; -A#322+tmp#327+2147483645.>=0; A#322+tmp#327+2147483646.>=0; -R#323+tmp#327+2147483645.>=0; R#323+tmp#327+2147483646.>=0; -r#326+tmp#327+9.22337203686e+18>=0; r#326+tmp#327+9.22337203686e+18>=0; tmp#327-1.>=0; -A#322-tmp#327+2147483647.>=0; A#322-tmp#327+2147483648.>=0; -R#323-tmp#327+2147483647.>=0; R#323-tmp#327+2147483648.>=0; -r#326-tmp#327+9.22337203686e+18>=0; r#326-tmp#327+9.22337203686e+18>=0; -tmp#327+1.>=0; -A#322+tmp___0#329+2147483645.>=0; A#322+tmp___0#329+2147483646.>=0; -R#323+tmp___0#329+2147483645.>=0; R#323+tmp___0#329+2147483646.>=0; -r#326+tmp___0#329+9.22337203686e+18>=0; r#326+tmp___0#329+9.22337203686e+18>=0; -tmp#327+tmp___0#329>=0; tmp#327+tmp___0#329-2.>=0; tmp___0#329-1.>=0; -A#322-tmp___0#329+2147483647.>=0; A#322-tmp___0#329+2147483648.>=0; -R#323-tmp___0#329+2147483647.>=0; R#323-tmp___0#329+2147483648.>=0; -r#326-tmp___0#329+9.22337203686e+18>=0; r#326-tmp___0#329+9.22337203686e+18>=0; -tmp#327-tmp___0#329+2.>=0; tmp#327-tmp___0#329>=0; -tmp___0#329+1.>=0; -A#322+u#324+6442450931.>=0; A#322+u#324+6442450932.>=0; -R#323+u#324+2147483638.>=0; R#323+u#324+6442450932.>=0; -r#326+u#324-2.>=0; r#326+u#324+9.22337204115e+18>=0; -tmp#327+u#324+4294967286.>=0; tmp#327+u#324+4294967284.>=0; -tmp___0#329+u#324+4294967286.>=0; tmp___0#329+u#324+4294967284.>=0; u#324+4294967285.>=0; -A#322-u#324+9.22337203901e+18>=0; A#322-u#324+9.22337203901e+18>=0; -R#323-u#324+9.22337203901e+18>=0; R#323-u#324+9.22337203901e+18>=0; -r#326-u#324+1.84467440738e+19>=0; r#326-u#324+9.22337203686e+18>=0; -tmp#327-u#324+9.22337203686e+18>=0; tmp#327-u#324+9.22337203686e+18>=0; -tmp___0#329-u#324+9.22337203686e+18>=0; tmp___0#329-u#324+9.22337203686e+18>=0; -u#324+9.22337203686e+18>=0; -A#322+v#325+2147483645.>=0; A#322+v#325+2147483646.>=0; -R#323+v#325+2147483645.>=0; R#323+v#325+2147483646.>=0; -r#326+v#325+9.22337203686e+18>=0; r#326+v#325+9.22337203686e+18>=0; -tmp#327+v#325>=0; tmp#327+v#325-2.>=0; -tmp___0#329+v#325>=0; tmp___0#329+v#325-2.>=0; -u#324+v#325+9.22337203686e+18>=0; u#324+v#325+4294967284.>=0; v#325-1.>=0; -A#322-v#325+7.90574746109e+18>=0; A#322-v#325+7.90574746109e+18>=0; -R#323-v#325+7.90574746109e+18>=0; R#323-v#325+7.90574746109e+18>=0; -r#326-v#325+1.71291194958e+19>=0; r#326-v#325+1.71291194958e+19>=0; -tmp#327-v#325+7.90574745894e+18>=0; tmp#327-v#325+7.90574745894e+18>=0; -tmp___0#329-v#325+7.90574745894e+18>=0; tmp___0#329-v#325+7.90574745894e+18>=0; -u#324-v#325+1.71291194958e+19>=0; u#324-v#325+7.90574746323e+18>=0; -v#325+7.90574745894e+18>=0|] (env: [|0> A#322:int; 1> R#323:int; 2> r#326:int; 3> tmp#327:int; 4> tmp___0#329:int; 5> u#324:int; 6> v#325:int|]), ())], map:{})}
 Difference: Map: [threadflag:Singlethreaded,
                   mutex:(lockset:{}, multiplicity:{}),
                   apron:()] = [apron:-r#326+u#324-3.>=0, r#326-u#324+1.84467440738e+19>=0]

where we also get the following warnings:

[Warning][Analyzer] Invariant Apron: coefficient is not int: 9.22337203901e+18
[Warning][Analyzer] Invariant Apron: coefficient is not int: 9.22337203686e+18
[Warning][Analyzer] Invariant Apron: coefficient is not int: 9.22337204115e+18
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.84467440738e+19
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.71291194958e+19
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.58114949179e+19
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.58114949308e+19
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.58114949265e+19
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.58114949222e+19

[michael-schwarz]

This is a small counter example:

//SKIP PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none
// FXIPOINT

void assume_abort_if_not(int cond) {
  if(!cond) {abort();}
}

int main(void)
{
  int R;
  long long v = 1LL;
  long long r;

  assume_abort_if_not(R>=0 && R<=1);
  assume_abort_if_not(((long long )R - 1LL) * -1 < 1);
  // R is 1 in the concrete

  r = (long long )R * (long long )R - 1; // r = 0


  if (r == 0LL) {
    return 0;
  }

  // In the concrete, none of the stuff after this is reachable

  if (r <= 0LL) {
    return 0;
  }

  r -= v;

  v += 2LL;

  while (r > 0LL) {
    r -= v;
    v += 2LL;
  }

  return 0;
}