Fatal error: exception Failure("Node.move_opt: ambiguous moved index") for creating witnesses with path-sensitive analyses

[michael-schwarz]

On top of #1234 with path-sensitive MemLeak analysis, the generation of witnesses fails with an error message

Fatal error: exception Failure("Node.move_opt: ambiguous moved index")

The reduced program (with a manual config e.g. without autotuning and loop unrolling (so unrelated to #1225)) is the following:

//PARAM: --enable witness.graphml.enabled --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --sets ana.specification /home/michael/Documents/sv-comp/sv-benchmarks/c/properties/valid-memsafety.prp  --sets ana.activated[+] "memLeak" --set ana.malloc.unique_address_count 1
struct _twoIntsStruct {
   int intOne ;
   int intTwo ;
};

typedef struct _twoIntsStruct twoIntsStruct;

void printStructLine(twoIntsStruct const *structTwoIntsStruct)
{
  return;
}


int main(int argc, char **argv)
{
  twoIntsStruct *data;
  int tmp_1;


  if (tmp_1 != 0) {
    twoIntsStruct *dataBuffer = malloc(800UL);
    data = dataBuffer;
  }
  else {

    twoIntsStruct *dataBuffer_0 = malloc(800UL);
    data = dataBuffer_0;
  }

  printStructLine((twoIntsStruct const *)data);
  free((void *)data);

  return;
}

The problem seems to be related to the call of printStructLine, so I started wondering if the issue has to do with path-sensitivity...

We should probably aim to fix this or at least return trivial witnesses in such cases to still get points if fixing is out-of-reach.