Angr unconstrained state has the same address as a found state

I am working on a simple symbolic execution problem. The code is as follows

// odd_even.c
#include <stdio.h>

int main(void)
{
    int x;   //yes x is uninitialized here, but that won't matter during symbolic execution would it?
    if (x % 2 == 0)
        printf("Even");
    else
        printf("Odd");
    return 0;
}

After compiling with gcc odd_even.c -o odd_even on a 64-bit machine and using binary ninja here is the cfg of main

Disassembly for main()

00401136  int32_t main(int32_t argc, char** argv, char** envp)

00401136  f30f1efa           endbr64 
0040113a  55                 push    rbp {__saved_rbp}
0040113b  4889e5             mov     rbp, rsp {__saved_rbp}
0040113e  4883ec10           sub     rsp, 0x10
00401142  8b45fc             mov     eax, dword [rbp-0x4 {var_c}]
00401145  83e001             and     eax, 0x1
00401148  85c0               test    eax, eax
0040114a  7511               jne     0x40115d

0040114c  bf04204000         mov     edi, 0x402004  {"Even"}
00401151  b800000000         mov     eax, 0x0
00401156  e8e5feffff         call    printf
0040115b  eb0f               jmp     0x40116c

0040115d  bf09204000         mov     edi, 0x402009
00401162  b800000000         mov     eax, 0x0
00401167  e8d4feffff         call    printf

0040116c  b800000000         mov     eax, 0x0
00401171  c9                 leave    {__saved_rbp}
00401172  c3                 retn     {__return_addr}

My goal is to reach the address 0x0040116c. I am able to use the explore() method on angr's simulation_manager and it does work, except that it ends with 2 stashes, found, and active which eventually becomesunconstrained, both having address as 0x0040116c.

Here is my angr script, in the python interpreter

>>> import angr
>>> p = angr.Project('odd_even')
>>> s = p.factory.blank_state(addr = 0x401142, add_options={angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY
,angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS})
>>> x = s.solver.BVS("x",64)
>>> s.regs.rbp = s.regs.rsp                            //setting up the stack
>>> s.stack_push(x)
>>> simgr = p.factory.simulation_manager(s,save_unconstrained = True)
>>> simgr.explore(find= 0x40116c)
<SimulationManager with 1 active, 1 found>
>>> simgr.active
[<SimState @ 0x40116c>]                                //active and found states have same address
>>> simgr.found
[<SimState @ 0x40116c>]
>>> simgr.found[0].solver.constraints
[<Bool (x_40_64[39:32] & 1) != 0>]
>>> simgr.active[0].solver.constraints
[<Bool (x_40_64[39:32] & 1) == 0>]
>>> simgr.step()
WARNING  | 2024-11-12 16:57:01,371 | angr.engines.successors | Exit state has over 256 possible solutions
. Likely unconstrained; skipping. <BV64 mem_7ffffffffff0008_42_64{UNINITIALIZED}>
<SimulationManager with 1 unconstrained, 1 found>
>>> simgr.unconstrained[0]
<SimState @ <BV64 mem_7ffffffffff0008_42_64{UNINITIALIZED}>>
>>> simgr.unconstrained[0].solver.constraints
[<Bool x_40_64[32:32] == 0>]
>>> simgr.unconstrained[0].solver.eval(x)
0x0
>>> simgr.found[0].solver.eval(x)
0x100000000

I expected 2 states in the found stash with both the states representing the odd and even branches respectively. What could be the reason for this behavior?

From the source code of angr.sim_manager.SimulationManager.explore

Tick stash "stash" forward (up to "n" times or until "num_find" states are found), looking for condition "find", avoiding condition "avoid". Stores found states into "find_stash' and avoided states into "avoid_stash".

As mentioned, using simgr.explore(find= 0x40116c, num_find = 2) results in 2 states in the found stash, with each of them representing their respective constraints.

Alternatively, calling simgr.explore(find= 0x40116c) multiple times also achieves the same result, eventually.