Z3 통계 : 시간 측정은 무엇입니까?

Question

-st 명령 옵션을 사용하여 Z3 3.1을 실행할 때 이상한 통계 결과가 나타납니다. Ctrl-C를 누르면 Z3에서 total_time< 시간을보고합니다. 그렇지 않으면, Z3가 완료 될 때까지 기다린다면 : total_time> time.

1. "총 시간"과 "시간"은 무엇을 측정합니까?
2. 버그 (사소하지만) (위에서 설명한 차이점)?

고마워요!

Answer 1

이것은 Linux (버전 3.0 및 3.1)의 Z3 버그입니다. 버그는 Windows 버전에 영향을주지 않습니다. 이 수정본은 다음 릴리스 (Z3 3.2)에서 사용할 수 있습니다. time을 추적하는 데 사용 된 타이머가 잘못되었습니다.

BTW, total-time은 총 실행 시간을 측정하며 time은 마지막 check-sat 명령이 소비 한 시간 만 측정합니다. 그래서, 우리는 그것을 가지고 있어야합니다 total-time >= time.

참고 :이 답변은 Swen Jacobs가 제공 한 피드백을 사용하여 업데이트되었습니다.