저는 실시간 작업 시스템에서 얻은 일정의 견고성을 증명하기 위해 Z3을 사용하고 있습니다. 이 스크립트를 확인할 때 http://www.cs.ru.nl/~georgeta/script.smt2 나는 답을 얻지 못했다. 그러나 PROOF_MODE = 1 옵션을 사용하면 응답이 앉습니다. 전자의 경우에 무엇이 잘못 될 수 있습니까?PROOF_MODE 옵션을 사용하지 않은 경우 응답이 없습니다
예제를 다운로드했습니다.
(설정 논리 QF_AUFLIA)
이 논리는 스크립트는 배열, 해석의 기능 및 정수 변수없이 한정사를 포함하도록 지정 : 지정된 논리는 잘못된 명령입니다. 그러나 실제 변수가 포함되어 있습니다. 이 명령을 제거하면 두 경우 모두에서 올바른 대답 (sat)을 얻게됩니다. Z3의 일부 프리 프로세서가 테스트 생성을 지원하지 않기 때문에 PROOF_MODE = 1을 사용할 때 다른 대답을 얻었습니다. 그런 다음 테스트 생성이 켜져 있으면 사용할 수 없습니다.
즉, 우리는 Z3 2.19에 많은 버그를 수정했습니다. 새 버전 3.0이 곧 출시 될 예정입니다. 제출 한 시험판 버전을 SMT-COMP으로 이미 사용할 수 있습니다.
도움 주셔서 감사합니다. 실제로 잘못된 로직이 사용되었습니다 ... set-logic 명령이 선택 사항임을 알기 좋습니다. –