Goose  Diff

Differences From Artifact [a02e5ff5dd]:

• File bs/verify/value.cpp — part of check-in [b2945b5bb1] at 2021-03-05 17:56:37 on branch trunk — Implemented refinement type predicate unification. Predicate violations by variable initialization are now properly detected. (user: achavasse size: 13861)

To Artifact [c068b1bc6f]:

• File bs/verify/value.cpp — part of check-in [3e169a34af] at 2021-03-18 12:42:59 on branch trunk — Verifier: get rid of a helper that's no longer needed (user: achavasse size: 13847)

251
252
253
254
255
256
257
258
259
260
261
262
263
264
265

    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Xor& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bool() && rhs.is_bool() )
                return mkZ3BoolXor( lhs, rhs );

            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return lhsBV ^ rhsBV;
        } );
    }

|

251
252
253
254
255
256
257
258
259
260
261
262
263
264
265

    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Xor& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bool() && rhs.is_bool() )
                return lhs ^ rhs;

            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return lhsBV ^ rhsBV;
        } );
    }