z3 变量命名标准

【问题标题】：z3 variable naming standardsz3 变量命名标准
【发布时间】：2013-05-06 03:16:13
【问题描述】：

是不是z3不允许变量以

开头

__*

我在 python 中运行以下代码后

    __a = BitVec('__a', 3)

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

【问题讨论】：

标签： variables naming-conventions z3

【解决方案1】：

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

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

顺便说一句，以下变体适用于rise4fun（也可用here）：

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

【讨论】：