논리식 구성과 풀이 구분
정수나 불리언 같은 미지의 값을 만들고 필요한 관계를 논리식으로 표현한다. 식을 만드는 단계와 특정 solver로 푸는 단계는 분리되어 있다. 같은 모델이라도 선택한 이론과 기능에 따라 사용할 수 있는 solver가 달라질 수 있다. 타입에 맞는 식이라는 사실과 실제 문제를 올바르게 모델링했다는 사실도 구분한다.
개별 프로세스와 지속 연결
질의마다 새 solver를 실행하는 방식과 하나의 연결을 유지하며 여러 질의를 보내는 방식이 있다. 전자는 상태 관리가 단순하고 질의를 따로 실행하기 쉽다. 후자는 이전에 정의한 식과 가정을 재사용할 수 있지만 현재 solver 상태와 분석 도구의 상태를 맞춰야 한다. 여기서 연결 방식은 인터넷 접속 여부를 뜻하지 않는다.
결과와 호환성
조건을 만족하는 모델이 있는 결과와 불가능한 결과 및 알 수 없는 결과를 구분해 처리한다. 모델이 나왔다면 필요한 항의 값을 읽어 원래 문제와 비교한다. solver 버전에 따라 기능과 동작이 달라질 수 있어 공식 호환 범위를 확인한다. Crucible 같은 기호 실행 도구의 기반으로 활용되지만 라이브러리 자체가 임의의 소스를 자동 검증하지는 않는다.