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

回答