Reverse Dungeon – Telegram
Reverse Dungeon
4.08K subscribers
713 photos
59 videos
982 files
2.23K links
Reverser's notes
The Mentor
1989
Download Telegram
Формальная верификация

x y z

x + y = 100
y + z = 100
x + z = 50

from z3 import *

x = [ BitVec(f"x{i}", 8) for i in range(3) ]
s = Solver()

s.add(x[0] + x[1] == 100)
s.add(x[1] + x[2] == 100)
s.add(x[0] + x[2] == 50)

s.check()
print(s.model())