Ghost in the Shellcode 2015 - Blocky's Revenge Theorem

gistfile1.lisp

(declare-const c2 Bool)
(declare-const c3 Bool)
(declare-const c4 Bool)
(declare-const c5 Bool)
(declare-const c6 Bool)
(declare-const c7 Bool)
(declare-const c8 Bool)
(declare-const c9 Bool)
(declare-const c10 Bool)
(declare-const c11 Bool)
(declare-const c12 Bool)
(declare-const c13 Bool)
(declare-const c14 Bool)
(declare-const c15 Bool)
(declare-const c16 Bool)
(declare-const c17 Bool)
(declare-const c18 Bool)
(declare-const c19 Bool)
(declare-const c20 Bool)
(declare-const c21 Bool)
(declare-const c22 Bool)
(declare-const c23 Bool)
(declare-const c24 Bool)
(declare-const c25 Bool)
(declare-const c26 Bool)
(declare-const c27 Bool)
(declare-const c28 Bool)
(declare-const c29 Bool)
(declare-const c30 Bool)
(declare-const c31 Bool)
(declare-const c32 Bool)
(declare-const c33 Bool)

(define-fun f2 () Bool (not c18))
(define-fun f3 () Bool (not c20))
(define-fun f4 () Bool (not c4))
(define-fun f5 () Bool (not c22))
(define-fun f6 () Bool (not c6))
(define-fun f7 () Bool (not c24))
(define-fun f8 () Bool (not c26))
(define-fun f9 () Bool (not c10))
(define-fun f10 () Bool (and c7 c26))
(define-fun f11 () Bool (not c28))
(define-fun f12 () Bool (xor c7 c27))
(define-fun f13 () Bool (not c8))
(define-fun f14 () Bool (not c27))
(define-fun f15 () Bool (not c30))
(define-fun f16 () Bool (and c10 c29))
(define-fun f17 () Bool (not c9))
(define-fun f18 () Bool (not c28))
(define-fun f19 () Bool (not c14))
(define-fun f20 () Bool (and c11 c30))
(define-fun f21 () Bool (xor c10 c29))
(define-fun f22 () Bool (not c32))
(define-fun f23 () Bool (xor c11 c30))
(define-fun f24 () Bool (not c16))
(define-fun f25 () Bool (xor c13 c32))
(define-fun f26 () Bool (xor c15 c18))
(define-fun f27 () Bool (not c6))
(define-fun f28 () Bool (not c25))
(define-fun f29 () Bool (not c5))
(define-fun f30 () Bool (not c24))
(define-fun f31 () Bool (not c4))
(define-fun f32 () Bool (not c23))
(define-fun f33 () Bool (not c3))
(define-fun f34 () Bool (not c22))
(define-fun f35 () Bool (not c2))
(define-fun f36 () Bool (not c17))
(define-fun f37 () Bool (not c20))
(define-fun f38 () Bool (not c16))
(define-fun f39 () Bool (not c19))
(define-fun f40 () Bool (and c15 c18))
(define-fun f41 () Bool (not c14))
(define-fun f42 () Bool (and c13 c32))
(define-fun f43 () Bool (not c12))

(define-fun i2 () Bool (not f12))
(define-fun i3 () Bool (and f17 f18))
(define-fun i4 () Bool (xor f13 f14))
(define-fun i5 () Bool (xor f17 f18))
(define-fun i6 () Bool (and c31 f43))
(define-fun i7 () Bool (xor c33 f41))
(define-fun i8 () Bool (xor f38 f39))
(define-fun i9 () Bool (xor f36 f37))
(define-fun i10 () Bool (xor c21 f35))
(define-fun i11 () Bool (xor f34 f33))
(define-fun i12 () Bool (xor f31 f32))
(define-fun i13 () Bool (xor f29 f30))
(define-fun i14 () Bool (xor f27 f28))
(define-fun i15 () Bool (and f27 f28))
(define-fun i16 () Bool (and f29 f30))
(define-fun i17 () Bool (and f31 f32))
(define-fun i18 () Bool (and f33 f34))
(define-fun i19 () Bool (and f35 c21))
(define-fun i20 () Bool (and f36 f37))
(define-fun i21 () Bool (and f38 f39))
(define-fun i22 () Bool (and f41 c33))
(define-fun i23 () Bool (xor c31 f43))

