배경 이론을 포함한 논리식
일차 논리식이 여러 배경 이론과 그 조합 아래에서 만족 가능한지 다룬다. 단순한 참·거짓 변수의 조합보다 자료와 연산의 의미를 포함한 조건을 표현하는 문제에 쓰인다.
만족 가능성과 타당성
공식 소개는 만족 가능성과 그 쌍대적인 타당성을 판정하는 용도를 설명한다. 어떤 식에 해가 있는지와 어떤 조건에서 식이 타당한지는 검사할 논리 문제의 구성에 따라 구분된다.
함수를 합성하는 기능
구문 유도 합성인 SyGuS 엔진도 제공한다. 배경 이론과 그 조합을 이용해 정해진 표현 틀 안에서 함수를 합성하는 작업을 다룬다.
다른 도구와의 결합
CVC4를 이어 개방적이고 확장 가능한 SMT 엔진을 목표로 한다. 독립된 실행 도구로 사용하거나 라이브러리로 연결해 더 큰 분석 시스템의 일부로 활용할 수 있다.