First or second argument must be a Z3 bit-vector expression

Hello, I am testing Oyente with the Ballot contract found here.

However, it seems that the symbolic execution engine inserts a symbolic expression for CALLDATALOAD, which then cannot be shifted using SHR, resulting in a symbolic expression shr(224,Id_1) to be added to the stack. Then, when we apply the GT instruction, it throws an error in Z3. Here is the full trace along with the stack:

==============================
EXECUTING: CALLDATALOAD
Stack after executing instruction CALLDATALOAD
[Id_1]
==============================
EXECUTING: PUSH1 0xe0
29
Stack after executing instruction PUSH1 0xe0
[(224, 26), Id_1]
==============================
EXECUTING: SHR
Stack after executing instruction SHR
['shr(224,Id_1)']
==============================
EXECUTING: DUP1
Stack after executing instruction DUP1
['shr(224,Id_1)', 'shr(224,Id_1)']
==============================
EXECUTING: PUSH4 0x609ff1bd
33
Stack after executing instruction PUSH4 0x609ff1bd
[(1621094845, 26), 'shr(224,Id_1)', 'shr(224,Id_1)']
==============================
EXECUTING: GT
Traceback (most recent call last):
  File "ethir.py", line 204, in run_solidity_analysis
    result, return_code = symExec.run(disasm_file=inp['disasm_file'], source_map=inp['source_map'], source_file=inp['source'],cfg = args.control_flow_graph,saco = args.saco,execution = 0, cname = inp["c_name"],hashes = function_names,debug = args.debug,evm_version = evm_version_modifications,cfile = args.cfile,svc=svc_options,go = args.goto,opt_bytecode = args.optimize_run)
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 3327, in run
    analyze(evm_version)
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 3111, in analyze
    run_build_cfg_and_analyze(evm_v = evm_version,timeout_cb=timeout_cb)
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 3063, in run_build_cfg_and_analyze
    build_cfg_and_analyze(evm_v)
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 327, in build_cfg_and_analyze
    full_sym_exec()  # jump targets are constructed on the fly
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 814, in full_sym_exec
    return sym_exec_block(params, 0, 0, 0, -1, 0,[(0,0)])
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 1046, in sym_exec_block
    analyze_next_block(block, left_branch, stack, path, func_call, depth, current_level, new_params, jump_type)
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 2964, in analyze_next_block
    sym_exec_block(new_params, successor, block, depth, func_call,current_level+1,path)
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 1074, in sym_exec_block
    analyze_next_block(block, right_branch, stack, path, func_call, depth, current_level, new_params, "falls_to")
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 2964, in analyze_next_block
    sym_exec_block(new_params, successor, block, depth, func_call,current_level+1,path)
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 925, in sym_exec_block
    sym_exec_ins(params, block, instr, func_call,stack_old,instr_index)
  File "/mnt/c/Users/junwe/Git/proj/EthIR/ethir/symExec.py", line 1621, in sym_exec_ins
    computed = If(UGT(first, second), BitVecVal(1, 256), BitVecVal(0, 256))
  File "/home/richhardry/.local/lib/python3.8/site-packages/z3/z3.py", line 4195, in UGT
    _check_bv_args(a, b)
  File "/home/richhardry/.local/lib/python3.8/site-packages/z3/z3.py", line 4125, in _check_bv_args
    _z3_assert(is_bv(a) or is_bv(b), "First or second argument must be a Z3 bit-vector expression")
  File "/home/richhardry/.local/lib/python3.8/site-packages/z3/z3.py", line 112, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: First or second argument must be a Z3 bit-vector expression

Any ideas? Would be greatly appreciated.

enzymefinance / oyente

First or second argument must be a Z3 bit-vector expression #428