Reversing

z3 사용

MyriaBreak 2019. 9. 23. 23:34 
from z3 import *
s = Solver()
x1 = Int('x1')
x2 = Int('x2')
x3 = Int('x3')
x4 = Int('x4')
x5 = Int('x5')
s.add(x1 + x2 + x3 + x4 + x5 == x1*x2*x3*x4*x5)
print s.check()
print s.model()

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
from z3 import *
 
s = Solver()
 
# 변수들
x1 = Int('x1')
x2 = Int('x2')
x3 = Int('x3')
x4 = Int('x4')
x5 = Int('x5')
 
s.add(x1 + x2 + x3 + x4 + x5 == x1*x2*x3*x4*x5)        # 조건식
 
print s.check()
print s.model()
cs



저작자표시