조건을 만족하는 해 찾기
여러 조건을 논리식으로 표현하고 모두 참이 되게 하는 해석이 있는지 검사한다. 해석이 있으면 그 조건들의 모델이 되며 문제의 가능한 값을 구하는 데 사용할 수 있다.
자료형에 맞는 이론
정수와 실수, 비트 벡터, 배열과 문자열 같은 이론으로 서로 다른 대상을 표현한다. 수학적 정수와 실수는 고정된 크기의 기계 정수나 부동소수점 수와 구별해 모델링해야 한다.
소프트웨어 분석과의 연결
프로그램의 구성 요소를 지원하는 이론의 수식으로 옮기면 검증 문제를 논리식 풀이에 연결할 수 있다. Z3는 이런 변환을 수행하는 다른 도구 안의 저수준 구성 요소로 활용하도록 API를 제공한다.
공통 입력 형식
여러 SMT 도구가 사용하는 SMT-LIB 형식도 지원한다. 도구가 논리 모델을 직렬화하고 다시 읽을 수 있는 공통 표현을 통해 다른 분석 과정과 연결한다.