Z3 статистика: что измеряет время?

Question

Я получаю странные статистические результаты при запуске Z3 3.1 с опцией -st команды. Если вы нажмете Ctrl-C, Z3 сообщит total_time < времени. В противном случае, если вы дождитесь окончания Z3: total_time> time.

1. Что измеряет «общее время» и «время»?
2. Это ошибка (хотя и незначительная) (разница выше)?

Спасибо!

Answer 1

Это ошибка в Z3 для Linux (версии 3.0 и 3.1). Ошибка не влияет на версию Windows. Исправление будет доступно в следующей версии (Z3 3.2). Неверный таймер, используемый для отслеживания time.

BTW, total-time измеряет общее время выполнения, а time - это время, затрачиваемое последней командой check-sat. Итак, мы должны иметь это total-time >= time.

Примечание: этот ответ был обновлен с использованием обратной связи, предоставленной Swen Jacobs.