Length matching error when using the `and` bit operation on two conditional expressions

[Lerr1uqs]

Description

I use two conditional expressions to execute & bit arithmetic operation. But failed in length check.

│ /home/squ/Projects/self-proj/Warden/src/see/engine.py:382 in exec_branch                         │
│                                                                                                  │
│   379 │   │   │   elif op == const.opcode.AND:                                                   │
│   380 │   │   │   │   [s0, s1] = state.stack_pop(2)                                              │
│   381 │   │   │   │   # fix for python10 claripy                                                 │
│ ❱ 382 │   │   │   │   state.stack_push(s0 & s1)                                                  │
│   383 │   │   │   │   # state.stack_push(                                                        │
│   384 │   │   │   │   #     claripy.If(                                                          │
│   385 │   │   │   │   #         claripy.And((s0 != BVV0), (s1 != BVV0)),                         │
│                                                                                                  │
│ ╭─────────────────────────────────────────── locals ───────────────────────────────────────────╮ │
│ │     bps = []                                                                                 │ │
│ │ curinst = <Instruction name=AND address=0x6ea size=1 >                                       │ │
│ │   depth = 3                                                                                  │ │
│ │      op = 22                                                                                 │ │
│ │ pushnum = 32                                                                                 │ │
│ │      s0 = <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0>                            │ │
│ │      s1 = <BV256 if 0x2 > 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff │ │
│ │           / input-uint256_2_256 then 0x1 else 0x0>                                           │ │
│ │    self = <see.engine.SymExecEngine object at 0x7fb09f40ea70>                                │ │
│ │   state = State(                                                                             │ │
│ │           selfdestruct_to = None                                                             │ │
│ │           pc = 6ea                                                                           │ │
│ │           calls = []                                                                         │ │
│ │           storage = 1 <BV256 (0xff & LShR(LShR(LShR(input-uint256_3_256, 0x8), 0x8), 0x8)) * │ │
│ │           0x1 | 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00 & (0x100  │ │
│ │           * (0x0 .. input-uint256_3_256[23:16]) | (0x10000 * (0x0 ..                         │ │
│ │           input-uint256_3_256[15:8])[255:16] | (0x1000000 * (0x0 ..                          │ │
│ │           input-uint256_3_256[7:0])[255:24] .. 0) .. 0x0))>                                  │ │
│ │                                                                                              │ │
│ │           solver = <claripy.solvers.Solver object at 0x7fb09ef79e40>                         │ │
│ │           )                                                                                  │ │
│ │     txn = <evm.transaction.Transaction object at 0x7fb09ef7aaa0>                             │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│                                                                                                  │
│ /home/squ/.local/lib/python3.10/site-packages/claripy/operations.py:57 in _op                    │
│                                                                                                  │
│    54 │   │   │   │   │   raise ClaripyOperationError(msg)                                       │
│    55 │   │                                                                                      │
│    56 │   │   # pylint:disable=too-many-nested-blocks                                            │
│ ❱  57 │   │   simp = _handle_annotations(simplifications.simpleton.simplify(name, fixed_args),   │
│    58 │   │   if simp is not None:                                                               │
│    59 │   │   │   return simp                                                                    │
│    60                                                                                            │
│                                                                                                  │
│ ╭─────────────────────────────────────────── locals ───────────────────────────────────────────╮ │
│ │ _type_fixer = <function op.<locals>._type_fixer at 0x7fb0a53765f0>                           │ │
│ │        args = (                                                                              │ │
│ │               │   <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0>,                   │ │
│ │               │   <BV256 if 0x2 >                                                            │ │
│ │               0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff /           │ │
│ │               input-uint256_2_256 then 0x1 else 0x0>                                         │ │
│ │               )                                                                              │ │
│ │ calc_length = <function basic_length_calc at 0x7fb0a559ff40>                                 │ │
│ │ extra_check = <function length_same_check at 0x7fb0a559feb0>                                 │ │
│ │  fixed_args = (                                                                              │ │
│ │               │   <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0>,                   │ │
│ │               │   <BV256 if 0x2 >                                                            │ │
│ │               0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff /           │ │
│ │               input-uint256_2_256 then 0x1 else 0x0>                                         │ │
│ │               )                                                                              │ │
│ │           i = <BV256 if 0x2 >                                                                │ │
│ │               0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff /           │ │
│ │               input-uint256_2_256 then 0x1 else 0x0>                                         │ │
│ │         msg = "args' length must all be equal"                                               │ │
│ │        name = '__and__'                                                                      │ │
│ │ return_type = <class 'claripy.ast.bv.BV'>                                                    │ │
│ │     success = True                                                                           │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│                                                                                                  │
│ /home/squ/.local/lib/python3.10/site-packages/claripy/simplifications.py:43 in simplify          │
│                                                                                                  │
│     40 │   def simplify(self, op, args):                                                         │
│     41 │   │   if op not in self._simplifiers:                                                   │
│     42 │   │   │   return None                                                                   │
│ ❱   43 │   │   return self._simplifiers[op](*args)                                               │
│     44 │                                                                                         │
│     45 │   @staticmethod                                                                         │
│     46 │   def _deduplicate_filter(args):                                                        │
│                                                                                                  │
│ ╭─────────────────────────────────────────── locals ───────────────────────────────────────────╮ │
│ │ args = (                                                                                     │ │
│ │        │   <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0>,                          │ │
│ │        │   <BV256 if 0x2 >                                                                   │ │
│ │        0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff /                  │ │
│ │        input-uint256_2_256 then 0x1 else 0x0>                                                │ │
│ │        )                                                                                     │ │
│ │   op = '__and__'                                                                             │ │
│ │ self = <claripy.simplifications.SimplificationManager object at 0x7fb0a55dc5b0>              │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│                                                                                                  │
│ /home/squ/.local/lib/python3.10/site-packages/claripy/simplifications.py:734 in                  │
│ bitwise_and_simplifier                                                                           │
│                                                                                                  │
│    731 │   │   │   # if(cond0, 1, 0) & if(cond1, 1, 0)  ->  if(cond0 & cond1, 1, 0)              │
│    732 │   │   │   if a.op == "If" and b.op == "If":                                             │
│    733 │   │   │   │   if (                                                                      │
│ ❱  734 │   │   │   │   │   (a.args[1] == ast.all_operations.BVV(1, 1)).is_true()                 │
│    735 │   │   │   │   │   and (a.args[2] == ast.all_operations.BVV(0, 1)).is_true()             │
│    736 │   │   │   │   │   and (b.args[1] == ast.all_operations.BVV(1, 1)).is_true()             │
│    737 │   │   │   │   │   and (b.args[2] == ast.all_operations.BVV(0, 1)).is_true()             │
│                                                                                                  │
│ ╭─────────────────────────────────────────── locals ───────────────────────────────────────────╮ │
│ │    a = <BV256 if input-uint256_2_256 != 0x0 then 0x1 else 0x0>                               │ │
│ │ args = ()                                                                                    │ │
│ │    b = <BV256 if 0x2 > 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff /  │ │
│ │        input-uint256_2_256 then 0x1 else 0x0>                                                │ │
│ │    r = None                                                                                  │ │
│ ╰──────────────────────────────────────────────────────────────────────────────────────────────╯ │
│                                                                                                  │
│ /home/squ/.local/lib/python3.10/site-packages/claripy/operations.py:54 in _op                    │
│                                                                                                  │
│    51 │   │   │   if extra_check is not None:                                                    │
│    52 │   │   │   │   success, msg = extra_check(*fixed_args)                                    │
│    53 │   │   │   │   if not success:                                                            │
│ ❱  54 │   │   │   │   │   raise ClaripyOperationError(msg)                                       │
│    55 │   │                                                                                      │
│    56 │   │   # pylint:disable=too-many-nested-blocks                                            │
│    57 │   │   simp = _handle_annotations(simplifications.simpleton.simplify(name, fixed_args),   │
│                                                                                                  │
│ ╭────────────────────────────── locals ──────────────────────────────╮                           │
│ │ _type_fixer = <function op.<locals>._type_fixer at 0x7fb0a5375360> │                           │
│ │        args = (<BV256 0x1>, <BV1 1>)                               │                           │
│ │ calc_length = None                                                 │                           │
│ │ extra_check = <function length_same_check at 0x7fb0a559feb0>       │                           │
│ │  fixed_args = (<BV256 0x1>, <BV1 1>)                               │                           │
│ │           i = <BV1 1>                                              │                           │
│ │         msg = "args' length must all be equal"                     │                           │
│ │        name = '__eq__'                                             │                           │
│ │ return_type = <class 'claripy.ast.bool.Bool'>                      │                           │
│ │     success = False                                                │                           │
│ ╰────────────────────────────────────────────────────────────────────╯                           │
╰──────────────────────────────────────────────────────────────────────────────────────────────────╯

Steps to reproduce the bug

a = BVS("uint256-a", 256)
b = BVS("uint256-b", 256)

BVV0 = BVV(0, 256)
BVV1 = BVV(1, 256)

solver = Solver()
# solver.add(Not(a == 0))
c = If(a > 0, BVV(0xff, 256), BVV0)
d = If(b < 0xff, BVV(0xff, 256), BVV0)
e = (c ^ d)
print(e) # work
e = (c | d)
print(e) # work
e = (c & d)
print(e) # !!! raise ClaripyOperationError(claripy.errors.ClaripyOperationError: args' length must all be equal)

Environment

angr environment report

Date: 2023-12-25 19:30:05.904681
!!! running in global environment. Are you sure? !!!
Platform: linux-x86_64
Python version: 3.10.12 (main, Nov 20 2023, 15:14:05) [GCC 11.4.0]
######## angr #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/angr/init.py
Pip version angr 9.2.81
Couldn't find git info
######## ailment #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/ailment/init.py
Pip version ailment 9.2.81
Couldn't find git info
######## cle #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/cle/init.py
Pip version cle 9.2.81
Couldn't find git info
######## pyvex #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/pyvex/init.py
Pip version pyvex 9.2.81
Couldn't find git info
######## claripy #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/claripy/init.py
Pip version claripy 9.2.81
Couldn't find git info
######## archinfo #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/archinfo/init.py
Pip version archinfo 9.2.81
Couldn't find git info
######## z3 #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/z3/init.py
Pip version z3-solver 4.10.2.0
Couldn't find git info
######## unicorn #########
Python found it in /home/squ/.local/lib/python3.10/site-packages/unicorn/init.py
Pip version unicorn 2.0.1.post1
Couldn't find git info
######### Native Module Info ##########
angr: <CDLL '/home/squ/.local/lib/python3.10/site-packages/angr/state_plugins/../lib/angr_native.so', handle 55c215f60590 at 0x7f463e041d80>
unicorn: <CDLL '/home/squ/.local/lib/python3.10/site-packages/unicorn/lib/libunicorn.so.2', handle 55c215a70b20 at 0x7f4640d21630>
pyvex: <cffi.api._make_ffi_library..FFILibrary object at 0x7f4641a1e320>
z3: <CDLL '/home/squ/.local/lib/python3.10/site-packages/z3/lib/libz3.so', handle 55c215737340 at 0x7f4643bfb7c0>

Additional context

No response

[jvoisin]

I encounter this issue locally when trying to decompile the main function from the
Free Madame De Maintenon – CTF Challenge:

$ angr-management 

(python:51985): dbind-WARNING **: 17:52:35.514: AT-SPI: Error retrieving accessibility bus address: org.freedesktop.DBus.Error.ServiceUnknown: The name org.a11y.Bus was not provided by any .service files
0.00s - Debugger warning: It seems that frozen modules are being used, which may
0.00s - make the debugger miss breakpoints. Please pass -Xfrozen_modules=off
0.00s - to python to disable frozen modules.
0.00s - Note: Debugging will proceed. Set PYDEVD_DISABLE_FILE_VALIDATION=1 to disable this validation.
INFO     | 2024-01-17 17:52:54,455 | angrmanagement.data.jobs.job | Job "Loading file" started
WARNING  | 2024-01-17 17:52:54,471 | cle.backends.backend | Unused kwargs for loading binary /home/jvoisin/Downloads/challenge: ignore_missing_arch
INFO     | 2024-01-17 17:53:01,693 | angrmanagement.data.jobs.job | Job "Loading file" completed after 7.24 seconds
INFO     | 2024-01-17 17:53:01,693 | angrmanagement.data.jobs.job | Job "CFG generation" started
INFO     | 2024-01-17 17:53:02,067 | angrmanagement.data.jobs.job | Job "CFG generation" completed after 0.37 seconds
INFO     | 2024-01-17 17:53:02,144 | angrmanagement.data.jobs.job | Job "Applying FLIRT signatures" started
WARNING  | 2024-01-17 17:53:02,145 | angrmanagement.data.jobs.flirt_signature_recognition | No FLIRT signatures exist for architecture AMD64.
INFO     | 2024-01-17 17:53:02,145 | angrmanagement.data.jobs.job | Job "Applying FLIRT signatures" completed after 0.00 seconds
INFO     | 2024-01-17 17:53:02,166 | angrmanagement.data.jobs.job | Job "Function prototype finding" started
INFO     | 2024-01-17 17:53:02,166 | angrmanagement.data.jobs.job | Job "Function prototype finding" completed after 0.00 seconds
INFO     | 2024-01-17 17:53:02,207 | angrmanagement.data.jobs.job | Job "Variable Recovery" started
WARNING  | 2024-01-17 17:53:02,225 | angr.analyses.variable_recovery.engine_vex.SimEngineVRVEX | Unsupported Binop Iop_MullU64.
WARNING  | 2024-01-17 17:53:02,554 | angr.analyses.reaching_definitions.engine_vex.SimEngineRDVEX | Unsupported Binop Iop_64HLto128.
INFO     | 2024-01-17 17:53:02,928 | angrmanagement.data.jobs.job | Job "Variable Recovery" completed after 0.72 seconds
INFO     | 2024-01-17 17:53:14,888 | angrmanagement.data.jobs.job | Job "Variable Recovery" started
INFO     | 2024-01-17 17:53:14,982 | angrmanagement.data.jobs.job | Job "Variable Recovery" completed after 0.09 seconds
INFO     | 2024-01-17 17:53:14,995 | angrmanagement.data.jobs.job | Job "Decompiling" started
ERROR    | 2024-01-17 17:53:15,116 | angrmanagement.data.instance | Exception while running job "Decompiling":
Traceback (most recent call last):
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angrmanagement/data/instance.py", line 343, in _worker
    result = job.run(self)
             ^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angrmanagement/data/jobs/job.py", line 69, in run
    r = self._run(inst)
        ^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angrmanagement/data/jobs/decompile_function.py", line 17, in _run
    decompiler = inst.project.analyses.Decompiler(
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 216, in __call__
    r = w(*args, **kwargs)
        ^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 201, in wrapper
    oself.__init__(*args, **kwargs)
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/decompiler.py", line 97, in __init__
    self._decompile()
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/decompiler.py", line 158, in _decompile
    clinic = self.project.analyses.Clinic(
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 216, in __call__
    r = w(*args, **kwargs)
        ^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 201, in wrapper
    oself.__init__(*args, **kwargs)
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/clinic.py", line 142, in __init__
    self._analyze_for_decompiling()
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/clinic.py", line 245, in _analyze_for_decompiling
    self._simplify_function(
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/utils/timing.py", line 43, in timed_func
    return func(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/clinic.py", line 837, in _simplify_function
    simplified = self._simplify_function_once(
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/utils/timing.py", line 43, in timed_func
    return func(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/clinic.py", line 867, in _simplify_function_once
    simp = self.project.analyses.AILSimplifier(
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 216, in __call__
    r = w(*args, **kwargs)
        ^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 201, in wrapper
    oself.__init__(*args, **kwargs)
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 104, in __init__
    self._simplify()
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 117, in _simplify
    folded_exprs = self._fold_exprs()
                   ^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 538, in _fold_exprs
    propagator = self._compute_propagation(immediate_stmt_removal=True)
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 198, in _compute_propagation
    reaching_definitions=self._compute_reaching_definitions(),
                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/decompiler/ail_simplifier.py", line 178, in _compute_reaching_definitions
    rd = self.project.analyses.ReachingDefinitions(
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 216, in __call__
    r = w(*args, **kwargs)
        ^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/analysis.py", line 201, in wrapper
    oself.__init__(*args, **kwargs)
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/reaching_definitions.py", line 202, in __init__
    self._analyze()
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/forward_analysis/forward_analysis.py", line 252, in _analyze
    self._analysis_core_graph()
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/forward_analysis/forward_analysis.py", line 269, in _analysis_core_graph
    changed, output_state = self._run_on_node(n, job_state)
                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/reaching_definitions.py", line 524, in _run_on_node
    state = engine.process(
            ^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 85, in process
    self._process(
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/engines/light/engine.py", line 807, in _process
    self._process_Stmt(whitelist=whitelist)
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 119, in _process_Stmt
    super()._process_Stmt(whitelist=whitelist)
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/engines/light/engine.py", line 823, in _process_Stmt
    self._handle_Stmt(stmt)
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 130, in _handle_Stmt
    handler(stmt)
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 153, in _ail_handle_Assignment
    src = self._expr(stmt.src)
          ^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 141, in _expr
    return handler(expr)
           ^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 636, in _ail_handle_BinaryOp
    r = super()._ail_handle_BinaryOp(expr)
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/engines/light/engine.py", line 960, in _ail_handle_BinaryOp
    return handler(expr)
           ^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 719, in _ail_handle_DivMod
    return self._ail_handle_Div(expr)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/angr/analyses/reaching_definitions/engine_ail.py", line 781, in _ail_handle_Div
    r = MultiValues(offset_to_values={0: {expr0_v / expr1_v}})
                                          ~~~~~~~~^~~~~~~~~
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/claripy/utils/deprecated.py", line 16, in inner
    return func(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^^^
  File "/home/jvoisin/Downloads/.ven/lib/python3.11/site-packages/claripy/operations.py", line 54, in _op
    raise ClaripyOperationError(msg)
claripy.errors.ClaripyOperationError: args' length must all be equal
$