(declare-const op_1_instruction.action.block_1!1 Bool) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!5 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!3 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!4 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!3 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!12 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!8 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!15 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!14 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!9 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!6 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!16 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!4 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!7 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!5 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!6 (_ BitVec 64)) (declare-const op_1_instruction.operation.xor_general_0.ra!2 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.ra!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!11 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!10 (_ BitVec 64)) (declare-const temp64!12 (_ BitVec 64)) (declare-const temp64!13 (_ BitVec 64)) (declare-const temp64!14 (_ BitVec 64)) (declare-const temp64!15 (_ BitVec 64)) (declare-const temp64!16 (_ BitVec 64)) (declare-const temp64!17 (_ BitVec 64)) (declare-const temp64!18 (_ BitVec 64)) (declare-const op_1_instruction.operation.rs!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.D!1 (_ BitVec 16)) (declare-const temp64!19 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 (_ BitVec 5)) (declare-const __tmp_31!1 (_ BitVec 32)) (declare-const SPR!1 (Array (_ BitVec 10) (_ BitVec 64))) (declare-const op_2_instruction.address.0!2 (_ BitVec 64)) (declare-const op_2_instruction.address.0!3 (_ BitVec 64)) (declare-const op_2_instruction.address.0!4 (_ BitVec 64)) (declare-const temp_address!3 (_ BitVec 29)) (declare-const temp_address!2 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!12 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!11 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.ra.i!1 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!10 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.action.block_4!1 Bool) (declare-const temp64!10 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 Bool) (declare-const temp64!11 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_4!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.2!2 (_ BitVec 64)) (declare-const op_1_instruction.operation.rb!1 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.rb!1 (_ BitVec 32)) (declare-const temp64!20 (_ BitVec 64)) (declare-const temp64!21 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra.read.value.0!2 (_ BitVec 32)) (declare-const temp64!2 (_ BitVec 64)) (declare-const op_1_instruction.operation.xor_general_0.rb.read.index.0!2 (_ BitVec 5)) (declare-const temp64!4 (_ BitVec 64)) (declare-const temp64!3 (_ BitVec 64)) (declare-const temp64!6 (_ BitVec 64)) (declare-const temp64!5 (_ BitVec 64)) (declare-const temp64!8 (_ BitVec 64)) (declare-const temp64!7 (_ BitVec 64)) (declare-const temp64!9 (_ BitVec 64)) (declare-const BRANCH!2 (_ BitVec 1)) (declare-const __tmp_30!1 (_ BitVec 32)) (declare-const BRANCH!3 (_ BitVec 1)) (declare-const BRANCH!4 (_ BitVec 1)) (declare-const op_1_instruction.operation.xor_general_0.action.block_5!1 Bool) (declare-const temp64_0!12 (_ BitVec 64)) (declare-const temp64_0!11 (_ BitVec 64)) (declare-const temp64_0!10 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 Bool) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!5 (_ BitVec 8)) (declare-const op_1_instruction.operation.xor_general_0.rs!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!4 (_ BitVec 8)) (declare-const op_1_instruction.operation.ra!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!7 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!6 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!8 (_ BitVec 8)) (declare-const op_1_instruction.operation.xor_general_0.ra.tmp_1!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra!3 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra.write.value.2!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!2 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.byte_num!1 (_ BitVec 3)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!4 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!7 (_ BitVec 32)) (declare-const temp!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!5 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!8 (_ BitVec 32)) (declare-const temp!3 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!2 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!9 (_ BitVec 32)) (declare-const temp!4 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!3 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!4 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.ra!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!3 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!3 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!4 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!5 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!6 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!6 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!7 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!11 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!10 (_ BitVec 32)) (declare-const temp64_0!19 (_ BitVec 64)) (declare-const temp64_0!18 (_ BitVec 64)) (declare-const temp64_0!17 (_ BitVec 64)) (declare-const temp!5 (_ BitVec 32)) (declare-const temp64_0!16 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 Bool) (declare-const temp!6 (_ BitVec 32)) (declare-const temp64_0!15 (_ BitVec 64)) (declare-const temp64_0!14 (_ BitVec 64)) (declare-const op_1_instruction.operation.xor_general_0.ra.write.value.2!2 (_ BitVec 32)) (declare-const temp!7 (_ BitVec 32)) (declare-const temp64_0!13 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!12 (_ BitVec 32)) (declare-const CR!1 (_ BitVec 32)) (declare-const op_1_instruction.action.block_2!1 Bool) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_6!1 Bool) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!4 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.D!1 (_ BitVec 16)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 Bool) (declare-const op_2_instruction.operation.load_general_0.D!1 (_ BitVec 16)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!5 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra.write.index.2!2 (_ BitVec 5)) (declare-const op_1_instruction.operation.ra.i!1 (_ BitVec 5)) (declare-const op_1_instruction.address.0!2 (_ BitVec 64)) (declare-const op_1_instruction.address.0!3 (_ BitVec 64)) (declare-const op_1_instruction.address.0!4 (_ BitVec 64)) (declare-const MEM!9 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!8 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!5 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!4 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!7 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!6 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!1 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!3 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!2 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const CR!6 (_ BitVec 32)) (declare-const CR!5 (_ BitVec 32)) (declare-const CR!4 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 Bool) (declare-const op_1_instruction.operation.xor_general_0.action.block_3!1 Bool) (declare-const CR!3 (_ BitVec 32)) (declare-const CR!2 (_ BitVec 32)) (declare-const __tmp_7!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 Bool) (declare-const op_2_instruction.operation.rd.i!1 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1 (_ BitVec 5)) (declare-const temp1!3 (_ BitVec 32)) (declare-const temp1!2 (_ BitVec 32)) (declare-const op_2_instruction.action.block_1!1 Bool) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.5!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1 (_ BitVec 5)) (declare-const __tmp_23!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.rs.i!1 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.3!2 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.byte_num!1 (_ BitVec 3)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_19!1 Bool) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.upd!1 (_ BitVec 1)) (declare-const op_1_instruction.operation.xor_general_0.action.block_0!1 Bool) (declare-const __tmp_12!1 (_ BitVec 32)) (declare-const __tmp_6!1 (_ BitVec 32)) (declare-const NEXTPC!4 (_ BitVec 64)) (declare-const NEXTPC!3 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 Bool) (declare-const op_0_instruction.operation.ra.i!1 (_ BitVec 5)) (declare-const NEXTPC!2 (_ BitVec 64)) (declare-const temp2!4 (_ BitVec 32)) (declare-const temp2!3 (_ BitVec 32)) (declare-const temp2!2 (_ BitVec 32)) (declare-const upd_flag_mmu!2 (_ BitVec 1)) (declare-const upd_flag_mmu!3 (_ BitVec 1)) (declare-const __tmp_22!1 (_ BitVec 32)) (declare-const GPR!10 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!12 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!11 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_15!1 Bool) (declare-const op_1_instruction.operation.rb.i!1 (_ BitVec 5)) (declare-const GPR!14 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!13 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra!2 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra!3 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!3 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!2 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!5 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!4 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!7 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!6 (_ BitVec 29)) (declare-const __tmp_11!1 (_ BitVec 32)) (declare-const __tmp_34!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!2 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_1!1 Bool) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!3 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!6 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!7 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!4 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra.read.index.0!2 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!5 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.3!2 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.ra.i!1 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!8 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!9 (_ BitVec 32)) (declare-const __tmp_21!1 (_ BitVec 32)) (declare-const XO_10!2 (_ BitVec 10)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 Bool) (declare-const op_1_instruction.operation.xor_general_0.ra.read.index.0!2 (_ BitVec 5)) (declare-const __tmp_10!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.5!2 (_ BitVec 29)) (declare-const __tmp_9!1 (_ BitVec 32)) (declare-const __tmp_33!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!3 (_ BitVec 32)) (declare-const CIA!8 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!4 (_ BitVec 32)) (declare-const CIA!9 (_ BitVec 64)) (declare-const CIA!6 (_ BitVec 64)) (declare-const CIA!7 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!7 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!8 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!5 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!6 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!2 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!9 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.upd!1 (_ BitVec 1)) (declare-const __tmp_20!1 (_ BitVec 32)) (declare-const op_0_instruction.address.0!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!7 (_ BitVec 64)) (declare-const op_0_instruction.address.0!3 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!2 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!6 (_ BitVec 64)) (declare-const op_0_instruction.address.0!4 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!5 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!4 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!3 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!6 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!5 (_ BitVec 32)) (declare-const CIA!1 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!4 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!3 (_ BitVec 32)) (declare-const CIA!4 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!9 (_ BitVec 32)) (declare-const CIA!5 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!8 (_ BitVec 32)) (declare-const CIA!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!7 (_ BitVec 32)) (declare-const CIA!3 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 Bool) (declare-const __tmp_32!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.rd!1 (_ BitVec 32)) (declare-const CIA!10 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.D!1 (_ BitVec 32)) (declare-const __tmp_8!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.ra!1 (_ BitVec 32)) (declare-const __tmp_3!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra.write.index.2!2 (_ BitVec 5)) (declare-const op_1_instruction.operation.xor_general_0.Rc_op!1 (_ BitVec 1)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!5 (_ BitVec 29)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!8 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!6 (_ BitVec 29)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!9 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!6 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!7 (_ BitVec 29)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!7 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!4 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!2 (_ BitVec 29)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!5 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!2 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!3 (_ BitVec 29)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!3 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!4 (_ BitVec 29)) (declare-const __tmp_27!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 Bool) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.0!2 (_ BitVec 64)) (declare-const op_1_instruction.operation.xor_general_0.rs.i!1 (_ BitVec 5)) (declare-const op_1_instruction.operation.xor_general_0.ra.read.value.0!2 (_ BitVec 32)) (declare-const __tmp_16!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_0!1 Bool) (declare-const __tmp_2!1 (_ BitVec 32)) (declare-const temp_lo_index!2 (_ BitVec 3)) (declare-const temp_lo_index!3 (_ BitVec 3)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 Bool) (declare-const __tmp_26!1 (_ BitVec 32)) (declare-const Rc!2 (_ BitVec 1)) (declare-const op_2_instruction.operation.load_general_0.upd!1 (_ BitVec 1)) (declare-const GPR!6 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!7 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!4 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!5 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!2 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!3 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!1 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const __tmp_15!1 (_ BitVec 32)) (declare-const __tmp_5!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!2 (_ BitVec 32)) (declare-const GPR!8 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const GPR!9 (Array (_ BitVec 5) (_ BitVec 32))) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!8 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!7 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!9 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!4 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!3 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!6 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!5 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_0!1 Bool) (declare-const __tmp_25!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!6 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!7 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!2 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!3 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!4 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!4 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!3 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!5 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.ra.write.value.2!2 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!6 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!5 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!7 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!10 (_ BitVec 5)) (declare-const __tmp_14!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!12 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!11 (_ BitVec 5)) (declare-const __tmp_4!1 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.rb.read.value.0!2 (_ BitVec 32)) (declare-const op_1_instruction.operation.rs.i!1 (_ BitVec 5)) (declare-const temp0!3 (_ BitVec 32)) (declare-const temp0!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.ra.i!1 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_1!1 Bool) (declare-const op_2_instruction.action.block_2!1 Bool) (declare-const op_1_instruction.operation.xor_general_0.read.value.0!2 (_ BitVec 64)) (declare-const __tmp_24!1 (_ BitVec 32)) (declare-const OPCD!4 (_ BitVec 6)) (declare-const OPCD!3 (_ BitVec 6)) (declare-const OPCD!2 (_ BitVec 6)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.2!2 (_ BitVec 29)) (declare-const op_2_instruction.operation.load_general_0.byte_num!1 (_ BitVec 3)) (declare-const __tmp_13!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!7 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!5 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!6 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!3 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!4 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!2 (_ BitVec 29)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_6!1 Bool) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.D!1 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.ra.write.index.2!2 (_ BitVec 5)) (declare-const op_2_instruction.operation.ra!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!9 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!8 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!7 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!6 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!5 (_ BitVec 5)) (declare-const temp64_0!9 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!4 (_ BitVec 5)) (declare-const temp64_0!8 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!3 (_ BitVec 5)) (declare-const temp64_0!7 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!2 (_ BitVec 5)) (declare-const temp64_0!6 (_ BitVec 64)) (declare-const temp64_0!5 (_ BitVec 64)) (declare-const temp64_0!4 (_ BitVec 64)) (declare-const temp64_0!3 (_ BitVec 64)) (declare-const temp64_0!2 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.ra!1 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.read.index.0!2 Int) (declare-const op_0_instruction.action.block_1!1 Bool) (declare-const op_0_instruction.operation.D!1 (_ BitVec 16)) (declare-const __tmp_19!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!4 (_ BitVec 64)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!6 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!2 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!7 (_ BitVec 8)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!9 (_ BitVec 64)) (declare-const op_2_instruction.operation.load_general_0.rd.i!1 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!7 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!8 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!9 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 Bool) (declare-const MEM!16 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!3 (_ BitVec 32)) (declare-const MEM!15 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!4 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!5 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!6 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra.read.value.0!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.rd!2 (_ BitVec 32)) (declare-const MEM!12 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!11 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!14 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!13 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const MEM!10 (Array (_ BitVec 29) (_ BitVec 64))) (declare-const op_0_instruction.action.block_2!1 Bool) (declare-const __tmp_1!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.0!2 (_ BitVec 29)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 Bool) (declare-const op_1_instruction.operation.xor_general_0.rb.i!1 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 Bool) (declare-const __tmp_29!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.rs.i!1 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.rs!1 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.rs.read.value.0!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.byte_num!1 (_ BitVec 3)) (declare-const op_0_instruction.operation.store_general_0.ra.i!1 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 Bool) (declare-const __tmp_18!1 (_ BitVec 32)) (declare-const op_1_instruction.operation.xor_general_0.rs.read.index.0!2 (_ BitVec 5)) (declare-const __tmp_0!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!2 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 Bool) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!4 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!3 (_ BitVec 32)) (declare-const __tmp_28!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.rd!1 (_ BitVec 32)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.upd!1 (_ BitVec 1)) (declare-const op_0_instruction.operation.rs!1 (_ BitVec 32)) (declare-const __tmp_17!1 (_ BitVec 32)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1 (_ BitVec 5)) (declare-const op_2_instruction.operation.load_general_0.powerpc_load_0.ra.read.index.0!2 (_ BitVec 5)) (declare-const op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 Bool) (assert (= op_0_instruction.operation.rs.i!1 #b00011)) (assert (= op_0_instruction.operation.D!1 #b1111111111101000)) (assert (= op_0_instruction.operation.ra.i!1 #b00001)) (assert (and (= BRANCH!2 #b0) (= NEXTPC!2 #b0000000000000000000000000000000000000000000000000000000000000000) (= OPCD!2 #b100100) (= upd_flag_mmu!2 #b0) (= op_0_instruction.operation.store_general_0.rs.i!1 op_0_instruction.operation.rs.i!1) (= op_0_instruction.operation.store_general_0.rs!1 op_0_instruction.operation.rs!1) (= op_0_instruction.operation.store_general_0.D!1 op_0_instruction.operation.D!1) (= op_0_instruction.operation.store_general_0.ra.i!1 op_0_instruction.operation.ra.i!1) (= op_0_instruction.operation.store_general_0.ra!1 op_0_instruction.operation.ra!1) (= op_0_instruction.operation.store_general_0.upd!1 upd_flag_mmu!2) (= op_0_instruction.operation.store_general_0.byte_num!1 #b100) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1 op_0_instruction.operation.store_general_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 op_0_instruction.operation.store_general_0.rs!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.D!1 ((_ sign_extend 16) op_0_instruction.operation.store_general_0.D!1)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1 op_0_instruction.operation.store_general_0.ra.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra!1 op_0_instruction.operation.store_general_0.ra!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.upd!1 op_0_instruction.operation.store_general_0.upd!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.byte_num!1 op_0_instruction.operation.store_general_0.byte_num!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_0!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1 #b00000)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_1!1 (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_0!1))) (or (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_0!1 (= temp!2 #b00000000000000000000000000000000)) (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_1!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra.read.index.0!2 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra.read.value.0!2 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1) __tmp_0!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra!1 __tmp_0!1) (= temp!3 __tmp_0!1))) (and (= temp!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_1!1 temp!3 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_0!1 temp!2 temp!3)))) (= temp1!2 (bvadd temp!4 op_0_instruction.operation.store_general_0.powerpc_store_0.D!1)) (= temp_address!2 ((_ extract 28 0) (bvlshr temp1!2 #b00000000000000000000000000000011))) (= ((_ extract 2 0) temp_lo_index!2) ((_ extract 2 0) temp1!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.0!2 temp_address!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.0!2 (select MEM!1 temp_address!2)) (= temp64!2 (select MEM!1 temp_address!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.byte_num!1 #b001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 (and (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.byte_num!1 #b010))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 (and (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.byte_num!1 #b100))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_6!1 (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1))) (or (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!2 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!2 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_1!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_1!1) (= (bvshl temp64!2 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) (bvshl temp64!3 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2))))))) (= (bvlshr temp64!2 (bvadd ((_ zero_extend 58) (bvadd #b000111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001)) (bvlshr temp64!3 (bvadd ((_ zero_extend 58) (bvadd #b000111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001))) (= ((_ extract 8 0) (bvlshr temp64!3 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) ((_ zero_extend 1) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!2 ((_ extract 7 0) __tmp_1!1)) (= MEM!2 (store MEM!1 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.2!2 temp_address!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.2!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!2 temp64!3)) (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 (= temp_lo_index!2 #b111)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1))) (or (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!3 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!3 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_2!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_2!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!3 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!3 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_3!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_3!1) (= ((_ extract 55 0) temp64!4) ((_ extract 55 0) temp64!3)) (= ((_ extract 63 56) temp64!4) ((_ extract 7 0) __tmp_2!1)) (= MEM!3 (store MEM!2 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!4)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!2 temp_address!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!4) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!4 temp64!4) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!2 (bvadd temp_address!2 #b00000000000000000000000000001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!2 (select MEM!3 (bvadd temp_address!2 #b00000000000000000000000000001))) (= temp64_0!2 (select MEM!3 (bvadd temp_address!2 #b00000000000000000000000000001))) (= ((_ extract 63 8) temp64_0!3) ((_ extract 63 8) temp64_0!2)) (= ((_ extract 7 0) temp64_0!3) ((_ extract 15 8) __tmp_3!1)) (= MEM!4 (store MEM!3 (bvadd temp_address!2 #b00000000000000000000000000001) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!2 (bvadd temp_address!2 #b00000000000000000000000000001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!2 temp64_0!3)) (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!4 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!4 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_4!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_4!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!4 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!4 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_5!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_5!1) (= (bvshl temp64!3 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) (bvshl temp64!5 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2))))))) (= (bvlshr temp64!3 (bvadd ((_ zero_extend 58) (bvadd #b000111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001)) (bvlshr temp64!5 (bvadd ((_ zero_extend 58) (bvadd #b000111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001))) (= ((_ extract 8 0) (bvlshr temp64!5 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) ((_ zero_extend 1) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!6)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!6 ((_ extract 7 0) __tmp_4!1)) (= (bvshl temp64!5 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b001000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) (bvshl temp64!6 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b001000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2))))))) (= (bvlshr temp64!5 (bvadd ((_ zero_extend 58) (bvadd #b001111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001)) (bvlshr temp64!6 (bvadd ((_ zero_extend 58) (bvadd #b001111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001))) (= ((_ extract 8 0) (bvlshr temp64!6 ((_ zero_extend 58) (bvadd #b001000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) ((_ zero_extend 1) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!4)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!4 ((_ extract 15 8) __tmp_5!1)) (= MEM!5 (store MEM!2 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.3!2 temp_address!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.3!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!2 temp64!6))) (and (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!3 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!2))) (= MEM!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 MEM!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 MEM!4 MEM!2))) (= temp64!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 temp64!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 temp64!4 temp64!3))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!3 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!2))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!3 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!2))) (= ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!7) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!6) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_9!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!4 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!2)))) (= ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!5) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_10!1 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!4) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!2)))) (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 (bvugt temp_lo_index!2 #b100)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1))) (or (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 (= temp_lo_index!2 #b101)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 (and (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1)) (= temp_lo_index!2 #b110))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 (and (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1)) (= temp_lo_index!2 #b111))) (or (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!6 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!6 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_6!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_6!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!6 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!6 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_7!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_7!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!6 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!6 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_8!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_8!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!6 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!6 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_9!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_9!1) (= ((_ extract 39 0) temp64!8) ((_ extract 39 0) temp64!7)) (= ((_ extract 63 48) temp64!8) ((_ extract 63 48) temp64!7)) (= ((_ extract 47 40) temp64!8) ((_ extract 7 0) __tmp_6!1)) (= ((_ extract 47 0) temp64!9) ((_ extract 47 0) temp64!8)) (= ((_ extract 63 56) temp64!9) ((_ extract 63 56) temp64!8)) (= ((_ extract 55 48) temp64!9) ((_ extract 15 8) __tmp_7!1)) (= ((_ extract 55 0) temp64!10) ((_ extract 55 0) temp64!9)) (= ((_ extract 63 56) temp64!10) ((_ extract 23 16) __tmp_8!1)) (= MEM!7 (store MEM!6 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!9)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!3 temp_address!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!3 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!9) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!9 temp64!10) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!3 (bvadd temp_address!2 #b00000000000000000000000000001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!3 (select MEM!7 (bvadd temp_address!2 #b00000000000000000000000000001))) (= temp64_0!4 (select MEM!7 (bvadd temp_address!2 #b00000000000000000000000000001))) (= ((_ extract 63 8) temp64_0!5) ((_ extract 63 8) temp64_0!4)) (= ((_ extract 7 0) temp64_0!5) ((_ extract 31 24) __tmp_9!1)) (= MEM!8 (store MEM!7 (bvadd temp_address!2 #b00000000000000000000000000001) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!3)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!3 (bvadd temp_address!2 #b00000000000000000000000000001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!3 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!3) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!3 temp64_0!5)) (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!7 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!7 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_10!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_10!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!7 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!7 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_11!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_11!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!7 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!7 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_12!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_12!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!7 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!7 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_13!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_13!1) (= ((_ extract 47 0) temp64!11) ((_ extract 47 0) temp64!7)) (= ((_ extract 63 56) temp64!11) ((_ extract 63 56) temp64!7)) (= ((_ extract 55 48) temp64!11) ((_ extract 7 0) __tmp_10!1)) (= ((_ extract 55 0) temp64!12) ((_ extract 55 0) temp64!11)) (= ((_ extract 63 56) temp64!12) ((_ extract 15 8) __tmp_11!1)) (= MEM!9 (store MEM!6 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!10)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!4 temp_address!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!4 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!10) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!10 temp64!12) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!4 (bvadd temp_address!2 #b00000000000000000000000000001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!4 (select MEM!9 (bvadd temp_address!2 #b00000000000000000000000000001))) (= temp64_0!6 (select MEM!9 (bvadd temp_address!2 #b00000000000000000000000000001))) (= ((_ extract 63 8) temp64_0!7) ((_ extract 63 8) temp64_0!6)) (= ((_ extract 7 0) temp64_0!7) ((_ extract 23 16) __tmp_12!1)) (= ((_ extract 7 0) temp64_0!8) ((_ extract 7 0) temp64_0!7)) (= ((_ extract 63 16) temp64_0!8) ((_ extract 63 16) temp64_0!7)) (= ((_ extract 15 8) temp64_0!8) ((_ extract 31 24) __tmp_13!1)) (= MEM!10 (store MEM!9 (bvadd temp_address!2 #b00000000000000000000000000001) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!4)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!4 (bvadd temp_address!2 #b00000000000000000000000000001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!4 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!4) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!4 temp64_0!8)) (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!8 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!8 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_14!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_14!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!8 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!8 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_15!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_15!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!8 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!8 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_16!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_16!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!8 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!8 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_17!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_17!1) (= ((_ extract 55 0) temp64!13) ((_ extract 55 0) temp64!7)) (= ((_ extract 63 56) temp64!13) ((_ extract 7 0) __tmp_14!1)) (= MEM!11 (store MEM!6 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!11)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!5 temp_address!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!5 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!11) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!11 temp64!13) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!5 (bvadd temp_address!2 #b00000000000000000000000000001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!5 (select MEM!11 (bvadd temp_address!2 #b00000000000000000000000000001))) (= temp64_0!9 (select MEM!11 (bvadd temp_address!2 #b00000000000000000000000000001))) (= ((_ extract 63 8) temp64_0!10) ((_ extract 63 8) temp64_0!9)) (= ((_ extract 7 0) temp64_0!10) ((_ extract 15 8) __tmp_15!1)) (= ((_ extract 7 0) temp64_0!11) ((_ extract 7 0) temp64_0!10)) (= ((_ extract 63 16) temp64_0!11) ((_ extract 63 16) temp64_0!10)) (= ((_ extract 15 8) temp64_0!11) ((_ extract 23 16) __tmp_16!1)) (= ((_ extract 15 0) temp64_0!12) ((_ extract 15 0) temp64_0!11)) (= ((_ extract 63 24) temp64_0!12) ((_ extract 63 24) temp64_0!11)) (= ((_ extract 23 16) temp64_0!12) ((_ extract 31 24) __tmp_17!1)) (= MEM!12 (store MEM!11 (bvadd temp_address!2 #b00000000000000000000000000001) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!5)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!5 (bvadd temp_address!2 #b00000000000000000000000000001)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!5 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!5) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!5 temp64_0!12)) (and (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1)))) (and (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!3 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!2)))) (= temp64_0!13 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 temp64_0!12 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 temp64_0!8 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 temp64_0!5 temp64_0!3)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!9 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!8 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!6 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!5)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!3 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!2)))) (= temp64!14 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 temp64!13 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 temp64!12 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 temp64!10 temp64!7)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!3 op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!2)))) (= MEM!13 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 MEM!12 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 MEM!10 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 MEM!8 MEM!6)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!9 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!8 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!6 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!5)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!3 op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!2)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!3 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!2)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!3 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!2)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!3 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!2)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!9 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!8 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!6 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!5)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!12 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_17!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!11 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_16!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!10 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_15!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!9 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!7))))))) (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!10 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!10 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_18!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_18!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!10 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!10 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_19!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_19!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!10 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!10 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_20!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_20!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!10 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!10 (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1)) (= (select GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.i!1) __tmp_21!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs!1 __tmp_21!1) (= (bvshl temp64!2 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) (bvshl temp64!15 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2))))))) (= (bvlshr temp64!7 (bvadd ((_ zero_extend 58) (bvadd #b000111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001)) (bvlshr temp64!15 (bvadd ((_ zero_extend 58) (bvadd #b000111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001))) (= ((_ extract 7 0) (bvlshr temp64!15 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!14) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!14 ((_ extract 7 0) __tmp_18!1)) (= (bvshl temp64!15 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b001000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) (bvshl temp64!16 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b001000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2))))))) (= (bvlshr temp64!15 (bvadd ((_ zero_extend 58) (bvadd #b001111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001)) (bvlshr temp64!16 (bvadd ((_ zero_extend 58) (bvadd #b001111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001))) (= ((_ extract 7 0) (bvlshr temp64!16 ((_ zero_extend 58) (bvadd #b001000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!6) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!6 ((_ extract 15 8) __tmp_19!1)) (= (bvshl temp64!16 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b010000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) (bvshl temp64!17 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b010000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2))))))) (= (bvlshr temp64!16 (bvadd ((_ zero_extend 58) (bvadd #b010111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001)) (bvlshr temp64!17 (bvadd ((_ zero_extend 58) (bvadd #b010111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001))) (= ((_ extract 7 0) (bvlshr temp64!17 ((_ zero_extend 58) (bvadd #b010000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!4) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!4 ((_ extract 23 16) __tmp_20!1)) (= (bvshl temp64!17 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b011000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) (bvshl temp64!18 (bvsub #b0000000000000000000000000000000000000000000000000000000001000000 ((_ zero_extend 58) (bvadd #b011000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2))))))) (= (bvlshr temp64!17 (bvadd ((_ zero_extend 58) (bvadd #b011111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001)) (bvlshr temp64!18 (bvadd ((_ zero_extend 58) (bvadd #b011111 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))) #b0000000000000000000000000000000000000000000000000000000000000001))) (= ((_ extract 7 0) (bvlshr temp64!18 ((_ zero_extend 58) (bvadd #b011000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!2)))))) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!8) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!8 ((_ extract 31 24) __tmp_21!1)) (= MEM!14 (store MEM!1 temp_address!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_4!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.5!2 temp_address!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.5!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_4!2) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_4!2 temp64!18))) (and (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!6 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.4!2)) (= temp64_0!14 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 temp64_0!13 temp64_0!3)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!11 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!10 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!9 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!5))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!6 op_0_instruction.operation.store_general_0.powerpc_store_0.write.value.1!2)) (= temp64!19 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 temp64!18 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 temp64!14 temp64!7))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!6 op_0_instruction.operation.store_general_0.powerpc_store_0.read.index.2!2)) (= MEM!15 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 MEM!14 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 MEM!13 MEM!1))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!11 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!10 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!9 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!5))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!6 op_0_instruction.operation.store_general_0.powerpc_store_0.read.value.2!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!6 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.1!2)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!6 op_0_instruction.operation.store_general_0.powerpc_store_0.write.index.4!2)) (= ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!5) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!4) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_2!2)) (= ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!9) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!8) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!6 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_3!2))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!11 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!10 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!9 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!5))) (= ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!15) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!14) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_12!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!12 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!7)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_13!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!6 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!5)))) (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_6!1)) (and (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!12 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!11 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!2 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.value.0!11)))) (= temp64!20 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 temp64!19 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 temp64!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 temp64!3 temp64!2)))) (= MEM!16 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 MEM!15 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 MEM!6 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 MEM!2 MEM!1)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!12 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!11 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!2 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.tmp_1!11)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!16 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!15 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!7 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!2 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_0!15)))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!12 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!11 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!5 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!2 op_0_instruction.operation.store_general_0.powerpc_store_0.rs.read.index.0!11)))) (= ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!8) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_5!1 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!7) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_4!1 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!5) (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_3!1 op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!2 ((_ zero_extend 56) op_0_instruction.operation.store_general_0.powerpc_store_0.action.tmp_1!7)))))) (= op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_19!1 (and (= op_0_instruction.operation.store_general_0.powerpc_store_0.upd!1 #b1) (distinct op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1 #b00000))) (or (and op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_19!1 (= GPR!2 (store GPR!1 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!3)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra.write.index.2!2 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.i!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra.write.value.2!2 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!3) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!3 __tmp_22!1) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra!2 __tmp_22!1) (= __tmp_22!1 temp1!2)) (and (not (or op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_19!1)))) (and (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra!3 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_19!1 op_0_instruction.operation.store_general_0.powerpc_store_0.ra!2 op_0_instruction.operation.store_general_0.powerpc_store_0.ra!1)) (= GPR!3 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_19!1 GPR!2 GPR!1)) (= op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!4 (ite op_0_instruction.operation.store_general_0.powerpc_store_0.action.block_19!1 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!3 op_0_instruction.operation.store_general_0.powerpc_store_0.ra.tmp_1!2))) (= op_0_instruction.action.block_1!1 (= BRANCH!2 #b1)) (= op_0_instruction.action.block_2!1 (not (or op_0_instruction.action.block_1!1))) (or (and op_0_instruction.action.block_1!1 (= CIA!2 NEXTPC!2) (= op_0_instruction.address.0!2 CIA!2)) (and op_0_instruction.action.block_2!1 (= CIA!3 (bvadd CIA!1 #b0000000000000000000000000000000000000000000000000000000000000100)) (= op_0_instruction.address.0!3 CIA!3))) (and (= op_0_instruction.address.0!4 (ite op_0_instruction.action.block_2!1 op_0_instruction.address.0!3 (ite op_0_instruction.action.block_1!1 op_0_instruction.address.0!2 op_0_instruction.address.0!3))) (= CIA!4 (ite op_0_instruction.action.block_2!1 CIA!3 (ite op_0_instruction.action.block_1!1 CIA!2 CIA!3)))))) (assert (= op_1_instruction.operation.ra.i!1 #b00011)) (assert (= op_1_instruction.operation.rs.i!1 #b00011)) (assert (= op_1_instruction.operation.rb.i!1 #b00011)) (assert (and (= BRANCH!3 #b0) (= NEXTPC!3 #b0000000000000000000000000000000000000000000000000000000000000000) (= Rc!2 #b0) (= op_1_instruction.operation.xor_general_0.Rc_op!1 Rc!2) (= op_1_instruction.operation.xor_general_0.ra.i!1 op_1_instruction.operation.ra.i!1) (= op_1_instruction.operation.xor_general_0.ra!1 op_1_instruction.operation.ra!1) (= op_1_instruction.operation.xor_general_0.rs.i!1 op_1_instruction.operation.rs.i!1) (= op_1_instruction.operation.xor_general_0.rs!1 op_1_instruction.operation.rs!1) (= op_1_instruction.operation.xor_general_0.rb.i!1 op_1_instruction.operation.rb.i!1) (= op_1_instruction.operation.xor_general_0.rb!1 op_1_instruction.operation.rb!1) (= XO_10!2 #b0100111100) (= OPCD!3 #b011111) (= GPR!4 (store GPR!3 op_1_instruction.operation.xor_general_0.ra.i!1 op_1_instruction.operation.xor_general_0.ra.tmp_1!2)) (= op_1_instruction.operation.xor_general_0.ra.write.index.2!2 op_1_instruction.operation.xor_general_0.ra.i!1) (= op_1_instruction.operation.xor_general_0.ra.write.value.2!2 op_1_instruction.operation.xor_general_0.ra.tmp_1!2) (= op_1_instruction.operation.xor_general_0.ra.tmp_1!2 __tmp_23!1) (= op_1_instruction.operation.xor_general_0.ra!2 __tmp_23!1) (= op_1_instruction.operation.xor_general_0.rs.read.index.0!2 op_1_instruction.operation.xor_general_0.rs.i!1) (= op_1_instruction.operation.xor_general_0.rs.read.value.0!2 (select GPR!3 op_1_instruction.operation.xor_general_0.rs.i!1)) (= (select GPR!3 op_1_instruction.operation.xor_general_0.rs.i!1) __tmp_24!1) (= op_1_instruction.operation.xor_general_0.rs!1 __tmp_24!1) (= op_1_instruction.operation.xor_general_0.rb.read.index.0!2 op_1_instruction.operation.xor_general_0.rb.i!1) (= op_1_instruction.operation.xor_general_0.rb.read.value.0!2 (select GPR!3 op_1_instruction.operation.xor_general_0.rb.i!1)) (= (select GPR!3 op_1_instruction.operation.xor_general_0.rb.i!1) __tmp_25!1) (= op_1_instruction.operation.xor_general_0.rb!1 __tmp_25!1) (= __tmp_23!1 (bvxor __tmp_24!1 __tmp_25!1)) (= op_1_instruction.operation.xor_general_0.action.block_0!1 (= op_1_instruction.operation.xor_general_0.Rc_op!1 #b1)) (or (and op_1_instruction.operation.xor_general_0.action.block_0!1 (= op_1_instruction.operation.xor_general_0.ra.read.index.0!2 op_1_instruction.operation.xor_general_0.ra.i!1) (= op_1_instruction.operation.xor_general_0.ra.read.value.0!2 (select GPR!4 op_1_instruction.operation.xor_general_0.ra.i!1)) (= (select GPR!4 op_1_instruction.operation.xor_general_0.ra.i!1) __tmp_26!1) (= op_1_instruction.operation.xor_general_0.ra!2 __tmp_26!1) (= op_1_instruction.operation.xor_general_0.ra.read.index.0!2 op_1_instruction.operation.xor_general_0.ra.i!1) (= op_1_instruction.operation.xor_general_0.ra.read.value.0!2 (select GPR!4 op_1_instruction.operation.xor_general_0.ra.i!1)) (= (select GPR!4 op_1_instruction.operation.xor_general_0.ra.i!1) __tmp_27!1) (= op_1_instruction.operation.xor_general_0.ra!2 __tmp_27!1) (= op_1_instruction.operation.xor_general_0.action.block_3!1 (= __tmp_26!1 #b00000000000000000000000000000000)) (= op_1_instruction.operation.xor_general_0.action.block_4!1 (and (not (or op_1_instruction.operation.xor_general_0.action.block_3!1)) (= ((_ extract 31 31) __tmp_27!1) #b1))) (= op_1_instruction.operation.xor_general_0.action.block_5!1 (not (or op_1_instruction.operation.xor_general_0.action.block_3!1 op_1_instruction.operation.xor_general_0.action.block_4!1))) (or (and op_1_instruction.operation.xor_general_0.action.block_3!1 (= ((_ extract 31 4) CR!2) ((_ extract 31 4) CR!1)) (= ((_ extract 3 0) CR!2) ((_ zero_extend 3) #b1))) (and op_1_instruction.operation.xor_general_0.action.block_4!1 (= ((_ extract 31 4) CR!3) ((_ extract 31 4) CR!1)) (= ((_ extract 3 0) CR!3) ((_ zero_extend 3) #b1))) (and op_1_instruction.operation.xor_general_0.action.block_5!1 (= ((_ extract 31 4) CR!4) ((_ extract 31 4) CR!1)) (= ((_ extract 3 0) CR!4) ((_ zero_extend 3) #b1)))) (and (= CR!5 (ite op_1_instruction.operation.xor_general_0.action.block_5!1 CR!4 (ite op_1_instruction.operation.xor_general_0.action.block_4!1 CR!3 (ite op_1_instruction.operation.xor_general_0.action.block_3!1 CR!2 CR!4))))) (= op_1_instruction.operation.xor_general_0.read.index.0!2 1) (= op_1_instruction.operation.xor_general_0.read.value.0!2 (select SPR!1 #b0000000001)) (= ((_ extract 31 4) CR!6) ((_ extract 31 4) CR!1)) (= ((_ zero_extend 60) ((_ extract 3 0) CR!6)) (select SPR!1 #b0000000001))) (and (not (or op_1_instruction.operation.xor_general_0.action.block_0!1)))) (= op_1_instruction.action.block_1!1 (= BRANCH!3 #b1)) (= op_1_instruction.action.block_2!1 (not (or op_1_instruction.action.block_1!1))) (or (and op_1_instruction.action.block_1!1 (= CIA!5 NEXTPC!3) (= op_1_instruction.address.0!2 CIA!5)) (and op_1_instruction.action.block_2!1 (= CIA!6 (bvadd CIA!4 #b0000000000000000000000000000000000000000000000000000000000000100)) (= op_1_instruction.address.0!3 CIA!6))) (and (= op_1_instruction.address.0!4 (ite op_1_instruction.action.block_2!1 op_1_instruction.address.0!3 (ite op_1_instruction.action.block_1!1 op_1_instruction.address.0!2 op_1_instruction.address.0!3))) (= CIA!7 (ite op_1_instruction.action.block_2!1 CIA!6 (ite op_1_instruction.action.block_1!1 CIA!5 CIA!4)))))) (assert (= op_2_instruction.operation.rd.i!1 #b00011)) (assert (= op_2_instruction.operation.D!1 #b1111111111101000)) (assert (= op_2_instruction.operation.ra.i!1 #b00001)) (assert (and (= BRANCH!4 #b0) (= NEXTPC!4 #b0000000000000000000000000000000000000000000000000000000000000000) (= OPCD!4 #b100000) (= upd_flag_mmu!3 #b0) (= op_2_instruction.operation.load_general_0.rd.i!1 op_2_instruction.operation.rd.i!1) (= op_2_instruction.operation.load_general_0.rd!1 op_2_instruction.operation.rd!1) (= op_2_instruction.operation.load_general_0.D!1 op_2_instruction.operation.D!1) (= op_2_instruction.operation.load_general_0.ra.i!1 op_2_instruction.operation.ra.i!1) (= op_2_instruction.operation.load_general_0.ra!1 op_2_instruction.operation.ra!1) (= op_2_instruction.operation.load_general_0.upd!1 upd_flag_mmu!3) (= op_2_instruction.operation.load_general_0.byte_num!1 #b100) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 op_2_instruction.operation.load_general_0.rd.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!1 op_2_instruction.operation.load_general_0.rd!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.D!1 ((_ sign_extend 16) op_2_instruction.operation.load_general_0.D!1)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1 op_2_instruction.operation.load_general_0.ra.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra!1 op_2_instruction.operation.load_general_0.ra!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.upd!1 op_2_instruction.operation.load_general_0.upd!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.byte_num!1 op_2_instruction.operation.load_general_0.byte_num!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_0!1 (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1 #b00000)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_1!1 (not (or op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_0!1))) (or (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_0!1 (= temp!5 #b00000000000000000000000000000000)) (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_1!1 (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra.read.index.0!2 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra.read.value.0!2 (select GPR!4 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1)) (= (select GPR!4 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1) __tmp_28!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra!1 __tmp_28!1) (= temp!6 __tmp_28!1))) (and (= temp!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_1!1 temp!6 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_0!1 temp!5 temp!4)))) (= temp1!3 (bvadd temp!7 op_2_instruction.operation.load_general_0.powerpc_load_0.D!1)) (= temp_address!3 ((_ extract 28 0) (bvlshr temp1!3 #b00000000000000000000000000000011))) (= ((_ extract 2 0) temp_lo_index!3) ((_ extract 2 0) temp1!3)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!2 temp_address!3) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!2 (select MEM!16 temp_address!3)) (= temp64!21 (select MEM!16 temp_address!3)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 (= op_2_instruction.operation.load_general_0.powerpc_load_0.byte_num!1 #b001)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 (and (not (or op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.byte_num!1 #b010))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 (and (not (or op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.byte_num!1 #b100))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_6!1 (not (or op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1))) (or (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 (= GPR!5 (store GPR!4 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!2)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!2 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!2 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!2) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!2 __tmp_29!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!2 __tmp_29!1) (= ((_ zero_extend 1) __tmp_29!1) ((_ zero_extend 24) ((_ extract 8 0) (bvlshr temp64!21 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!3))))))))) (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 (= temp_lo_index!3 #b111)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 (not (or op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1))) (or (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 (= GPR!6 (store GPR!5 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!3)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!3 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!3 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!3) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!3 __tmp_30!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!3 __tmp_30!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!3 (bvadd temp_address!3 #b00000000000000000000000000001)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!3 (select MEM!16 (bvadd temp_address!3 #b00000000000000000000000000001))) (= temp64_0!15 (select MEM!16 (bvadd temp_address!3 #b00000000000000000000000000001))) (= __tmp_30!1 ((_ zero_extend 16) (concat ((_ extract 7 0) temp64_0!15) ((_ extract 63 56) temp64!21))))) (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 (= GPR!7 (store GPR!5 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!4)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!4 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!4 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!4) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!4 __tmp_31!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!4 __tmp_31!1) (= __tmp_31!1 ((_ zero_extend 16) (concat ((_ extract 7 0) (bvlshr temp64!21 ((_ zero_extend 58) (bvadd #b001000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!3)))))) ((_ extract 7 0) (bvlshr temp64!21 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!3))))))))))) (and (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!4 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!3 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!2))) (= temp64_0!16 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 temp64_0!15 temp64_0!14)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!4 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!3 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!2))) (= GPR!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 GPR!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 GPR!6 GPR!5))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!4 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!3 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!2))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!4 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!3 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!2))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!4 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!3 op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!2)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_10!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!4 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!3 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!2))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!4 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_9!1 op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!3 op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!2)))) (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 (bvugt temp_lo_index!3 #b100)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 (not (or op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1))) (or (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 (= GPR!9 (store GPR!4 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!6)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!6 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!6 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!6) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!6 __tmp_32!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!6 __tmp_32!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!5 (bvadd temp_address!3 #b00000000000000000000000000001)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!5 (select MEM!16 (bvadd temp_address!3 #b00000000000000000000000000001))) (= temp64_0!17 (select MEM!16 (bvadd temp_address!3 #b00000000000000000000000000001))) (= temp2!2 #b00000000000000000000000000000000) (= temp2!3 ((_ extract 31 0) (bvlshr temp64!21 ((_ zero_extend 58) (bvmul ((_ zero_extend 3) temp_lo_index!3) #b001000))))) (= temp0!2 #b00000000000000000000000000000000) (= temp0!3 ((_ extract 31 0) (bvlshr (bvshl temp64_0!17 ((_ zero_extend 58) (bvadd #b100000 (bvmul (bvsub #b001000 ((_ zero_extend 3) temp_lo_index!3)) #b001000)))) ((_ zero_extend 58) (bvadd #b100000 (bvmul (bvsub #b001000 ((_ zero_extend 3) temp_lo_index!3)) #b001000)))))) (= temp2!4 (bvor temp2!3 (bvshl temp0!3 ((_ zero_extend 26) (bvmul (bvsub #b001000 ((_ zero_extend 3) temp_lo_index!3)) #b001000))))) (= __tmp_32!1 (concat ((_ extract 31 24) temp2!4) ((_ extract 23 16) temp2!4) ((_ extract 15 8) temp2!4) ((_ extract 7 0) temp2!4)))) (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 (= GPR!10 (store GPR!4 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!7)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!7 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!7 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!7) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!7 __tmp_33!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!7 __tmp_33!1) (= __tmp_33!1 (concat ((_ extract 7 0) (bvlshr temp64!21 ((_ zero_extend 58) (bvadd #b011000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!3)))))) ((_ extract 7 0) (bvlshr temp64!21 ((_ zero_extend 58) (bvadd #b010000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!3)))))) ((_ extract 7 0) (bvlshr temp64!21 ((_ zero_extend 58) (bvadd #b001000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!3)))))) ((_ extract 7 0) (bvlshr temp64!21 ((_ zero_extend 58) (bvadd #b000000 (bvmul #b001000 ((_ zero_extend 3) temp_lo_index!3)))))))))) (and (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!6 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!5))) (= temp64_0!18 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 temp64_0!17 temp64_0!16)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!6 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!5))) (= GPR!11 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 GPR!10 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 GPR!9 GPR!8))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!6 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!5))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!6 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!5))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!6 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!5 op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!4)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_13!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!6 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!5))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!6 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_12!1 op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!5 op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!4)))) (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_6!1)) (and (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!9 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!2 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.value.2!8)))) (= temp64_0!19 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 temp64_0!18 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 temp64_0!16 temp64_0!14))) (= GPR!12 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 GPR!11 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 GPR!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 GPR!5 GPR!4)))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!6 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!4 op_2_instruction.operation.load_general_0.powerpc_load_0.read.index.0!2))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd!9 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!2 op_2_instruction.operation.load_general_0.powerpc_load_0.rd!1)))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!9 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!2 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_1!8)))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!9 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!2 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.tmp_0!8)))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!7 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!6 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!4 op_2_instruction.operation.load_general_0.powerpc_load_0.read.value.0!2))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!9 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_5!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!8 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_4!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!5 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_3!1 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!2 op_2_instruction.operation.load_general_0.powerpc_load_0.rd.write.index.2!8))))) (= op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_15!1 (and (= op_2_instruction.operation.load_general_0.powerpc_load_0.upd!1 #b1) (distinct op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1 #b00000))) (or (and op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_15!1 (= GPR!13 (store GPR!12 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!3)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra.write.index.2!2 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.i!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra.write.value.2!2 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!3) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!3 __tmp_34!1) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra!2 __tmp_34!1) (= __tmp_34!1 temp1!3)) (and (not (or op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_15!1)))) (and (= GPR!14 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_15!1 GPR!13 GPR!12)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra!3 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_15!1 op_2_instruction.operation.load_general_0.powerpc_load_0.ra!2 op_2_instruction.operation.load_general_0.powerpc_load_0.ra!1)) (= op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!4 (ite op_2_instruction.operation.load_general_0.powerpc_load_0.action.block_15!1 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!3 op_2_instruction.operation.load_general_0.powerpc_load_0.ra.tmp_1!2))) (= op_2_instruction.action.block_1!1 (= BRANCH!4 #b1)) (= op_2_instruction.action.block_2!1 (not (or op_2_instruction.action.block_1!1))) (or (and op_2_instruction.action.block_1!1 (= CIA!8 NEXTPC!4) (= op_2_instruction.address.0!2 CIA!8)) (and op_2_instruction.action.block_2!1 (= CIA!9 (bvadd CIA!7 #b0000000000000000000000000000000000000000000000000000000000000100)) (= op_2_instruction.address.0!3 CIA!9))) (and (= CIA!10 (ite op_2_instruction.action.block_2!1 CIA!9 (ite op_2_instruction.action.block_1!1 CIA!8 CIA!7))) (= op_2_instruction.address.0!4 (ite op_2_instruction.action.block_2!1 op_2_instruction.address.0!3 (ite op_2_instruction.action.block_1!1 op_2_instruction.address.0!2 op_2_instruction.address.0!3)))))) ;;set entry point to 0 (assert (= CIA!1 #b0000000000000000000000000000000000000000000000000000000000000000)) (assert (= (select GPR!1 (_ bv1 5)) (_ bv4096 32))) (declare-const arg (_ BitVec 32)) (assert (= arg (select GPR!1 (_ bv3 5)))) (assert (= arg #x12345678)) (declare-const res (_ BitVec 32)) (assert (= res (select GPR!14 (_ bv3 5)))) (assert (not (= res #x12345678))) ;unsat (check-sat) (get-model) (exit)