z3 variable naming standards -

is z3 doesn't allow variables starting with

    __* 

after run following code in python

    __a = bitvec('__a', 3) 

program terminates due error doesn't give reason of termination

i guess using z3 @ rise4fun.com. online tool uses code "sanitizer". idea prevent attacks rise4fun website. example, block import statements, , names starting __. sanitizer conservative, , blocks several harmless scripts. if execute z3 on machine, script work. tried following simple one:

   z3 import *    __a = bitvec('__a', 3)    print 

btw, following variation works @ rise4fun (also available here):

   _a = bitvec('__a', 3)    print