값이 존재하는지 확인하기
여러 제약을 동시에 만족하는 값의 조합이 있는지 묻는 도구다. 실수와 정수 산술 및 비트벡터 등을 다루며 타입과 연산의 의미를 정확히 골라야 한다. 예를 들어 고정 폭 비트 연산과 수학적 정수 계산은 같은 모델이 아니다. 얻은 모델의 값도 입력으로 정의한 의미에 맞춰 해석한다.
지원 기능과 빌드 구성
선형과 비선형 산술을 지원하지만 비선형 처리를 위한 MC-SAT 구성에는 별도 빌드 조건이 있다. 실행 파일이 존재한다고 모든 기능이 준비되었다고 볼 수는 없다. 라이브러리의 스레드 안전성도 기본 구성에서 가정해서는 안 되며 해당 기능을 켜더라도 문맥과 모델을 다루는 스레드의 범위를 지켜야 한다.
검증 도구에 연결하기
SMT-LIB 입력을 보내거나 자체 명세 언어와 API를 사용할 수 있다. Java와 Python 및 Go 등에서 연결하는 바인딩도 제공한다. 프로그램 분석에서는 어떤 경로와 가정을 논리식으로 바꾸었는지가 결과를 결정한다. 만족 불가능한 결과와 미확정 결과를 구분하고 solver 버전과 설정 및 질의 자료를 함께 기록한다.