1(set-logic QF_UF) 2(set-info :status sat) 3(declare-sort var 0) 4(declare-sort reg 0) 5(declare-fun a1_1 () var) 6(declare-fun a2_1 () var) 7(declare-fun c_3 () var) 8(declare-fun c_4 () var) 9(declare-fun b_3 () var) 10(declare-fun r0 () reg) 11(declare-fun r1 () reg) 12(declare-fun r2 () reg) 13(declare-fun r3 () reg) 14(declare-fun r4 () reg) 15(declare-fun r6 () reg) 16(assert (not (= r0 r1))) 17(assert (not (= r0 r2))) 18(assert (not (= r0 r3))) 19(assert (not (= r0 r4))) 20(assert (not (= r0 r6))) 21(assert (not (= r1 r2))) 22(assert (not (= r1 r3))) 23(assert (not (= r1 r4))) 24(assert (not (= r1 r6))) 25(assert (not (= r2 r3))) 26(assert (not (= r2 r4))) 27(assert (not (= r2 r6))) 28(assert (not (= r3 r4))) 29(assert (not (= r3 r6))) 30(assert (not (= r4 r6))) 31(declare-fun assign (var) reg) 32(assert (or (= (assign a1_1) r0) (= (assign a1_1) r1) (= (assign a1_1) r2) (= (assign a1_1) r3) (= (assign a1_1) r4) (= (assign a1_1) r6) )) 33(assert (or (= (assign a2_1) r0) (= (assign a2_1) r1) (= (assign a2_1) r2) (= (assign a2_1) r3) (= (assign a2_1) r4) (= (assign a2_1) r6) )) 34(assert (or (= (assign c_3) r0) (= (assign c_3) r1) (= (assign c_3) r2) (= (assign c_3) r3) (= (assign c_3) r4) (= (assign c_3) r6) )) 35(assert (or (= (assign c_4) r0) (= (assign c_4) r1) (= (assign c_4) r2) (= (assign c_4) r3) (= (assign c_4) r4) (= (assign c_4) r6) )) 36(assert (or (= (assign b_3) r0) (= (assign b_3) r1) (= (assign b_3) r2) (= (assign b_3) r3) (= (assign b_3) r4) (= (assign b_3) r6) )) 37(assert (not (= (assign a1_1) (assign c_4)))) 38(assert (not (= (assign a2_1) (assign c_3)))) 39(assert (not (= (assign a2_1) (assign b_3)))) 40(assert (not (= (assign c_3) (assign b_3)))) 41(assert (not (= (assign c_4) (assign b_3)))) 42(assert (= (assign a1_1) r0)) 43(assert (= (assign a2_1) r2)) 44(assert (= (assign c_3) r1)) 45(assert (= (assign c_4) r1)) 46(assert (= (assign b_3) r0)) 47(check-sat) 48(exit) 49