Я получаю странные результаты статистики при запуске Z3 3.1 с опцией -st. Если вы нажмете Ctrl-C, Z3 сообщит общее время ‹ время. В противном случае, если вы дождетесь завершения Z3: total_time > time.
Спасибо!
Это ошибка в Z3 для Linux (версии 3.0 и 3.1). Ошибка не влияет на версию Windows. Исправление будет доступно в следующем выпуске (Z3 3.2). Таймер, используемый для отслеживания time, неверен.
Кстати, total-time измеряет общее время выполнения, а time — только время, затраченное последней командой check-sat. Итак, у нас должен быть этот total-time >= time.
Примечание: этот ответ был обновлен с использованием отзывов, предоставленных Свеном Джейкобсом.
