Мы сталкиваемся с проблемами производительности, поскольку я считаю, что Z3 является частью нелинейной арифметики. Вот простой конкретный пример Boogie, который при проверке с Z3 (версия 4.1) занимает много времени (порядка 3 минут) для завершения.

const D: int;
function f(n: int) returns (int) { n * D }

procedure test() returns ()
{
  var a, b, c: int;
  var M: [int]int;
  var t: int;

  assume 0 < a && 1000 * a < f(1);
  assume 0 < c && 1000 * c < f(1);
  assume f(100) * b == a * c;

  assert M[t] > 0;
}

Кажется, что проблема вызвана взаимодействием функций, допущением диапазона целочисленных переменных, а также умножением (неизвестных) целочисленных значений. Утверждение в конце не должно быть доказуемым. Вместо быстрого отказа, кажется, что у Z3 есть способы как-то создать множество терминов, так как его потребление памяти довольно быстро увеличивается до 300 МБ, и в этот момент он сдается.

Мне интересно, является ли это ошибкой или возможно ли улучшить эвристику, когда Z3 должен остановить поиск в определенном направлении, в котором он в настоящее время пытается решить проблему.

Одна интересная вещь заключается в том, что встраивание функции с помощью

function {:inline} f(n: int) returns (int) { n * D }

заставляет проверку прекратить очень быстро.

Предыстория: это минимальный тестовый пример для проблемы, которую мы видим в нашей чаше верификатора. Там программы Boogie становятся намного длиннее, возможно, с несколькими предположениями подобного рода. Часто проверка не заканчивается вообще.

Есть идеи?