int BitVecNumericalCompare(BitVec *bv1, BitVec *bv2) {
        ValidateBitVec(bv1);
        ValidateBitVec(bv2);

    
        // Same sign, compare numerically
        int result = BitVecNumericalCompare(bv1, bv2);
    
        // If both negative, reverse the comparison

    // Test BitVecNumericalCompare function
    bool test_bitvec_numerical_compare(void) {
        WriteFmt("Testing BitVecNumericalCompare\n");
    
        BitVec bv1 = BitVecInit();

    
        // Numerical comparison should compare the integer values
        int  cmp_result = BitVecNumericalCompare(&bv1, &bv2);
        bool result     = (cmp_result > 0); // 5 > 3

        BitVecPush(&bv2, true); // Also 101
    
        result = result && (BitVecNumericalCompare(&bv1, &bv2) == 0);
    
        // Clean up

    
        // Numerically, 10 (2) < 101 (5)
        result = result && (BitVecNumericalCompare(&bv1, &bv2) < 0);
    
        // Test equal cases

        BitVec bv3 = BitVecClone(&bv1);
        result     = result && !(BitVecCompare(&bv1, &bv3) < 0);
        result     = result && !(BitVecNumericalCompare(&bv1, &bv3) < 0);
    
        // Test reverse comparison

        // Test reverse comparison
        result = result && !(BitVecCompare(&bv2, &bv1) < 0);
        result = result && !(BitVecNumericalCompare(&bv2, &bv1) < 0);
    
        // Clean up

        // Cross-validate different comparison methods
        // Numerical: 86 < 89, so bv1 < bv2
        result = result && (BitVecNumericalCompare(&bv1, &bv2) < 0);
        result = result && (BitVecCompare(&bv1, &bv2) < 0);

        }
    
        if (BitVecNumericalCompare(&bv1, &bv2) < 0 && BitVecNumericalCompare(&bv2, &bv3) < 0) {
            result = result && (BitVecNumericalCompare(&bv1, &bv3) < 0);
        }

    
        if (BitVecNumericalCompare(&bv1, &bv2) < 0 && BitVecNumericalCompare(&bv2, &bv3) < 0) {
            result = result && (BitVecNumericalCompare(&bv1, &bv3) < 0);
        }

    
        // Unsigned: 01111111 (127) < 10000001 (129)
        result = result && (BitVecNumericalCompare(&pos, &neg) < 0);
    
        // Signed: 01111111 (+127) > 10000001 (-127)