Estamos teniendo problemas de rendimiento con lo que creo que es la parte de Z3 que trata la aritmética no lineal. Aquí hay un ejemplo concreto simple de Boogie, que cuando se verifica con Z3 (versión 4.1) toma mucho tiempo (en el orden de 3 minutos) en completarse.

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

Parece que el problema se debe a una interacción de funciones, el supuesto de rango en variables enteras y multiplicaciones de valores enteros (desconocidos). La afirmación al final no debe ser demostrable. En lugar de fallar rápidamente, parece que Z3 tiene formas de crear una gran cantidad de términos de alguna manera, ya que sus consumos de memoria aumentan bastante rápidamente a unos 300 MB, momento en el que se rinde.

Me pregunto si esto es un error, o si es posible mejorar las heurísticas sobre cuándo Z3 debería detener la búsqueda en la dirección particular en la que actualmente está tratando de resolver el problema.

Una cosa interesante es que alinear la función usando

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

hace que la verificación termine muy rápidamente.

Antecedentes: Este es un caso de prueba mínimo para un problema que vemos en nuestro verificador Cáliz. Allí, los programas Boogie se vuelven mucho más largos, potencialmente con múltiples suposiciones de un tipo similar. A menudo, la verificación no parece estar terminando en absoluto.

¿Algunas ideas?