fn general_relational()

in checker/src/z3_solver.rs [420:488]
69 lines of code
11 McCabe index (conditional complexity)

    fn general_relational(
        &self,
        left: &Rc<AbstractValue>,
        right: &Rc<AbstractValue>,
        float_op: unsafe extern "C" fn(
            c: z3_sys::Z3_context,
            t1: z3_sys::Z3_ast,
            t2: z3_sys::Z3_ast,
        ) -> z3_sys::Z3_ast,
        int_op: unsafe extern "C" fn(
            c: z3_sys::Z3_context,
            t1: z3_sys::Z3_ast,
            t2: z3_sys::Z3_ast,
        ) -> z3_sys::Z3_ast,
        signed_bit_op: unsafe extern "C" fn(
            c: z3_sys::Z3_context,
            t1: z3_sys::Z3_ast,
            t2: z3_sys::Z3_ast,
        ) -> z3_sys::Z3_ast,
        unsigned_bit_op: unsafe extern "C" fn(
            c: z3_sys::Z3_context,
            t1: z3_sys::Z3_ast,
            t2: z3_sys::Z3_ast,
        ) -> z3_sys::Z3_ast,
    ) -> z3_sys::Z3_ast {
        let (signed, num_bits) = if left.expression.is_bit_vector() {
            let ty = left.expression.infer_type();
            (ty.is_signed_integer(), u32::from(ty.bit_length()))
        } else if right.expression.is_bit_vector() {
            let ty = right.expression.infer_type();
            let mut result = (ty.is_signed_integer(), u32::from(ty.bit_length()));
            if let Expression::BitAnd { left, .. } = &right.expression {
                if let Expression::CompileTimeConstant(ConstantDomain::U128(v)) = left.expression {
                    if v < u128::MAX && (v + 1).is_power_of_two() {
                        result = (false, 0);
                    }
                }
            }
            result
        } else {
            (false, 0)
        };
        if num_bits > 0 {
            let left_ast = self.get_as_bv_z3_ast(&(**left).expression, num_bits);
            let right_ast = self.get_as_bv_z3_ast(&(**right).expression, num_bits);
            unsafe {
                if signed {
                    signed_bit_op(self.z3_context, left_ast, right_ast)
                } else {
                    unsigned_bit_op(self.z3_context, left_ast, right_ast)
                }
            }
        } else {
            let (lf, left_ast) = self.get_as_numeric_z3_ast(&(**left).expression);
            let (rf, right_ast) = self.get_as_numeric_z3_ast(&(**right).expression);
            if lf != rf {
                warn!("can't encode {:?} relational op {:?}", left, right);
                return self
                    .general_variable(&Path::get_as_path(left.clone()), ExpressionType::Bool);
            }
            unsafe {
                if lf {
                    float_op(self.z3_context, left_ast, right_ast)
                } else {
                    int_op(self.z3_context, left_ast, right_ast)
                }
            }
        }
    }