自升级到Z3(最新的git master)的开源版本以来,我注意到使用C API(从2-122s开始)重复运行几乎相同的SMT查询之间存在显着的时序差异.查询之间的唯一区别是数组的命名(在QF_AUFBV逻辑中).
我们按如下方式分配数组:
Z3_symbol s = Z3_mk_string_symbol(z3_context, arrayName);
Z3_mk_const(z3_context, s,
Z3_mk_array_sort(z3_context, getSort(32), getSort(8)));
下面是一个示例查询(转换为SMT-LIB).将"arr51"替换为其他名称(例如,"a"或"arr51_0x2628008")会显着改变查询的持续时间,最多可达两个数量级.在不改变阵列名称的情况下重复运行不会出现明显的时序变化.
有趣的是,Z3 3.2的旧二进制版本似乎不受阵列命名的影响(并且对于我们的大多数查询运行速度更快).
(benchmark klee
:status unsat
:logic QF_AUFBV
:extrafuns ((arr51 Array[32:8]))
:assumption
(let (?x13 (concat (select arr51 bv58[32]) (concat (select arr51 bv57[32]) (select arr51 bv56[32]))))
(let (?x16 (concat (select arr51 bv59[32]) ?x13))
(let (?x23 (concat bv0[32] ?x16))
(let (?x34 (bvsub (bvadd (concat (extract[33:0] ?x23) bv0[30]) (concat (extract[35:0] ?x23) bv0[28])) (concat (extract[40:0] ?x23) bv0[23])))
(let (?x42 (bvadd (bvadd ?x34 (concat (extract[44:0] ?x23) bv0[19])) (concat (extract[45:0] ?x23) …z3 ×1