bits.smt2

(declare-const |~prime| Int)
(declare-const |~one| Int)

(declare-const x Int)

(declare-const b1 Int)
(declare-const b2 Int)
(declare-const b3 Int)
(declare-const b4 Int)
(declare-const b5 Int)
(declare-const b6 Int)
(declare-const b7 Int)
(declare-const b8 Int)

(declare-const c1 Int)
(declare-const c2 Int)
(declare-const c3 Int)
(declare-const c4 Int)
(declare-const c5 Int)
(declare-const c6 Int)
(declare-const c7 Int)
(declare-const c8 Int)

(assert (and
(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
(= |~one| 1)
))

(define-fun bits ((_0 Int) (_1 Int) (_2 Int) (_3 Int) (_4 Int) (_5 Int) (_6 Int) (_7 Int) (_8 Int)) Bool (and
	(= (mod (* (* |_1| 1) (* |_1| 1)) |~prime|) (mod (* |_1| 1) |~prime|))
	(= (mod (* (* |_2| 1) (* |_2| 1)) |~prime|) (mod (* |_2| 1) |~prime|))
	(= (mod (* (* |_3| 1) (* |_3| 1)) |~prime|) (mod (* |_3| 1) |~prime|))
	(= (mod (* (* |_4| 1) (* |_4| 1)) |~prime|) (mod (* |_4| 1) |~prime|))
	(= (mod (* (* |_5| 1) (* |_5| 1)) |~prime|) (mod (* |_5| 1) |~prime|))
	(= (mod (* (* |_6| 1) (* |_6| 1)) |~prime|) (mod (* |_6| 1) |~prime|))
	(= (mod (* (* |_7| 1) (* |_7| 1)) |~prime|) (mod (* |_7| 1) |~prime|))
	(= (mod (* (* |_8| 1) (* |_8| 1)) |~prime|) (mod (* |_8| 1) |~prime|))
	(= (mod (* (* |~one| 1) (+ (* |_1| 128) (* |_2| 64) (* |_3| 32) (* |_4| 16) (* |_5| 8) (* |_6| 4) (* |_7| 2) (* |_8| 1))) |~prime|) (mod (* |_0| 1) |~prime|))
))

(assert (and
(bits x b1 b2 b3 b4 b5 b6 b7 b8)
(bits x c1 c2 c3 c4 c5 c6 c7 c8)
(not (and
	(= b1 c1)
	(= b2 c2)
	(= b3 c3)
	(= b4 c4)
	(= b5 c5)
	(= b6 c6)
	(= b7 c7)
	(= b8 c8)
))
))

(check-sat)
(get-model)