>

Z3을 처음 사용했고 온라인 파이썬 튜토리얼을 확인하고있었습니다.

그런 다음 BitVecs에서 오버플로 동작을 확인할 수 있다고 생각했습니다.

이 코드를 썼습니다 :

x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))

그리고 나는 [y = 7, x = 7]을 기대하고 있었다 (즉, 값이 같지만 x + 1이 0이고 y + 1이 8이기 때문에 후속자가 아닌 경우)

그러나 Z3은 [y = 0, x = 0]으로 대답합니다.

내가 뭘 잘못하고 있니?


  • 답변 # 1

    나는 당신이 잘못하고 있다고 생각하지 않습니다. BV2Int 처럼 보입니다.  버그가 있습니다 :

    x = BitVec('x', 3)
     prove(x <= 3)
     prove(BV2Int(x) <= 3)
    
    

    Z3py는 첫 번째 것을 증명하지만 반대 예를 제시합니다.  두 번째. 소리가 안 들려요. (유일한 설명은 이상한 파이썬 일 수 있지만 방법을 모르겠습니다.)

    또한 귀하가 얻는 모델은 x=0 여부에 따라 다릅니다.  파이썬 바인딩에서 비트 벡터를 부호있는 숫자로 취급합니다. 그러나 +  서명되지 않은 값으로 처리하지 않을 수 있습니다. 이로 인해 문제가 더욱 복잡해집니다.

    어쨌든 BV2Int 처럼 보입니다.  꽤 정결하지 않습니다. Z3 사람들의 공식적인 답변이 나올 때까지 나는 그것을 피할 것입니다.

  • 답변 # 2

    이 문제가 우려되는 다른 사람들에게는 이것이 어느 시점에서 해결 된 것으로 보입니다. 이 예제를 최신 z3 버전 (초기 게시 후 몇 년)으로 다시 실행하면 7,7이 반환됩니다.

    BV2Int

  • 이전 html - 즉 조건문은 설명이 필요하다
  • 다음 android - SMS에서 브로드 캐스트 수신기가 작동하지 않습니다