Sub:
00000556: sub sum(sum_result)
0000056b: sum_result :: out u32 = RAX

00000192:
00000194: #34 := RBP
00000196: RSP := RSP - 8
00000198: mem := mem with [RSP, el]:u64 <- #34
0000019c: RBP := RSP
000001a0: RAX := pad:64[low:32[RDI]]
000001a4: mem := mem with [RBP - 0x20, el]:u64 <- RSI
000001a8: mem := mem with [RBP - 0x14] <- low:8[RAX]
000001ac: mem := mem with [RBP - 2] <- 0
000001b0: mem := mem with [RBP - 1] <- 0
000001b5: goto %000001b3

000001b3:
000001b8: RAX := pad:64[pad:32[mem[RBP - 2]]]
000001be: CF := low:8[RAX] < mem[RBP - 0x14]
000001cd: when CF goto %000001cb
00000557: goto %00000210

00000210:
00000212: RAX := pad:64[pad:32[mem[RBP - 1]]]
00000216: RBP := mem[RSP, el]:u64
00000218: RSP := RSP + 8
0000021c: #43 := mem[RSP, el]:u64
0000021e: RSP := RSP + 8
00000220: call #43 with noreturn

000001cb:
000001d2: RAX := pad:64[pad:32[mem[RBP - 2]]]
000001d6: RDX := pad:64[low:32[RAX + 1]]
000001da: mem := mem with [RBP - 2] <- low:8[RDX]
000001de: RDX := pad:64[pad:32[low:8[RAX]]]
000001e2: RAX := mem[RBP - 0x20, el]:u64
000001e8: #38 := RDX
000001ea: RAX := RAX + #38
000001fa: RAX := pad:64[pad:32[mem[RAX]]]
00000200: #41 := low:8[RAX]
00000202: mem := mem with [RBP - 1] <- mem[RBP - 1] + #41
00000558: goto %000001b3

Evaluating precondition.
Checking precondition with Z3.

SAT!

Model:
	YMM9  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM8  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM7  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM6  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM5  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM4  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM3  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM2  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM15 |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM14 |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM13 |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM12 |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM11 |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM10 |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM1  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	YMM0  |->  0x0000000000000000000000000000000000000000000000000000000000000000
	ST7   |->  0x00000000000000000000
	ST6   |->  0x00000000000000000000
	ST5   |->  0x00000000000000000000
	ST4   |->  0x00000000000000000000
	ST3   |->  0x00000000000000000000
	ST2   |->  0x00000000000000000000
	ST1   |->  0x00000000000000000000
	ST0   |->  0x00000000000000000000
	SS    |->  0x0000
	RSP   |->  0x000000003f800200
	RSI   |->  0x4000000000000000
	RDX   |->  0x0000000000000000
	RDI   |->  0x0000000000000001
	RCX   |->  0x0000000000000000
	RBX   |->  0x0000000000000000
	RBP   |->  0x0000000000000000
	RAX   |->  0x0000000000000000
	R9    |->  0x0000000000000000
	R8    |->  0x0000000000000000
	R15   |->  0x0000000000000000
	R14   |->  0x0000000000000000
	R13   |->  0x0000000000000000
	R12   |->  0x0000000000000000
	R11   |->  0x0000000000000000
	R10   |->  0x0000000000000000
	MM7   |->  0x0000000000000000
	MM6   |->  0x0000000000000000
	MM5   |->  0x0000000000000000
	MM4   |->  0x0000000000000000
	MM3   |->  0x0000000000000000
	MM2   |->  0x0000000000000000
	MM1   |->  0x0000000000000000
	MM0   |->  0x0000000000000000
	ES    |->  0x0000
	DS    |->  0x0000
	CS    |->  0x0000
	CF    |->  0x0
	mem_orig |-> [
		#x4000000000000000 |-> 0x01 ;
		else |-> 0x00]
	mem_mod = mem_orig
	loop_mem023 |-> [
		#x0000000000000000 |-> 0xc0 ;
		#x000000003f8001e4 |-> 0x02 ;
		#x000000003f8001f7 |-> 0x80 ;
		else |-> 0x00]
	loop_RDX025   |->  
0x0000000000000000
	loop_RAX024   |->  0x0000000000000000
	loop_CF022    |->  0x0
	|loop_#41021| |->  0x00
	|loop_#38020| |->  0x0000000000000000

(declare-fun sum_array ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 8))  else -> (ite (bvule (:var 1) (:var 0))
     #x00
     (bvadd (select mem0 (:var 0))
            ((_ sum_array 0) (bvadd #x0000000000000001 (:var 0)) (:var 1))))]
(declare-fun const_array ((_ BitVec 64) (_ BitVec 64)) Bool)  else -> (ite (bvule (:var 1) (:var 0))
     true
     (and (= (select mem0 (:var 0)) (select init_mem0 (:var 0)))
          ((_ const_array 0) (bvadd #x0000000000000001 (:var 0)) (:var 1))))]


Refuted goals: