Z3变量的命名标准

难道Z3不允许变量开始Z3变量的命名标准

__*

后，我跑在python下面的代码

__a = BitVec('__a', 3)

程序终止，由于一些错误，但不给出终止的原因

2013-05-06 Sharad

我想你在使用Z3在rise4fun.com。在线工具使用代码“清洁剂”。这个想法是为了防止袭击4fun网站。例如，它将阻止import语句，并且名称以__开头。消毒剂是保守的，并阻止几个无害的脚本。如果你在你的机器上执行Z3，你的脚本将会工作。我只是尝试了以下简单：

from z3 import * 
    __a = BitVec('__a', 3) 
    print a

BTW，以下变化工作在rise4fun（也可here）：

_a = BitVec('__a', 3) 
    print a

2013-05-06 05:45:03

回答