0

是z3不允许变量以

    __*

在我在 python 中运行以下代码之后

    __a = BitVec('__a', 3)

程序由于某些错误而终止，但没有给出终止原因

4

1 回答 1

0

我猜你在rise4fun.com使用Z3 。在线工具使用代码“sanitizer”。这个想法是为了防止对rise4fun网站的攻击。例如，它将阻塞import语句和以 . 开头的名称__。消毒剂是保守的，并阻止了几个无害的脚本。如果你在你的机器上执行 Z3，你的脚本就可以工作。我刚刚尝试了以下简单的方法：

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

顺便说一句，以下变体适用于rise4fun（也可在此处获得）：

   _a = BitVec('__a', 3)
   print a
于 2013-05-06T05:45:03.520 回答