From 839d8098210e7239fa0d8c39d410452b3bde79e6 Mon Sep 17 00:00:00 2001 From: Rot127 Date: Thu, 7 Sep 2023 13:41:06 -0500 Subject: [PATCH] Fix incorrect tests with missing writeback due to missing post-index flag --- test/db/asm/arm_32 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/db/asm/arm_32 b/test/db/asm/arm_32 index b3e554fbed0..3aec5cc31a9 100644 --- a/test/db/asm/arm_32 +++ b/test/db/asm/arm_32 @@ -769,7 +769,7 @@ d "vzip.16 d2, d3" 8321b6f3 0x0 (seq (set d2 (cast 64 false (| (| (| (| (bv 128 d "vuzp.8 d0, d1" 0101b2f3 0x0 (seq (set d0 (| (| (| (| (bv 64 0x0) (| (<< (cast 64 false (cast 8 false (>> (var d0) (bv 8 0x0) false))) (bv 8 0x0) false) (<< (<< (cast 64 false (cast 8 false (>> (var d1) (bv 8 0x0) false))) (bv 8 0x0) false) (bv 8 0x20) false))) (| (<< (cast 64 false (cast 8 false (>> (var d0) (bv 8 0x10) false))) (bv 8 0x8) false) (<< (<< (cast 64 false (cast 8 false (>> (var d1) (bv 8 0x10) false))) (bv 8 0x8) false) (bv 8 0x20) false))) (| (<< (cast 64 false (cast 8 false (>> (var d0) (bv 8 0x20) false))) (bv 8 0x10) false) (<< (<< (cast 64 false (cast 8 false (>> (var d1) (bv 8 0x20) false))) (bv 8 0x10) false) (bv 8 0x20) false))) (| (<< (cast 64 false (cast 8 false (>> (var d0) (bv 8 0x30) false))) (bv 8 0x18) false) (<< (<< (cast 64 false (cast 8 false (>> (var d1) (bv 8 0x30) false))) (bv 8 0x18) false) (bv 8 0x20) false)))) (set d1 (| (| (| (| (bv 64 0x0) (| (<< (cast 64 false (cast 8 false (>> (var d0) (bv 8 0x8) false))) (bv 8 0x0) false) (<< (<< (cast 64 false (cast 8 false (>> (var d1) (bv 8 0x8) false))) (bv 8 0x0) false) (bv 8 0x20) false))) (| (<< (cast 64 false (cast 8 false (>> (var d0) (bv 8 0x18) false))) (bv 8 0x8) false) (<< (<< (cast 64 false (cast 8 false (>> (var d1) (bv 8 0x18) false))) (bv 8 0x8) false) (bv 8 0x20) false))) (| (<< (cast 64 false (cast 8 false (>> (var d0) (bv 8 0x28) false))) (bv 8 0x10) false) (<< (<< (cast 64 false (cast 8 false (>> (var d1) (bv 8 0x28) false))) (bv 8 0x10) false) (bv 8 0x20) false))) (| (<< (cast 64 false (cast 8 false (>> (var d0) (bv 8 0x38) false))) (bv 8 0x18) false) (<< (<< (cast 64 false (cast 8 false (>> (var d1) (bv 8 0x38) false))) (bv 8 0x18) false) (bv 8 0x20) false))))) d "vuzp.8 q0, q1" 4201b2f3 0x0 (seq (set d0 (cast 64 false (| (| (| (| (| (| (| (| (bv 128 0x0) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x0) false))) (bv 8 0x0) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x0) false))) (bv 8 0x0) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x10) false))) (bv 8 0x8) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x10) false))) (bv 8 0x8) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x20) false))) (bv 8 0x10) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x20) false))) (bv 8 0x10) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x30) false))) (bv 8 0x18) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x30) false))) (bv 8 0x18) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x40) false))) (bv 8 0x20) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x40) false))) (bv 8 0x20) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x50) false))) (bv 8 0x28) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x50) false))) (bv 8 0x28) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x60) false))) (bv 8 0x30) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x60) false))) (bv 8 0x30) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x70) false))) (bv 8 0x38) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x70) false))) (bv 8 0x38) false) (bv 8 0x40) false))))) (set d1 (cast 64 false (>> (| (| (| (| (| (| (| (| (bv 128 0x0) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x0) false))) (bv 8 0x0) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x0) false))) (bv 8 0x0) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x10) false))) (bv 8 0x8) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x10) false))) (bv 8 0x8) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x20) false))) (bv 8 0x10) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x20) false))) (bv 8 0x10) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x30) false))) (bv 8 0x18) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x30) false))) (bv 8 0x18) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x40) false))) (bv 8 0x20) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x40) false))) (bv 8 0x20) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x50) false))) (bv 8 0x28) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x50) false))) (bv 8 0x28) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x60) false))) (bv 8 0x30) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x60) false))) (bv 8 0x30) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x70) false))) (bv 8 0x38) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x70) false))) (bv 8 0x38) false) (bv 8 0x40) false))) (bv 8 0x40) false))) (set d2 (cast 64 false (| (| (| (| (| (| (| (| (bv 128 0x0) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x8) false))) (bv 8 0x0) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x8) false))) (bv 8 0x0) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x18) false))) (bv 8 0x8) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x18) false))) (bv 8 0x8) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x28) false))) (bv 8 0x10) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x28) false))) (bv 8 0x10) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x38) false))) (bv 8 0x18) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x38) false))) (bv 8 0x18) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x48) false))) (bv 8 0x20) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x48) false))) (bv 8 0x20) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x58) false))) (bv 8 0x28) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x58) false))) (bv 8 0x28) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x68) false))) (bv 8 0x30) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x68) false))) (bv 8 0x30) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x78) false))) (bv 8 0x38) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x78) false))) (bv 8 0x38) false) (bv 8 0x40) false))))) (set d3 (cast 64 false (>> (| (| (| (| (| (| (| (| (bv 128 0x0) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x8) false))) (bv 8 0x0) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x8) false))) (bv 8 0x0) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x18) false))) (bv 8 0x8) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x18) false))) (bv 8 0x8) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x28) false))) (bv 8 0x10) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x28) false))) (bv 8 0x10) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x38) false))) (bv 8 0x18) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x38) false))) (bv 8 0x18) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x48) false))) (bv 8 0x20) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x48) false))) (bv 8 0x20) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x58) false))) (bv 8 0x28) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x58) false))) (bv 8 0x28) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x68) false))) (bv 8 0x30) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x68) false))) (bv 8 0x30) false) (bv 8 0x40) false))) (| (<< (cast 128 false (cast 8 false (>> (append (var d1) (var d0)) (bv 8 0x78) false))) (bv 8 0x38) false) (<< (<< (cast 128 false (cast 8 false (>> (append (var d3) (var d2)) (bv 8 0x78) false))) (bv 8 0x38) false) (bv 8 0x40) false))) (bv 8 0x40) false)))) d "vuzp.16 d2, d4" 0421b6f3 0x0 (seq (set d2 (| (| (bv 64 0x0) (| (<< (cast 64 false (cast 16 false (>> (var d2) (bv 8 0x0) false))) (bv 8 0x0) false) (<< (<< (cast 64 false (cast 16 false (>> (var d4) (bv 8 0x0) false))) (bv 8 0x0) false) (bv 8 0x20) false))) (| (<< (cast 64 false (cast 16 false (>> (var d2) (bv 8 0x20) false))) (bv 8 0x10) false) (<< (<< (cast 64 false (cast 16 false (>> (var d4) (bv 8 0x20) false))) (bv 8 0x10) false) (bv 8 0x20) false)))) (set d4 (| (| (bv 64 0x0) (| (<< (cast 64 false (cast 16 false (>> (var d2) (bv 8 0x10) false))) (bv 8 0x0) false) (<< (<< (cast 64 false (cast 16 false (>> (var d4) (bv 8 0x10) false))) (bv 8 0x0) false) (bv 8 0x20) false))) (| (<< (cast 64 false (cast 16 false (>> (var d2) (bv 8 0x30) false))) (bv 8 0x10) false) (<< (<< (cast 64 false (cast 16 false (>> (var d4) (bv 8 0x30) false))) (bv 8 0x10) false) (bv 8 0x20) false))))) -d "vld1.8 {d0}, [r1], r0" 000721f4 0x0 (seq empty (set d0 (<< (cast 64 false (loadw 0 8 (var r1))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (var r1) (bv 32 0x1)))) (bv 8 0x8) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) empty) +d "vld1.8 {d0}, [r1], r0" 000721f4 0x0 (seq empty (set d0 (<< (cast 64 false (loadw 0 8 (var r1))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (var r1) (bv 32 0x1)))) (bv 8 0x8) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) (set r1 (+ (var r1) (var r0)))) d "vld1.16 {d1}, [r7]!" 4d1727f4 0x0 (seq empty (set d1 (<< (cast 64 false (loadw 0 16 (var r7))) (bv 8 0x0) false)) (set d1 (<< (cast 64 false (loadw 0 16 (+ (var r7) (bv 32 0x2)))) (bv 8 0x10) false)) (set d1 (<< (cast 64 false (loadw 0 16 (+ (+ (var r7) (bv 32 0x2)) (bv 32 0x2)))) (bv 8 0x20) false)) (set d1 (<< (cast 64 false (loadw 0 16 (+ (+ (+ (var r7) (bv 32 0x2)) (bv 32 0x2)) (bv 32 0x2)))) (bv 8 0x30) false)) (set r7 (+ (var r7) (bv 32 0x8)))) d "vld1.16 {d1}, [r7]" 4f1727f4 0x0 (seq empty (set d1 (<< (cast 64 false (loadw 0 16 (var r7))) (bv 8 0x0) false)) (set d1 (<< (cast 64 false (loadw 0 16 (+ (var r7) (bv 32 0x2)))) (bv 8 0x10) false)) (set d1 (<< (cast 64 false (loadw 0 16 (+ (+ (var r7) (bv 32 0x2)) (bv 32 0x2)))) (bv 8 0x20) false)) (set d1 (<< (cast 64 false (loadw 0 16 (+ (+ (+ (var r7) (bv 32 0x2)) (bv 32 0x2)) (bv 32 0x2)))) (bv 8 0x30) false)) empty) d "vld1.32 {d1}, [r7]" 8f1727f4 0x0 (seq empty (set d1 (<< (cast 64 false (loadw 0 32 (var r7))) (bv 8 0x0) false)) (set d1 (<< (cast 64 false (loadw 0 32 (+ (var r7) (bv 32 0x4)))) (bv 8 0x20) false)) empty) @@ -786,7 +786,7 @@ d "vld1.8 {d0, d1, d2}, [r0]" 0f0620f4 0x0 (seq empty (set d0 (<< (cast 64 false d "vld2.8 {d0, d2}, [r0]" 0f0920f4 0x0 (seq empty (set d0 (<< (cast 64 false (loadw 0 8 (var r0))) (bv 8 0x0) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (var r0) (bv 32 0x1)))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) empty) d "vld3.8 {d0, d1, d2}, [r0]" 0f0420f4 0x0 (seq empty (set d0 (<< (cast 64 false (loadw 0 8 (var r0))) (bv 8 0x0) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (var r0) (bv 32 0x1)))) (bv 8 0x0) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) empty) d "vld4.8 {d0, d1, d2, d3}, [r0]" 0f0020f4 0x0 (seq empty (set d0 (<< (cast 64 false (loadw 0 8 (var r0))) (bv 8 0x0) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (var r0) (bv 32 0x1)))) (bv 8 0x0) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x0) false)) (set d3 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d3 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x8) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d3 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d3 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x18) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d3 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d3 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x28) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d3 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x30) false)) (set d0 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) (set d1 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) (set d2 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) (set d3 (<< (cast 64 false (loadw 0 8 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (var r0) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)))) (bv 8 0x38) false)) empty) -d "vst1.8 {d0}, [r1], r0" 000701f4 0x0 (seq empty (storew 0 (var r1) (cast 8 false (>> (var d0) (bv 8 0x0) false))) (storew 0 (+ (var r1) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x8) false))) (storew 0 (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x10) false))) (storew 0 (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x18) false))) (storew 0 (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x20) false))) (storew 0 (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x28) false))) (storew 0 (+ (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x30) false))) (storew 0 (+ (+ (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x38) false))) empty) +d "vst1.8 {d0}, [r1], r0" 000701f4 0x0 (seq empty (storew 0 (var r1) (cast 8 false (>> (var d0) (bv 8 0x0) false))) (storew 0 (+ (var r1) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x8) false))) (storew 0 (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x10) false))) (storew 0 (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x18) false))) (storew 0 (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x20) false))) (storew 0 (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x28) false))) (storew 0 (+ (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x30) false))) (storew 0 (+ (+ (+ (+ (+ (+ (+ (var r1) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (bv 32 0x1)) (cast 8 false (>> (var d0) (bv 8 0x38) false))) (set r1 (+ (var r1) (var r0)))) d "vst1.16 {d1}, [r7]!" 4d1707f4 0x0 (seq empty (storew 0 (var r7) (cast 16 false (>> (var d1) (bv 8 0x0) false))) (storew 0 (+ (var r7) (bv 32 0x2)) (cast 16 false (>> (var d1) (bv 8 0x10) false))) (storew 0 (+ (+ (var r7) (bv 32 0x2)) (bv 32 0x2)) (cast 16 false (>> (var d1) (bv 8 0x20) false))) (storew 0 (+ (+ (+ (var r7) (bv 32 0x2)) (bv 32 0x2)) (bv 32 0x2)) (cast 16 false (>> (var d1) (bv 8 0x30) false))) (set r7 (+ (var r7) (bv 32 0x8)))) d "vst1.16 {d1}, [r7]" 4f1707f4 0x0 (seq empty (storew 0 (var r7) (cast 16 false (>> (var d1) (bv 8 0x0) false))) (storew 0 (+ (var r7) (bv 32 0x2)) (cast 16 false (>> (var d1) (bv 8 0x10) false))) (storew 0 (+ (+ (var r7) (bv 32 0x2)) (bv 32 0x2)) (cast 16 false (>> (var d1) (bv 8 0x20) false))) (storew 0 (+ (+ (+ (var r7) (bv 32 0x2)) (bv 32 0x2)) (bv 32 0x2)) (cast 16 false (>> (var d1) (bv 8 0x30) false))) empty) d "vst1.32 {d1}, [r7]" 8f1707f4 0x0 (seq empty (storew 0 (var r7) (cast 32 false (>> (var d1) (bv 8 0x0) false))) (storew 0 (+ (var r7) (bv 32 0x4)) (cast 32 false (>> (var d1) (bv 8 0x20) false))) empty)