Получавам странни статистически резултати, когато стартирам Z3 3.1 с команда -st опция. Ако натиснете Ctrl-C, Z3 отчита total_time ‹ време. В противен случай, ако изчакате Z3 да завърши: total_time > time.
Благодаря!
Това е грешка в Z3 за Linux (версии 3.0 и 3.1). Грешката не засяга версията на Windows. Корекцията ще бъде налична в следващото издание (Z3 3.2). Таймерът, използван за проследяване на time, е неправилен.
Между другото, total-time измерва общото време за изпълнение, а time само времето, изразходвано от последната команда check-sat. Така че трябва да имаме това total-time >= time.
Забележка: този отговор е актуализиран с помощта на обратната връзка, предоставена от Swen Jacobs.
