Z3 を使用してプログラムの充足可能性をチェックする方法は? 例えば：
Boolean x, y
while(x is False) {
x = x or y
y = x & y
}
y = x or y
質問する
471 次
Z3 を使用してプログラムの充足可能性をチェックする方法は? 例えば：
Boolean x, y
while(x is False) {
x = x or y
y = x & y
}
y = x or y