2013-05-06 50 views
0

難道Z3不允許變量開始Z3變量的命名標準

__* 

後,我跑在python下面的代碼

__a = BitVec('__a', 3) 

程序終止,由於一些錯誤,但不給出終止的原因

回答

0

我想你在使用Z3在rise4fun.com。在線工具使用代碼「清潔劑」。這個想法是爲了防止襲擊4fun網站。例如,它將阻止import語句,並且名稱以__開頭。消毒劑是保守的,並阻止幾個無害的腳本。 如果你在你的機器上執行Z3,你的腳本將會工作。我只是嘗試了以下簡單:

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

BTW,以下變化工作在rise4fun(也可here):

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