}
    
    int BitVecCompare(BitVec *bv1, BitVec *bv2) {
        ValidateBitVec(bv1);
        ValidateBitVec(bv2);

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

        BitVecPush(&bv2, false);
    
        bool result = (BitVecCompare(&bv1, &bv2) == 0);
    
        // Test first greater than second

        BitVecPush(&bv2, false); // 10
    
        result = result && (BitVecCompare(&bv1, &bv2) > 0);
        result = result && (BitVecCompare(&bv2, &bv1) < 0);

    
        result = result && (BitVecCompare(&bv1, &bv2) > 0);
        result = result && (BitVecCompare(&bv2, &bv1) < 0);
    
        // Clean up

    
        // Lexicographic comparison considers position-by-position
        int  cmp_result = BitVecCompare(&bv1, &bv2);
        bool result     = (cmp_result != 0); // Should not be equal

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

    
        // Lexicographically, shorter comes first
        bool result = (BitVecCompare(&bv1, &bv2) < 0);
    
        // Numerically, 10 (2) < 101 (5)

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

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

        // Test compare empty bitvecs
        result = result && BitVecEquals(&bv1, &bv2);
        result = result && (BitVecCompare(&bv1, &bv2) == 0);
    
        // Test compare empty vs non-empty

        BitVecPush(&bv1, true);
        result = result && !BitVecEquals(&bv1, &bv2);
        result = result && (BitVecCompare(&bv1, &bv2) != 0);
    
        // Test large identical bitvecs

        // Numerical: 86 < 89, so bv1 < bv2
        result = result && (BitVecNumericalCompare(&bv1, &bv2) < 0);
        result = result && (BitVecCompare(&bv1, &bv2) < 0);
    
        // Weight: bv1 has 4 ones, bv2 has 4 ones, so equal weight

    
        // Lexicographic comparison
        int  lex_cmp  = BitVecCompare(&bv1, &bv2);
        bool lex_less = (BitVecCompare(&bv1, &bv2) < 0);
        result        = result && ((lex_cmp < 0) == lex_less);

        // Lexicographic comparison
        int  lex_cmp  = BitVecCompare(&bv1, &bv2);
        bool lex_less = (BitVecCompare(&bv1, &bv2) < 0);
        result        = result && ((lex_cmp < 0) == lex_less);