Это крайне маловероятно, особенно если учесть, что вы заново создаете солвер Но это невозможно опровергнуть, поскольку вы на самом деле не показали ни одного кода, чтобы увидеть, могут ли быть ошибки.
Я бы рискнул предположить, что, если вы всегда будете наблюдать, как первое решение будет медленнее, чем После этого убедитесь, что вы правильно учли свой интерпретатор Python, чтобы запустить его, загрузить программу, загрузить всю необходимую инфраструктуру z3 и, наконец, вызвать решатель. Обратите внимание, что ничего из этого не будет дешевым, особенно если проблемы, которые вы тестируете, довольно малы.
Хороший способ для go состоит в том, чтобы отбросить временные результаты первых нескольких прогонов, чтобы убедиться, что все строки кэша в памяти прогреты и все выгружено. Затем выполните сравнение прогонов с 3 по 15. Вы все еще видите разницу? Это предполагает наличие других факторов, хотя я сомневаюсь в этом.
Но, опять же, все зависит от того, как вы это закодировали и какие проблемы вы сравниваете. Случайное начальное число, выбранное решающим устройством, может играть роль, но влияние этого должно быть случайным образом распределено, если оно есть.