연산의 의미 선택하기
비트벡터의 폭과 부호 및 부동소수점의 형식은 문제의 의미를 바꾼다. 같은 수식처럼 보여도 수학적 실수와 실제 반올림이 있는 연산은 결과가 다를 수 있다. 검증할 구현의 연산을 정확한 이론으로 옮겨야 풀이 결과를 원래 코드와 연결할 수 있다.
입력 지원과 검증 범위
명령행에서 SMT-LIBv2와 비순차 BTOR2 입력을 읽을 수 있다. BTOR2를 읽는다고 시간에 따른 상태 전이를 검사하는 모델 검사 기능까지 제공하는 것은 아니다. 단순 구문 분석과 전처리 및 실제 만족 가능성 판단도 다른 단계다. 어떤 실행 단계가 성공했는지 분명히 확인한다.
모델과 자원 제한
만족하는 모델을 생성하거나 불가능한 조건의 핵심을 얻는 기능을 선택할 수 있다. 시간과 메모리 제한 및 SAT 백엔드 설정은 수행 비용과 결과에 영향을 준다. 제한에 걸린 상태를 만족 불가능한 결과로 해석하지 않는다. 다른 도구에 연결할 때는 해당 API와 기능의 지원 여부를 확인하고 질의 및 설정을 함께 기록한다.