search

illera88 / Ponce

IDA 2016 plugin contest winner! Symbolic Execution just one-click away!
https://docs.idaponce.com
Other
1.48k stars 72 forks source link

i cant do successed Solving formula #96

Closed cbwang505 closed 4 years ago

cbwang505 commented 5 years ago

i compiled the source code below,and i user the parameter "ppppp"" then Symbolized ,but i cant do successed Solving formula ConsoleApplication2.zip

in (!strcmp(argv[1], "jsk")) the code disassemby address ,got the [!] No solution found : in ida output below, how can get the correct argv[1] with "jsk" by Solving formula use ponce?

//

include "stdafx.h"

include "string.h"

void success(){ printf("success\n"); } void failed(){ printf("failed\n"); } void next(char *pwd){ if (!strcmp(pwd, "123456")){ success(); } else{ failed(); } }

int _tmain(int argc, _TCHAR* argv[]) {

printf("please input n\n");
puts("this is puts\n");
if (argc < 2)
{
    failed();
    return 0;
}
if (!strcmp(argv[1], "jsk")){
    success();
}
else{
    failed();
}
return 0;

}

PDBSRC: loading symbols for 'E:\git\vsprj\ConsoleApplication2\x64\Debug\ConsoleApplication2.exe'... PDB: using DIA dll "C:\Program Files\Common Files\Microsoft Shared\VC\msdia90.dll" PDB: DIA interface version 9.0 PDB: using load address 13F330000 [+] Symbolizing memory from 0x3e980b to 0x3e9810. Total: 6 bytes [+] Reanalizyng instruction at 0x13f3310e0 BP Instructions traced: 16 Symbolic instructions: 0 Symbolic conditions: 0 Time: 15 secs BP Instructions traced: 17 Symbolic instructions: 0 Symbolic conditions: 0 Time: 24 secs [!] Instruction symbolized at 0x13f3314e8 [!] Instruction symbolized at 0x13f3314eb [!] Instruction symbolized at 0x13f3314ee [+] Branch symbolized detected at 0x13f3314ee: 0x13f3314f0 or 0x13f33153f, Taken:Yes [!] Instruction symbolized at 0x13f33153f [!] Instruction symbolized at 0x13f331542 [!] Instruction symbolized at 0x13f331147 [!] Instruction symbolized at 0x13f331149 [+] Branch symbolized detected at 0x13f331149: 0x13f33114b or 0x13f331152, Taken:Yes [+] Solving condition at 1 [+] Solving formula... [!] No solution found :(

0ca commented 5 years ago

Could you share the instructions from 0x13f3314e8 to 0x13f331149?

cbwang505 commented 5 years ago

.text:000000013F3310E0 ; int __fastcall T_001_main(int argc, char **argv) .text:000000013F3310E0 T_001_main proc near ; CODE XREF: main_0↑j .text:000000013F3310E0 ; DATA XREF: .pdata:000000013F365024↓o .text:000000013F3310E0 .text:000000013F3310E0 arg_0 = dword ptr 8 .text:000000013F3310E0 arg_8 = qword ptr 10h .text:000000013F3310E0 .text:000000013F3310E0 mov [rsp+arg_8], rdx .text:000000013F3310E5 mov [rsp+arg_0], ecx .text:000000013F3310E9 push rdi .text:000000013F3310EA sub rsp, 20h .text:000000013F3310EE mov rdi, rsp .text:000000013F3310F1 mov ecx, 8 .text:000000013F3310F6 mov eax, 0CCCCCCCCh .text:000000013F3310FB rep stosd .text:000000013F3310FD mov ecx, [rsp+28h+arg_0] .text:000000013F331101 lea rcx, aPleaseInputN ; "please input n\n" .text:000000013F331108 call printf .text:000000013F33110D lea rcx, string ; "this is puts\n" .text:000000013F331114 call puts .text:000000013F331119 cmp [rsp+28h+arg_0], 2 .text:000000013F33111E jge short loc_13F331129 .text:000000013F331120 call failed(void) .text:000000013F331125 xor eax, eax .text:000000013F331127 jmp short loc_13F331159 .text:000000013F331129 ; --------------------------------------------------------------------------- .text:000000013F331129 .text:000000013F331129 loc_13F331129: ; CODE XREF: T_001_main+3E↑j .text:000000013F331129 mov eax, 8 .text:000000013F33112E imul rax, 1 .text:000000013F331132 lea rdx, aJsk ; "jsk" .text:000000013F331139 mov rcx, [rsp+28h+arg_8] .text:000000013F33113E mov rcx, [rcx+rax] ; Str1 .text:000000013F331142 call T_000_strcmp .text:000000013F331147 test eax, eax ; Symbolized regs: eax .text:000000013F331149 jnz short loc_13F331152 ; Symbolized regs: zf .text:000000013F33114B call success(void) .text:000000013F331150 jmp short loc_13F331157 .text:000000013F331152 ; --------------------------------------------------------------------------- .text:000000013F331152 .text:000000013F331152 loc_13F331152: ; CODE XREF: T_001_main+69↑j .text:000000013F331152 call failed(void) .text:000000013F331157 .text:000000013F331157 loc_13F331157: ; CODE XREF: T_001_main+70↑j .text:000000013F331157 xor eax, eax .text:000000013F331159 .text:000000013F331159 loc_13F331159: ; CODE XREF: T_001_main+47↑j .text:000000013F331159 add rsp, 20h .text:000000013F33115D pop rdi .text:000000013F33115E retn .text:000000013F33115E T_001_main endp .text:000000013F33115E

.text:000000013F3314E0 ; int __cdecl T_000_strcmp(const char Str1, const char Str2) .text:000000013F3314E0 T_000_strcmp proc near ; CODE XREF: next(char *)+2A↑p .text:000000013F3314E0 ; T_001_main+62↑p .text:000000013F3314E0 ; DATA XREF: ... .text:000000013F3314E0 sub rdx, rcx .text:000000013F3314E3 test cl, 7 .text:000000013F3314E6 jz short loc_13F3314FC .text:000000013F3314E8 .text:000000013F3314E8 comp_head_loop_begin: ; CODE XREF: T_000_strcmp+1A↓j .text:000000013F3314E8 ; T_000_strcmp+3E↓j ... .text:000000013F3314E8 movzx eax, byte ptr [rcx] ; Symbolized memory: 0x3e980b .text:000000013F3314EB cmp al, [rcx+rdx] ; Symbolized regs: al .text:000000013F3314EE jnz short return_not_equal ; Symbolized regs: zf .text:000000013F3314F0 inc rcx .text:000000013F3314F3 test al, al ; Symbolized regs: al .text:000000013F3314F5 jz short return_equal ; Symbolized regs: zf .text:000000013F3314F7 test cl, 7 .text:000000013F3314FA jnz short comp_head_loop_begin .text:000000013F3314FC .text:000000013F3314FC loc_13F3314FC: ; CODE XREF: T_000_strcmp+6↑j .text:000000013F3314FC mov r11, 8080808080808080h .text:000000013F331506 mov r10, 0FEFEFEFEFEFEFEFFh .text:000000013F331510 .text:000000013F331510 loc_13F331510: ; CODE XREF: T_000_strcmp+5A↓j .text:000000013F331510 lea eax, [ecx+edx] .text:000000013F331514 and eax, 0FFFh .text:000000013F331519 cmp eax, 0FF8h .text:000000013F33151E ja short comp_head_loop_begin .text:000000013F331520 mov rax, [rcx] .text:000000013F331523 cmp rax, [rcx+rdx] .text:000000013F331527 jnz short comp_head_loop_begin .text:000000013F331529 lea r9, [r10+rax] .text:000000013F33152D not rax .text:000000013F331530 add rcx, 8 .text:000000013F331534 and rax, r9 .text:000000013F331537 test r11, rax .text:000000013F33153A jz short loc_13F331510 .text:000000013F33153C .text:000000013F33153C return_equal: ; CODE XREF: T_000_strcmp+15↑j .text:000000013F33153C xor eax, eax ; Symbolized regs: eax .text:000000013F33153E retn .text:000000013F33153F ; --------------------------------------------------------------------------- .text:000000013F33153F .text:000000013F33153F return_not_equal: ; CODE XREF: T_000_strcmp+E↑j .text:000000013F33153F sbb rax, rax ; Symbolized regs: rax cf .text:000000013F331542 or rax, 1 ; Symbolized regs: rax .text:000000013F331546 retn .text:000000013F331546 T_000_strcmp endp

cbwang505 commented 5 years ago

you can reverse my exe in attach with ida to lookup disassemby instruction

mxmssh commented 5 years ago

Confirming this problem:

taintFread: false
only_on_optimization: true
manageSymbolicIndexing: false
addCommentsControlledOperands: true
RenameTaintedFunctionNames: true
addCommentsSymbolicExpresions: true
paintExecutedInstructions: true
color_tainted: 99ffce
color_tainted_execution: e6e6e6
color_tainted_condition: b377
Windbg: using debugging tools from 'C:\Program Files (x86)\Windows Kits\10\Debuggers\x86\'
[+] Notification code: 19 str: dbg_bpt_changed
Rebasing program to 0x000000013FDF1000...
13FDF0000: process C:\Users\max\Desktop\ConsoleApplication2.exe has started (pid=5840)
[+] Notification code: 1 str: dbg_process_start
[+] Starting the debugged process. Reseting all the engines.
[+] Restarting triton engines...
[+] main function found at 0x13fdf100f
[+] Notification code: 19 str: dbg_bpt_changed
77A20000: loaded C:\Windows\system32\ntdll.dll
[+] Notification code: 7 str: dbg_library_load
77800000: loaded C:\Windows\system32\kernel32.dll
[+] Notification code: 7 str: dbg_library_load
7FEFDBF0000: loaded C:\Windows\system32\KernelBase.dll
[+] Notification code: 7 str: dbg_library_load
[+] Notification code: 12 str: dbg_bpt
PDBSRC: loading symbols for 'C:\Users\max\Desktop\ConsoleApplication2.exe'...
PDB: using DIA dll "C:\Program Files\Common Files\Microsoft Shared\VC\msdia90.dll"
PDB: DIA interface version 9.0
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 12 str: dbg_bpt
[+] Notification code: 11 str: dbg_suspend_process
Debugger: process has exited (exit code -1)
[+] Notification code: 2 str: dbg_process_exit
[!] Process_exiting...
Rebasing program to 0x000000013F211000...
13F210000: process C:\Users\max\Desktop\ConsoleApplication2.exe has started (pid=428)
[+] Notification code: 1 str: dbg_process_start
[+] Starting the debugged process. Reseting all the engines.
[+] Restarting triton engines...
[+] main function found at 0x13f21100f
77A20000: loaded C:\Windows\system32\ntdll.dll
[+] Notification code: 7 str: dbg_library_load
77800000: loaded C:\Windows\system32\kernel32.dll
[+] Notification code: 7 str: dbg_library_load
7FEFDBF0000: loaded C:\Windows\system32\KernelBase.dll
[+] Notification code: 7 str: dbg_library_load
[+] Notification code: 12 str: dbg_bpt
PDBSRC: loading symbols for 'C:\Users\max\Desktop\ConsoleApplication2.exe'...
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 12 str: dbg_bpt
[+] Notification code: 11 str: dbg_suspend_process
[+] Reanalizyng instruction at 0x13f2110e0
[+] Triton at 0x13f2110e0: mov qword ptr [rsp + 0x10], rdx (Thread id: 6116)
[+] We need a register! Register: rsp Value: 0x1ef8f8
[+] We need a register! Register: rdx Value: 0x398990
Enabling step tracing
Disabling step tracing
13F211005: using guessed type __int64 sub_13F211005(void);
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
Debugger: process has exited (exit code -1)
[+] Notification code: 2 str: dbg_process_exit
[!] Process_exiting...
Rebasing program to 0x000000013F841000...
13F840000: process C:\Users\max\Desktop\ConsoleApplication2.exe has started (pid=5492)
[+] Notification code: 1 str: dbg_process_start
[+] Starting the debugged process. Reseting all the engines.
[+] Restarting triton engines...
[+] main function found at 0x13f84100f
77A20000: loaded C:\Windows\system32\ntdll.dll
[+] Notification code: 7 str: dbg_library_load
77800000: loaded C:\Windows\system32\kernel32.dll
[+] Notification code: 7 str: dbg_library_load
7FEFDBF0000: loaded C:\Windows\system32\KernelBase.dll
[+] Notification code: 7 str: dbg_library_load
[+] Notification code: 12 str: dbg_bpt
PDBSRC: loading symbols for 'C:\Users\max\Desktop\ConsoleApplication2.exe'...
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 12 str: dbg_bpt
[+] Notification code: 16 str: dbg_step_over
[+] Notification code: 11 str: dbg_suspend_process
[+] Symbolizing memory from 0x3189d5 to 0x3189da. Total: 6 bytes
[+] We need memory! Address: 0x3189d5 Size: 1
[+] We need memory! Address: 0x3189d6 Size: 1
[+] We need memory! Address: 0x3189d7 Size: 1
[+] We need memory! Address: 0x3189d8 Size: 1
[+] We need memory! Address: 0x3189d9 Size: 1
[+] We need memory! Address: 0x3189da Size: 1
[+] Symbolizing memory from 0x3189d5 to 0x3189db. Total: 7 bytes
[+] We need memory! Address: 0x3189d5 Size: 1
[+] We need memory! Address: 0x3189d6 Size: 1
[+] We need memory! Address: 0x3189d7 Size: 1
[+] We need memory! Address: 0x3189d8 Size: 1
[+] We need memory! Address: 0x3189d9 Size: 1
[+] We need memory! Address: 0x3189da Size: 1
[+] We need memory! Address: 0x3189db Size: 1
[+] Notification code: 19 str: dbg_bpt_changed
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8410e5: mov dword ptr [rsp + 8], ecx (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe78
[+] We need a register! Register: ecx Value: 0x2
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8410e9: push rdi (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe78
[+] We need a register! Register: rdi Value: 0x1
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8410ea: sub rsp, 0x20 (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe70
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8410ee: mov rdi, rsp (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe50
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8410f1: mov ecx, 8 (Thread id: 696)
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8410f6: mov eax, 0xcccccccc (Thread id: 696)
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8410fb: rep stosd dword ptr [rdi], eax (Thread id: 696)
[+] We need a register! Register: rdi Value: 0x17fe50
[+] We need a register! Register: eax Value: 0xcccccccc
[+] We need a register! Register: rdi Value: 0x17fe50
[+] We need a register! Register: df Value: 0
[+] We need a register! Register: rcx Value: 0x8
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8410fd: mov ecx, dword ptr [rsp + 0x30] (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe50
[+] We need memory! Address: 0x17fe80 Size: 4
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841101: lea rcx, qword ptr [rip + 0x23c30] (Thread id: 696)
[+] We need a register! Register: rip Value: 0x13f841101
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 19 str: dbg_bpt_changed
[+] Triton at 0x13f841108: call 0x13f841280 (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe50
[+] Notification code: 12 str: dbg_bpt
BP Instructions traced: 16 Symbolic instructions: 0 Symbolic conditions: 0 Time: 167 secs
[+] Triton at 0x13f84110d: lea rcx, qword ptr [rip + 0x23c34] (Thread id: 696)
[+] We need a register! Register: rip Value: 0x13f84110d
[+] Notification code: 19 str: dbg_bpt_changed
[+] Notification code: 13 str: dbg_trace
[+] Notification code: 19 str: dbg_bpt_changed
[+] Triton at 0x13f841114: call 0x13f841354 (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe50
[+] Notification code: 12 str: dbg_bpt
BP Instructions traced: 17 Symbolic instructions: 0 Symbolic conditions: 0 Time: 198 secs
[+] Triton at 0x13f841119: cmp dword ptr [rsp + 0x30], 2 (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe50
[+] We need memory! Address: 0x17fe80 Size: 4
[+] Notification code: 19 str: dbg_bpt_changed
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f84111e: jge 0x13f841129 (Thread id: 696)
[+] We need a register! Register: sf Value: 0
[+] We need a register! Register: of Value: 0
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841129: mov eax, 8 (Thread id: 696)
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f84112e: imul rax, rax, 1 (Thread id: 696)
[+] We need a register! Register: rax Value: 0x8
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841132: lea rdx, qword ptr [rip + 0x23c1f] (Thread id: 696)
[+] We need a register! Register: rip Value: 0x13f841132
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841139: mov rcx, qword ptr [rsp + 0x38] (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe50
[+] We need memory! Address: 0x17fe88 Size: 8
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f84113e: mov rcx, qword ptr [rcx + rax] (Thread id: 696)
[+] We need a register! Register: rax Value: 0x8
[+] We need a register! Register: rcx Value: 0x318990
[+] We need memory! Address: 0x318998 Size: 8
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841142: call 0x13f8414e0 (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe50
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8414e0: sub rdx, rcx (Thread id: 696)
[+] We need a register! Register: rdx Value: 0x13f864d58
[+] We need a register! Register: rcx Value: 0x3189d5
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8414e3: test cl, 7 (Thread id: 696)
[+] We need a register! Register: cl Value: 0xd5
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8414e6: je 0x13f8414fc (Thread id: 696)
[+] We need a register! Register: zf Value: 0
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8414e8: movzx eax, byte ptr [rcx] (Thread id: 696)
[+] We need a register! Register: rcx Value: 0x3189d5
[+] We need memory! Address: 0x3189d5 Size: 1
[!] Instruction symbolized at 0x13f8414e8 
[+] Renaming function strcmp -> T_000_strcmp
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8414eb: cmp al, byte ptr [rcx + rdx] (Thread id: 696)
[+] We need a register! Register: rdx Value: 0x13f54c383
[+] We need a register! Register: rcx Value: 0x3189d5
[+] We need memory! Address: 0x13f864d58 Size: 1
[!] Instruction symbolized at 0x13f8414eb 
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f8414ee: jne 0x13f84153f (Thread id: 696)
[!] Instruction symbolized at 0x13f8414ee 
[+] Branch symbolized detected at 0x13f8414ee: 0x13f8414f0 or 0x13f84153f, Taken:Yes
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f84153f: sbb rax, rax (Thread id: 696)
[!] Instruction symbolized at 0x13f84153f 
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841542: or rax, 1 (Thread id: 696)
[!] Instruction symbolized at 0x13f841542 
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841546: ret  (Thread id: 696)
[+] We need a register! Register: rsp Value: 0x17fe48
[+] We need memory! Address: 0x17fe48 Size: 8
[+] We need a register! Register: rsp Value: 0x17fe48
[+] Notification code: 12 str: dbg_bpt
BP Instructions traced: 34 Symbolic instructions: 5 Symbolic conditions: 1 Time: 306 secs
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841147: test eax, eax (Thread id: 696)
[!] Instruction symbolized at 0x13f841147 
[+] Renaming function main_0 -> T_001_main_0
[+] Notification code: 11 str: dbg_suspend_process
[+] Notification code: 19 str: dbg_bpt_changed
[+] Notification code: 19 str: dbg_bpt_changed
[+] Notification code: 12 str: dbg_bpt
BP Instructions traced: 35 Symbolic instructions: 6 Symbolic conditions: 1 Time: 30953 secs
[+] Notification code: 13 str: dbg_trace
[+] Triton at 0x13f841149: jne 0x13f841152 (Thread id: 696)
[!] Instruction symbolized at 0x13f841149 
[+] Branch symbolized detected at 0x13f841149: 0x13f84114b or 0x13f841152, Taken:Yes
[+] Notification code: 11 str: dbg_suspend_process
[+] Solving condition at 1
[+] Keeping condition 0
[+] Inverting condition 1
[+] ripId: 157 notTakenAddr: 0x13f84114b
[+] Solving formula...
[+] Formula: (set-logic QF_AUFBV)
(declare-fun SymVar_0 () (_ BitVec 8))(declare-fun SymVar_1 () (_ BitVec 8))(declare-fun SymVar_2 () (_ BitVec 8))(declare-fun SymVar_3 () (_ BitVec 8))(declare-fun SymVar_4 () (_ BitVec 8))(declare-fun SymVar_5 () (_ BitVec 8))(declare-fun SymVar_6 () (_ BitVec 8))(declare-fun SymVar_7 () (_ BitVec 8))(declare-fun SymVar_8 () (_ BitVec 8))(declare-fun SymVar_9 () (_ BitVec 8))(declare-fun SymVar_10 () (_ BitVec 8))(declare-fun SymVar_11 () (_ BitVec 8))(declare-fun SymVar_12 () (_ BitVec 8))

(assert (= ((_ zero_extend 0) (ite (= ((_ extract 0 0) (ite (= ((_ extract 7 0) (bvsub ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8))))) (_ bv0 8)) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (_ bv5360588095 64) (_ bv5360588016 64))) (_ bv5360588095 64)))(assert (= ((_ zero_extend 0) (ite (= ((_ extract 0 0) (ite (= ((_ extract 31 0) (bvand ((_ extract 31 0) ((_ zero_extend 0) (bvor ((_ extract 63 0) ((_ zero_extend 0) (bvsub ((_ extract 63 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) (bvadd ((_ extract 63 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ zero_extend 63) ((_ extract 0 0) ((_ extract 7 7) (bvxor (bvxor ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) (bvxor ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8))) ((_ extract 7 0) (bvsub ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8))))))) (bvand (bvxor ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ extract 7 0) (bvsub ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8)))))) (bvxor ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8))))))))))))) (_ bv1 64)))) ((_ extract 31 0) ((_ zero_extend 0) (bvor ((_ extract 63 0) ((_ zero_extend 0) (bvsub ((_ extract 63 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) (bvadd ((_ extract 63 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ zero_extend 63) ((_ extract 0 0) ((_ extract 7 7) (bvxor (bvxor ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) (bvxor ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8))) ((_ extract 7 0) (bvsub ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8))))))) (bvand (bvxor ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ extract 7 0) (bvsub ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8)))))) (bvxor ((_ extract 7 0) ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) SymVar_6))))) ((_ sign_extend 0) ((_ extract 7 0) (_ bv106 8))))))))))))) (_ bv1 64)))))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (_ bv5360587090 64) (_ bv5360587083 64))) (_ bv5360587083 64)))
(check-sat)
(get-model)
[!] No solution found :(
0ca commented 5 years ago 
[+] Solving condition at 1
[+] Keeping condition 0
[+] Inverting condition 1

I think you should solve first the condition 0, that is the symbolic condition inside strcmp. If not it keeps the condition inside the strmp pwd[0] == 'a' and then it tries to solve ret value for strcmp != 0 and it can not find any solution.