log/arrayanderr.btor:2: literal '1' refers to an unexpected array expression