조건식과 검증의 연결
검증 도구는 프로그램에서 나온 조건을 논리식으로 옮겨 해결기에 전달한다. MathSAT는 그 식이 만족 가능한지와 관련 정보를 처리한다. 미해석 함수의 동등성, 산술, 비트벡터와 배열처럼 서로 다른 표현을 활용할 수 있다.
판정 이외의 정보
모델은 조건을 만족하는 값의 구성을 보여 주며, 불만족 코어는 함께 성립할 수 없는 조건의 일부를 나타낸다. 보간식과 증명 정보는 상위 검증 알고리즘에서도 활용된다. 어떤 기능을 사용할지는 분석 도구의 구성과 요구에 달려 있다.
이용 조건 확인
배포되는 MathSAT5는 연구와 평가 목적 이용 조건을 명시하며 상업 환경에서의 사용에는 서면 허가가 필요하다고 안내한다. 함께 사용한 다른 라이브러리의 라이선스만 보고 같은 조건이라고 가정하면 안 된다. 기술적 지원 범위와 이용 조건을 각각 확인한다.