독립 도구와 라이브러리
논리식을 입력해 판정을 받는 도구로 실행하거나 다른 프로그램의 라이브러리로 연결할 수 있다. 이론 또는 여러 이론의 조합에 대한 만족 가능성을 처리한다. 실제 프로그램을 분석하려면 그 동작을 논리식으로 옮기는 별도의 과정이 필요하다.
이전 세대와의 관계
이름은 CVC 계열의 네 번째 도구를 뜻하지만 앞선 버전의 코드를 그대로 포함한 구현은 아니다. CVC4와 cvc5도 별도 버전 및 API 환경으로 구분해야 한다. 이름의 연속성만으로 소스나 설정의 호환성을 판단하지 않는다.
보관된 도구의 활용
저장소는 최종 CVC4 버전의 아카이브라고 명시하며 새 오류 보고 대신 cvc5로 이전하도록 안내한다. 과거 연구를 재현할 때는 당시 버전을 보존하는 의미가 있다. 새 분석 환경을 구축할 때는 유지 상태와 의존성 호환성을 함께 고려한다.
관련 문서
cvc5 / Z3 / Yices / Smt-Switch