z3 사용

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



저작자표시

'Reversing' 카테고리의 다른 글

Sage n차 방정식 해 구하기 (mod n) feat. whitehatcontest2022(suspicious_signature)  (0) 2022.10.18
[rev] LazyKLEE / Symbolic Execution Engine  (0) 2022.10.18
angr이란  (1) 2018.04.28

+ Recent posts

티스토리툴바