Array indexing breaks without mem optimization

[jkwoods]

If the mem optimization is turned off, you are unable to update a variable that is later used to name an array index, but ONLY inside a loop/if statement (as far as I can tell). Toy example:

#include <stdio.h>
int main(void) {
  int mat[5] = {1,2,3,4,5};
  int a = -1;
  if( a < 0 ) {
    int i = 0;
    i = 1;
    int c = mat[i];
  }
}

Command: C_no_overflow=True C_smt_opts=cfee,ee,nary,cfee,arrayElim,flattenAnds,cfee,ee,flattenAnds,cfee,ee C_streams=smt::opt stack run -- c main toy.c --emit-r1cs

The error looks like this: Bad alias type Var "alloc_0_v0" (SortArray (SortBv 32) (SortBv 32))

Maybe mem optimization should just never be turned off?

[alex-ozdemir]

Yeah, we probably shouldn't call the mem pass an "optimization"---it's required for the R1CS pipeline, since R1CS cannot handle arrays.

Let's leave this issue open until I make a better error message.