以下等效吗？mkInt(3)和(IntExpr) mkIntConst("3")？
第二个不是创建一个名为“ 3”的整数常量，对吗？我要使用mkIntConst创建一个数值为3的常量。可能吗？
最佳答案
mkIntConst创建具有给定名称的符号值。 （因此，在您的情况下，该变量名为3，它的值不为3。mkInt用该值创建一个常数。
是的，这些完全不同。
看到这里：https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_context.html#a99be64ea1573a49e683067bf6023ffa4
如果要创建具有值3的符号值，请使用mkIntConst创建一个符号值，然后向该求解器添加一个断言，指示其等于3。