(define-fun l2 () Bool (xor i14 f10))
(define-fun l3 () Bool (or i2 f11))
(define-fun l4 () Bool (and c26 c7 i14))

(define-fun o2 () Bool (or l2 f9))
(define-fun o3 () Bool (or i15 l4))

(define-fun r2 () Bool (xor i13 o3))
(define-fun r3 () Bool (and o3 i13))

(define-fun u2 () Bool (not r2))
(define-fun u3 () Bool (or i16 r3))

(define-fun x2 () Bool (xor i12 u3))
(define-fun x3 () Bool (or u2 f8))
(define-fun x4 () Bool (and u3 i12))

(define-fun aa2 () Bool (not x2))
(define-fun aa3 () Bool (or i17 x4))

(define-fun ad2 () Bool (xor i11 aa3))
(define-fun ad3 () Bool (or aa2 c8))
(define-fun ad4 () Bool (and aa3 i11))

(define-fun ag2 () Bool (or ad2 f7))
(define-fun ag3 () Bool (or i18 ad4))

(define-fun aj2 () Bool (xor i10 ag3))
(define-fun aj3 () Bool (and ag3 i10))

(define-fun am2 () Bool (not aj2))
(define-fun am3 () Bool (or i19 aj3))

(define-fun l8 () Bool (xor i9 am3))
(define-fun l9 () Bool (or am2 f6))
(define-fun l10 () Bool (and am3 i9))

(define-fun o8 () Bool (or l8 f5))
(define-fun o9 () Bool (or i20 l10))

(define-fun r8 () Bool (xor i8 o9))
(define-fun r9 () Bool (and o9 i8))

(define-fun u8 () Bool (not r8))
(define-fun u9 () Bool (or i21 r9))

(define-fun x8 () Bool (xor f26 u9))
(define-fun x9 () Bool (or u8 f4))
(define-fun x10 () Bool (and u9 f26))

(define-fun aa8 () Bool (or x8 f3))
(define-fun aa9 () Bool (or f40 x10))

(define-fun ad8 () Bool (xor i7 aa9))
(define-fun ad9 () Bool (and aa9 i7))

(define-fun ag8 () Bool (not ad8))
(define-fun ag9 () Bool (or i22 ad9))

(define-fun aj8 () Bool (xor f25 ag9))
(define-fun aj9 () Bool (or ag8 c2))
(define-fun aj10 () Bool (and ag9 f25))

(define-fun am8 () Bool (not aj8))
(define-fun am9 () Bool (or f42 aj10))

(define-fun l13 () Bool (or am8 f2))
(define-fun l14 () Bool (and am9 i23))
(define-fun l15 () Bool (xor i23 am9))

(define-fun o13 () Bool (or i6 l14))
(define-fun o14 () Bool (not l15))

(define-fun r13 () Bool (and o13 f23))
(define-fun r14 () Bool (xor f23 o13))

(define-fun u13 () Bool (or f20 r13))
(define-fun u14 () Bool (not r14))

(define-fun x13 () Bool (and u13 f21))
(define-fun x14 () Bool (xor f21 u13))
(define-fun x15 () Bool (or u14 f22))

(define-fun aa13 () Bool (or f16 x13))
(define-fun aa14 () Bool (or x14 f19))
(define-fun aa15 () Bool (or o14 f24 x15))

(define-fun ad13 () Bool (and aa13 i5))
(define-fun ad14 () Bool (xor i5 aa13))

(define-fun ag13 () Bool (or i3 ad13))
(define-fun ag14 () Bool (not ad14))

(define-fun aj13 () Bool (xor i4 ag13))
(define-fun aj14 () Bool (or ag14 f15))

(define-fun am13 () Bool (not aj13))
(define-fun am14 () Bool (or aa15 aa14 aj14))

(define-fun l21 () Bool (or am13 c12))

(define-fun o21 () Bool (or am14 l21 l3))

(define-fun r21 () Bool (or o21 o2 x3))

(define-fun u21 () Bool (or r21 ad3 ag2))

(define-fun x21 () Bool (or u21 l9 o8))

(define-fun aa21 () Bool (or x21 x9 aa8))

(define-fun ad21 () Bool (or aa21 aj9 l13))

(define-fun ag21 () Bool (not ad21))

(assert ag21)
(check-sat)
(get-model)