Desde a atualização para o release de código aberto do Z3 (o mais recente git master), notei uma variação de tempo significativa entre execuções repetidas de consultas SMT quase idênticas usando a API C (em qualquer lugar de 2-122s). A única diferença entre as consultas é a nomenclatura de matrizes (na lógica QF_AUFBV).

Estamos alocando matrizes da seguinte forma:

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)));

Abaixo está uma consulta de exemplo (convertida para SMT-LIB). A substituição de "arr51" por outros nomes (por exemplo, "a" ou "arr51_0x2628008") altera significativamente a duração da consulta em até duas ordens de magnitude. As execuções repetidas sem variar o nome da matriz não exibem uma variação de tempo significativa.

Curiosamente, a versão binária antiga do Z3 3.2 não parece ser afetada pela nomenclatura de matriz (e é executada mais rapidamente na maioria das nossas consultas).

(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) bv0[18])))
(let (?x50 (bvadd (bvsub ?x42 (concat (extract[47:0] ?x23) bv0[16])) (concat (extract[49:0] ?x23) bv0[14])))
(let (?x58 (bvsub (bvadd ?x50 (concat (extract[50:0] ?x23) bv0[13])) (concat (extract[52:0] ?x23) bv0[11])))
(let (?x66 (bvadd (bvadd ?x58 (concat (extract[56:0] ?x23) bv0[7])) (concat (extract[59:0] ?x23) bv0[4])))
(let (?x68 (extract[63:32] (bvsub ?x66 ?x23)))
(flet ($x79 (= bv1[32] bv30[32]))
(let (?x80 (ite $x79 (concat bv0[30] (extract[31:30] (bvsub ?x16 ?x68))) (ite (= bv1[32] bv31[32]) (concat bv0[31] (extract[31:31] (bvsub ?x16 ?x68))) bv0[32])))
(flet ($x85 (= bv1[32] bv29[32]))
(flet ($x90 (= bv1[32] bv28[32]))
(let (?x91 (ite $x90 (concat bv0[28] (extract[31:28] (bvsub ?x16 ?x68))) (ite $x85 (concat bv0[29] (extract[31:29] (bvsub ?x16 ?x68))) ?x80)))
(flet ($x96 (= bv1[32] bv27[32]))
(flet ($x102 (= bv1[32] bv26[32]))
(let (?x103 (ite $x102 (concat bv0[26] (extract[31:26] (bvsub ?x16 ?x68))) (ite $x96 (concat bv0[27] (extract[31:27] (bvsub ?x16 ?x68))) ?x91)))
(flet ($x108 (= bv1[32] bv25[32]))
(flet ($x114 (= bv1[32] bv24[32]))
(let (?x115 (ite $x114 (concat bv0[24] (extract[31:24] (bvsub ?x16 ?x68))) (ite $x108 (concat bv0[25] (extract[31:25] (bvsub ?x16 ?x68))) ?x103)))
(flet ($x119 (= bv1[32] bv23[32]))
(flet ($x125 (= bv1[32] bv22[32]))
(let (?x126 (ite $x125 (concat bv0[22] (extract[31:22] (bvsub ?x16 ?x68))) (ite $x119 (concat bv0[23] (extract[31:23] (bvsub ?x16 ?x68))) ?x115)))
(flet ($x131 (= bv1[32] bv21[32]))
(flet ($x137 (= bv1[32] bv20[32]))
(let (?x138 (ite $x137 (concat bv0[20] (extract[31:20] (bvsub ?x16 ?x68))) (ite $x131 (concat bv0[21] (extract[31:21] (bvsub ?x16 ?x68))) ?x126)))
(flet ($x142 (= bv1[32] bv19[32]))
(flet ($x147 (= bv1[32] bv18[32]))
(let (?x148 (ite $x147 (concat bv0[18] (extract[31:18] (bvsub ?x16 ?x68))) (ite $x142 (concat bv0[19] (extract[31:19] (bvsub ?x16 ?x68))) ?x138)))
(flet ($x153 (= bv1[32] bv17[32]))
(flet ($x157 (= bv1[32] bv16[32]))
(let (?x158 (ite $x157 (concat bv0[16] (extract[31:16] (bvsub ?x16 ?x68))) (ite $x153 (concat bv0[17] (extract[31:17] (bvsub ?x16 ?x68))) ?x148)))
(flet ($x163 (= bv1[32] bv15[32]))
(flet ($x168 (= bv1[32] bv14[32]))
(let (?x169 (ite $x168 (concat bv0[14] (extract[31:14] (bvsub ?x16 ?x68))) (ite $x163 (concat bv0[15] (extract[31:15] (bvsub ?x16 ?x68))) ?x158)))
(flet ($x173 (= bv1[32] bv13[32]))
(flet ($x179 (= bv1[32] bv12[32]))
(let (?x180 (ite $x179 (concat bv0[12] (extract[31:12] (bvsub ?x16 ?x68))) (ite $x173 (concat bv0[13] (extract[31:13] (bvsub ?x16 ?x68))) ?x169)))
(flet ($x184 (= bv1[32] bv11[32]))
(flet ($x190 (= bv1[32] bv10[32]))
(let (?x191 (ite $x190 (concat bv0[10] (extract[31:10] (bvsub ?x16 ?x68))) (ite $x184 (concat bv0[11] (extract[31:11] (bvsub ?x16 ?x68))) ?x180)))
(flet ($x196 (= bv1[32] bv9[32]))
(flet ($x202 (= bv1[32] bv8[32]))
(let (?x203 (ite $x202 (concat bv0[8] (extract[31:8] (bvsub ?x16 ?x68))) (ite $x196 (concat bv0[9] (extract[31:9] (bvsub ?x16 ?x68))) ?x191)))
(flet ($x207 (= bv1[32] bv7[32]))
(flet ($x213 (= bv1[32] bv6[32]))
(let (?x214 (ite $x213 (concat bv0[6] (extract[31:6] (bvsub ?x16 ?x68))) (ite $x207 (concat bv0[7] (extract[31:7] (bvsub ?x16 ?x68))) ?x203)))
(flet ($x219 (= bv1[32] bv5[32]))
(flet ($x224 (= bv1[32] bv4[32]))
(let (?x225 (ite $x224 (concat bv0[4] (extract[31:4] (bvsub ?x16 ?x68))) (ite $x219 (concat bv0[5] (extract[31:5] (bvsub ?x16 ?x68))) ?x214)))
(flet ($x230 (= bv1[32] bv3[32]))
(flet ($x236 (= bv1[32] bv2[32]))
(let (?x237 (ite $x236 (concat bv0[2] (extract[31:2] (bvsub ?x16 ?x68))) (ite $x230 (concat bv0[3] (extract[31:3] (bvsub ?x16 ?x68))) ?x225)))
(flet ($x241 (= bv1[32] bv1[32]))
(let (?x69 (bvsub ?x16 ?x68))
(flet ($x243 (= bv1[32] bv0[32]))
(let (?x245 (bvadd (ite $x243 ?x69 (ite $x241 (concat bv0[1] (extract[31:1] ?x69)) ?x237)) ?x68))
(let (?x253 (ite (= bv16[32] bv30[32]) (concat bv0[30] (extract[31:30] ?x245)) (ite (= bv16[32] bv31[32]) (concat bv0[31] (extract[31:31] ?x245)) bv0[32])))
(let (?x261 (ite (= bv16[32] bv28[32]) (concat bv0[28] (extract[31:28] ?x245)) (ite (= bv16[32] bv29[32]) (concat bv0[29] (extract[31:29] ?x245)) ?x253)))
(let (?x269 (ite (= bv16[32] bv26[32]) (concat bv0[26] (extract[31:26] ?x245)) (ite (= bv16[32] bv27[32]) (concat bv0[27] (extract[31:27] ?x245)) ?x261)))
(let (?x277 (ite (= bv16[32] bv24[32]) (concat bv0[24] (extract[31:24] ?x245)) (ite (= bv16[32] bv25[32]) (concat bv0[25] (extract[31:25] ?x245)) ?x269)))
(let (?x285 (ite (= bv16[32] bv22[32]) (concat bv0[22] (extract[31:22] ?x245)) (ite (= bv16[32] bv23[32]) (concat bv0[23] (extract[31:23] ?x245)) ?x277)))
(let (?x293 (ite (= bv16[32] bv20[32]) (concat bv0[20] (extract[31:20] ?x245)) (ite (= bv16[32] bv21[32]) (concat bv0[21] (extract[31:21] ?x245)) ?x285)))
(let (?x301 (ite (= bv16[32] bv18[32]) (concat bv0[18] (extract[31:18] ?x245)) (ite (= bv16[32] bv19[32]) (concat bv0[19] (extract[31:19] ?x245)) ?x293)))
(let (?x309 (ite (= bv16[32] bv16[32]) (concat bv0[16] (extract[31:16] ?x245)) (ite (= bv16[32] bv17[32]) (concat bv0[17] (extract[31:17] ?x245)) ?x301)))
(let (?x317 (ite (= bv16[32] bv14[32]) (concat bv0[14] (extract[31:14] ?x245)) (ite (= bv16[32] bv15[32]) (concat bv0[15] (extract[31:15] ?x245)) ?x309)))
(let (?x325 (ite (= bv16[32] bv12[32]) (concat bv0[12] (extract[31:12] ?x245)) (ite (= bv16[32] bv13[32]) (concat bv0[13] (extract[31:13] ?x245)) ?x317)))
(let (?x333 (ite (= bv16[32] bv10[32]) (concat bv0[10] (extract[31:10] ?x245)) (ite (= bv16[32] bv11[32]) (concat bv0[11] (extract[31:11] ?x245)) ?x325)))
(let (?x341 (ite (= bv16[32] bv8[32]) (concat bv0[8] (extract[31:8] ?x245)) (ite (= bv16[32] bv9[32]) (concat bv0[9] (extract[31:9] ?x245)) ?x333)))
(let (?x349 (ite (= bv16[32] bv6[32]) (concat bv0[6] (extract[31:6] ?x245)) (ite (= bv16[32] bv7[32]) (concat bv0[7] (extract[31:7] ?x245)) ?x341)))
(let (?x357 (ite (= bv16[32] bv4[32]) (concat bv0[4] (extract[31:4] ?x245)) (ite (= bv16[32] bv5[32]) (concat bv0[5] (extract[31:5] ?x245)) ?x349)))
(let (?x365 (ite (= bv16[32] bv2[32]) (concat bv0[2] (extract[31:2] ?x245)) (ite (= bv16[32] bv3[32]) (concat bv0[3] (extract[31:3] ?x245)) ?x357)))
(let (?x371 (ite (= bv16[32] bv0[32]) ?x245 (ite (= bv16[32] bv1[32]) (concat bv0[1] (extract[31:1] ?x245)) ?x365)))
(let (?x372 (concat bv0[32] ?x371))
(let (?x380 (bvsub (bvadd (concat (extract[32:0] ?x372) bv0[31]) (concat (extract[34:0] ?x372) bv0[29])) (concat (extract[36:0] ?x372) bv0[27])))
(let (?x386 (bvsub (bvadd ?x380 (concat (extract[38:0] ?x372) bv0[25])) (concat (extract[40:0] ?x372) bv0[23])))
(let (?x392 (bvsub (bvadd ?x386 (concat (extract[42:0] ?x372) bv0[21])) (concat (extract[44:0] ?x372) bv0[19])))
(let (?x398 (bvsub (bvadd ?x392 (concat (extract[46:0] ?x372) bv0[17])) (concat (extract[48:0] ?x372) bv0[15])))
(let (?x404 (bvsub (bvadd ?x398 (concat (extract[50:0] ?x372) bv0[13])) (concat (extract[52:0] ?x372) bv0[11])))
(let (?x410 (bvsub (bvadd ?x404 (concat (extract[54:0] ?x372) bv0[9])) (concat (extract[56:0] ?x372) bv0[7])))
(let (?x416 (bvsub (bvadd ?x410 (concat (extract[58:0] ?x372) bv0[5])) (concat (extract[60:0] ?x372) bv0[3])))
(let (?x420 (extract[63:32] (bvadd ?x416 (concat (extract[62:0] ?x372) bv0[1]))))
(let (?x427 (ite $x79 (concat bv0[30] (extract[31:30] (bvsub ?x371 ?x420))) (ite (= bv1[32] bv31[32]) (concat bv0[31] (extract[31:31] (bvsub ?x371 ?x420))) bv0[32])))
(let (?x433 (ite $x90 (concat bv0[28] (extract[31:28] (bvsub ?x371 ?x420))) (ite $x85 (concat bv0[29] (extract[31:29] (bvsub ?x371 ?x420))) ?x427)))
(let (?x439 (ite $x102 (concat bv0[26] (extract[31:26] (bvsub ?x371 ?x420))) (ite $x96 (concat bv0[27] (extract[31:27] (bvsub ?x371 ?x420))) ?x433)))
(let (?x445 (ite $x114 (concat bv0[24] (extract[31:24] (bvsub ?x371 ?x420))) (ite $x108 (concat bv0[25] (extract[31:25] (bvsub ?x371 ?x420))) ?x439)))
(let (?x451 (ite $x125 (concat bv0[22] (extract[31:22] (bvsub ?x371 ?x420))) (ite $x119 (concat bv0[23] (extract[31:23] (bvsub ?x371 ?x420))) ?x445)))
(let (?x457 (ite $x137 (concat bv0[20] (extract[31:20] (bvsub ?x371 ?x420))) (ite $x131 (concat bv0[21] (extract[31:21] (bvsub ?x371 ?x420))) ?x451)))
(let (?x463 (ite $x147 (concat bv0[18] (extract[31:18] (bvsub ?x371 ?x420))) (ite $x142 (concat bv0[19] (extract[31:19] (bvsub ?x371 ?x420))) ?x457)))
(let (?x469 (ite $x157 (concat bv0[16] (extract[31:16] (bvsub ?x371 ?x420))) (ite $x153 (concat bv0[17] (extract[31:17] (bvsub ?x371 ?x420))) ?x463)))
(let (?x475 (ite $x168 (concat bv0[14] (extract[31:14] (bvsub ?x371 ?x420))) (ite $x163 (concat bv0[15] (extract[31:15] (bvsub ?x371 ?x420))) ?x469)))
(let (?x481 (ite $x179 (concat bv0[12] (extract[31:12] (bvsub ?x371 ?x420))) (ite $x173 (concat bv0[13] (extract[31:13] (bvsub ?x371 ?x420))) ?x475)))
(let (?x487 (ite $x190 (concat bv0[10] (extract[31:10] (bvsub ?x371 ?x420))) (ite $x184 (concat bv0[11] (extract[31:11] (bvsub ?x371 ?x420))) ?x481)))
(let (?x493 (ite $x202 (concat bv0[8] (extract[31:8] (bvsub ?x371 ?x420))) (ite $x196 (concat bv0[9] (extract[31:9] (bvsub ?x371 ?x420))) ?x487)))
(let (?x499 (ite $x213 (concat bv0[6] (extract[31:6] (bvsub ?x371 ?x420))) (ite $x207 (concat bv0[7] (extract[31:7] (bvsub ?x371 ?x420))) ?x493)))
(let (?x505 (ite $x224 (concat bv0[4] (extract[31:4] (bvsub ?x371 ?x420))) (ite $x219 (concat bv0[5] (extract[31:5] (bvsub ?x371 ?x420))) ?x499)))
(let (?x511 (ite $x236 (concat bv0[2] (extract[31:2] (bvsub ?x371 ?x420))) (ite $x230 (concat bv0[3] (extract[31:3] (bvsub ?x371 ?x420))) ?x505)))
(let (?x421 (bvsub ?x371 ?x420))
(let (?x516 (bvadd (ite $x243 ?x421 (ite $x241 (concat bv0[1] (extract[31:1] ?x421)) ?x511)) ?x420))
(let (?x524 (ite (= bv3[32] bv30[32]) (concat bv0[30] (extract[31:30] ?x516)) (ite (= bv3[32] bv31[32]) (concat bv0[31] (extract[31:31] ?x516)) bv0[32])))
(let (?x532 (ite (= bv3[32] bv28[32]) (concat bv0[28] (extract[31:28] ?x516)) (ite (= bv3[32] bv29[32]) (concat bv0[29] (extract[31:29] ?x516)) ?x524)))
(let (?x540 (ite (= bv3[32] bv26[32]) (concat bv0[26] (extract[31:26] ?x516)) (ite (= bv3[32] bv27[32]) (concat bv0[27] (extract[31:27] ?x516)) ?x532)))
(let (?x548 (ite (= bv3[32] bv24[32]) (concat bv0[24] (extract[31:24] ?x516)) (ite (= bv3[32] bv25[32]) (concat bv0[25] (extract[31:25] ?x516)) ?x540)))
(let (?x556 (ite (= bv3[32] bv22[32]) (concat bv0[22] (extract[31:22] ?x516)) (ite (= bv3[32] bv23[32]) (concat bv0[23] (extract[31:23] ?x516)) ?x548)))
(let (?x564 (ite (= bv3[32] bv20[32]) (concat bv0[20] (extract[31:20] ?x516)) (ite (= bv3[32] bv21[32]) (concat bv0[21] (extract[31:21] ?x516)) ?x556)))
(let (?x572 (ite (= bv3[32] bv18[32]) (concat bv0[18] (extract[31:18] ?x516)) (ite (= bv3[32] bv19[32]) (concat bv0[19] (extract[31:19] ?x516)) ?x564)))
(let (?x580 (ite (= bv3[32] bv16[32]) (concat bv0[16] (extract[31:16] ?x516)) (ite (= bv3[32] bv17[32]) (concat bv0[17] (extract[31:17] ?x516)) ?x572)))
(let (?x588 (ite (= bv3[32] bv14[32]) (concat bv0[14] (extract[31:14] ?x516)) (ite (= bv3[32] bv15[32]) (concat bv0[15] (extract[31:15] ?x516)) ?x580)))
(let (?x596 (ite (= bv3[32] bv12[32]) (concat bv0[12] (extract[31:12] ?x516)) (ite (= bv3[32] bv13[32]) (concat bv0[13] (extract[31:13] ?x516)) ?x588)))
(let (?x604 (ite (= bv3[32] bv10[32]) (concat bv0[10] (extract[31:10] ?x516)) (ite (= bv3[32] bv11[32]) (concat bv0[11] (extract[31:11] ?x516)) ?x596)))
(let (?x612 (ite (= bv3[32] bv8[32]) (concat bv0[8] (extract[31:8] ?x516)) (ite (= bv3[32] bv9[32]) (concat bv0[9] (extract[31:9] ?x516)) ?x604)))
(let (?x620 (ite (= bv3[32] bv6[32]) (concat bv0[6] (extract[31:6] ?x516)) (ite (= bv3[32] bv7[32]) (concat bv0[7] (extract[31:7] ?x516)) ?x612)))
(let (?x628 (ite (= bv3[32] bv4[32]) (concat bv0[4] (extract[31:4] ?x516)) (ite (= bv3[32] bv5[32]) (concat bv0[5] (extract[31:5] ?x516)) ?x620)))
(let (?x636 (ite (= bv3[32] bv2[32]) (concat bv0[2] (extract[31:2] ?x516)) (ite (= bv3[32] bv3[32]) (concat bv0[3] (extract[31:3] ?x516)) ?x628)))
(let (?x642 (ite (= bv3[32] bv0[32]) ?x516 (ite (= bv3[32] bv1[32]) (concat bv0[1] (extract[31:1] ?x516)) ?x636)))
(let (?x648 (bvsub ?x371 (bvadd (concat (extract[28:0] ?x642) bv0[3]) (concat (extract[30:0] ?x642) bv0[1]))))
(= bv253[8] (extract[7:0] ?x648))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
: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))
(not (= bv4294967295[32] ?x16))))
: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))
(bvule bv100000[32] ?x16)))
: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))
(bvule ?x16 bv999999[32])))
: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 (?x17 (sign_extend[32] ?x16))
(bvsle bv0[64] ?x17))))
:formula
true
)

Eu tentei definir explicitamente as sementes aleatórias, mas isso (sem surpresa) não ajudou:

Z3_set_param_value(z3_config, "ARITH_RANDOM_SEED", "0");
Z3_set_param_value(z3_config, "RANDOM_SEED", "0");

É normal que o Z3 exiba uma variação de tempo significativa apenas alterando os nomes dos símbolos?

Além disso, existe algum esquema de nomenclatura de matriz que reduza o tempo de solução no quadro?

Obrigado!