char buf[3];
ostrstream(buf,sizeof(buf)) << i << ends;
a.push_back(symbol(string("a")+buf));
x.push_back(symbol(string("x")+buf));
char buf[3];
ostrstream(buf,sizeof(buf)) << i << ends;
a.push_back(symbol(string("a")+buf));
x.push_back(symbol(string("x")+buf));