Goose  Diff

        else if( to.expr.is_bv() )
            return GetAsBitVec( expr, to.type );
        else
            return expr;
    }

    template< typename I, typename F >
    optional< Z3Val > BuildZ3UnaryExpr( Builder& b, const I& instr, F&& func )
    bool BuildZ3UnaryExpr( Builder& b, const I& instr, F&& func )
    {
        auto operand = BuildZ3ExprFromValue( b, instr.operand() );
        auto operand = b.pop();
        if( !operand )
            return nullopt;
            return false;

        return Z3Val{ func( operand->expr ), operand->type };
        b.push( Z3Val{ func( operand->expr ), operand->type } );
        return true;
    }

    template< typename I, typename F >
    optional< Z3Val > BuildZ3BinExpr( Builder& b, const I& instr, F&& func )
    bool BuildZ3BinExpr( Builder& b, const I& instr, F&& func )
    {
        auto lhs = BuildZ3ExprFromValue( b, instr.lhs() );
        if( !lhs )
            return nullopt;
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto rhs = BuildZ3ExprFromValue( b, instr.rhs() );
        if( !rhs )
            return nullopt;
        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
        {
            return Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type };
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type } );
            return true;
        }

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            return Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type };
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type } );
            return true;
        }
        else
        {
            assert( lhs->expr.is_int() );
            return Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type };
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type } );
            return true;
        }

        return nullopt;
        return false;
    }

    template< typename I, typename F >
    optional< Z3Val > BuildZ3BinBitwiseExpr( Builder& b, const I& instr, F&& func )
    bool BuildZ3BinBitwiseExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( instr.lhs().type() == GetValueType< BigInt >() )
        if( ValueToEIR( lhs->type ) == GetValueType< BigInt >() )
        {
            DiagnosticsManager::GetInstance().emitErrorMessage( instr.lhs().locationId(), "verifier error: bitwise operands can't be ct_int." );
            return nullopt;
            DiagnosticsManager::GetInstance().emitErrorMessage( 0, "verifier error: bitwise operands can't be ct_int." );
            return false;
        }

        if( instr.rhs().type() == GetValueType< BigInt >() )
        if( ValueToEIR( rhs->type ) == GetValueType< BigInt >() )
        {
            DiagnosticsManager::GetInstance().emitErrorMessage( instr.rhs().locationId(), "verifier error: bitwise operands can't be ct_int." );
            return nullopt;
            DiagnosticsManager::GetInstance().emitErrorMessage( 0, "verifier error: bitwise operands can't be ct_int." );
            return false;
        }

        auto lhs = BuildZ3ExprFromValue( b, instr.lhs() );
        if( !lhs )
        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
            return nullopt;

        {
        auto rhs = BuildZ3ExprFromValue( b, instr.rhs() );
        if( !rhs )
            return nullopt;

            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type } );
            return true;
        }
        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
            return Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type };

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            return Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type };
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type } );
            return true;
        }
        else
        {
            assert( lhs->expr.is_int() );
            return Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type };
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type } );
            return true;
        }

        return nullopt;
        return false;
    }

    template< typename I, typename F >
    optional< Z3Val > BuildZ3BinBoolExpr( Builder& b, const I& instr, F&& func )
    bool BuildZ3BinBoolExpr( Builder& b, const I& instr, F&& func )
    {
        auto lhs = BuildZ3ExprFromValue( b, instr.lhs() );
        if( !lhs )
            return nullopt;
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto rhs = BuildZ3ExprFromValue( b, instr.rhs() );
        if( !rhs )
            return nullopt;
        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
        {
            return Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ) };
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ) } );
            return true;
        }

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            return Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), *EIRToValue( GetValueType< bool >() ) };
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), *EIRToValue( GetValueType< bool >() ) } );
            return true;
        }
        else
        {
            assert( lhs->expr.is_int() );
            return Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ) };
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ) } );
            return true;
        }

        return nullopt;
        return false;
    }

    template< typename I, typename F >
    optional< Z3Val > BuildZ3BinLogicExpr( Builder& b, const I& instr, F&& func )
    bool BuildZ3BinLogicExpr( Builder& b, const I& instr, F&& func )
    {
        auto lhs = BuildZ3ExprFromValue( b, instr.lhs() );
        if( !lhs )
            return nullopt;
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto rhs = BuildZ3ExprFromValue( b, instr.rhs() );
        if( !rhs )
            return nullopt;
        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( !lhs->expr.is_bool() )
            return nullopt;
            return false;

        if( !rhs->expr.is_bool() )
            return nullopt;
            return false;

        return Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ) };
        b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ) } );
        return true;
    }

    bool BuildZ3Op( Builder& b, const cir::InstrSeq& is )
    {
        for( const auto& instr : is )
        {
            if( !BuildZ3Op( b, instr ) )
                return false;
        }

        return true;
    }

    template< typename T >
    optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
    bool BuildZ3Op( Builder& b, const T& instr )
    {
        return nullopt;
        return false;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
    bool BuildZ3Op( Builder& b, const Load& instr )
    {
        optional< Z3Val > zv;

        if( auto cstAddr = b.pop< Address >() )
            zv = LoadFromAddress( b, *cstAddr, instr.type() );
        else if( auto gfa = b.pop< GhostFuncApplication >() )
        auto zv = LoadFromAddress( b, *instr.addr() );
            zv = LoadFromAddress( b, *gfa );
        else if( auto symAddr = b.pop< Z3Val >() )
            zv = BuildZ3ConstantFromType( b, instr.type(), format( "val{}", b.newUniqueId() ) );

        if( !zv )
            return nullopt;
            return false;

        if( b.mustLoadAssume() )
        ForEachPredicate( b, instr.type(), zv->expr, [&]( auto&& z3expr, auto locId )
        {
            ForEachPredicate( b, instr.type(), zv->expr, [&]( auto&& z3expr, auto locId )
            {
            if( b.mustLoadAssume() )
                b.assume( z3expr );
        } );
            } );

        b.push( move( *zv ) );
        return zv;
        return true;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
    bool BuildZ3Op( Builder& b, const Store& instr )
    {
        auto zv = BuildZ3ExprFromValue( b, instr.val() );
        auto zv = b.pop();
        if( !zv )
            return nullopt;
            return false;

        ForEachPredicate( b, instr.type(), zv->expr, [&]( auto&& z3expr, auto locId )
        {
            if( !instr.destLocId().invalid() && !instr.val().locationId().invalid() )
            if( !instr.srcLocId().invalid() && !instr.destLocId().invalid() )
            {
                DiagnosticsContext dc( instr.destLocId(), "...to this." );
                DiagnosticsContext dc2( instr.val().locationId(), "When assigning this..." );
                DiagnosticsContext dc2( instr.srcLocId(), "When assigning this..." );
                b.checkAssertion( z3expr, locId );
            }
            else
                b.checkAssertion( z3expr, locId );
        } );

        if( auto cstAddr = b.pop< Address >() )
            StoreToAddress( b, *cstAddr, move( *zv ) );
        else if( auto gfa = b.pop< GhostFuncApplication >() )
        StoreToAddress( b, *instr.addr(), move( *zv ) );
        return nullopt;
            StoreToAddress( b, *gfa, move( *zv ) );
        else
            b.pop();

        return true;
    }

    // Implemented in call.cpp
    extern optional< Z3Val > BuildZ3Op( Builder& b, const Call& instr );
    extern bool BuildZ3Op( Builder& b, const Call& instr );

    optional< Z3Val > BuildZ3Op( Builder& b, const CreateTemporary& instr )
    bool BuildZ3Op( Builder& b, const CreateTemporary& instr )
    {
        auto zv = b.pop();
        if( !zv )
            return false;

        b.setVar( instr.index(), instr.value() );
        return nullopt;
        b.setVar( instr.index(), move( *zv ) );
        return true;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const GetTemporary& instr )
    bool BuildZ3Op( Builder& b, const GetTemporary& instr )
    {
        auto zv = b.retrieveVar( instr.index() );
        if( zv )
        {
            b.push( move( *zv ) );
            return zv;

        return BuildZ3ConstantFromType( b, instr.type(), format( "v{}", instr.index() ) );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const AllocVar& instr )
            return true;
        }

        auto result = BuildZ3ConstantFromType( b, instr.type(), format( "v{}", instr.index() ) );
        if( !result )
            return false;

        b.push( move( *result ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const AllocVar& instr )
    {
        auto tinfo = TypeCache::GetInstance()->getTypeInfo( b.context(), ValueToEIR( instr.type() ) );
        if( !tinfo )
            return nullopt;
            return false;

        b.setVar( instr.index(), Z3Val{ tinfo->undefined( b ), instr.type() } );
        return nullopt;
        return true;
    }

    // Implemented in phi.cpp
    optional< Z3Val > BuildZ3Op( Builder& b, const Phi& instr );
    bool BuildZ3Op( Builder& b, const Phi& instr );

    // TODO: LoadConstStr. Build a z3 str value.

    optional< Z3Val > BuildZ3Op( Builder& b, const Not& instr )
    bool BuildZ3Op( Builder& b, const Not& instr )
    {
        return BuildZ3UnaryExpr( b, instr, []( auto&& operand )
        {
            if( operand.is_bool() )
                return !operand;

            assert( operand.is_bv() );
            return ~operand;
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const And& instr )
    bool BuildZ3Op( Builder& b, const And& instr )
    {
        return BuildZ3BinBitwiseExpr( 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;
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Or& instr )
    bool BuildZ3Op( Builder& b, const Or& instr )
    {
        return BuildZ3BinBitwiseExpr( 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;
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Xor& instr )
    bool BuildZ3Op( Builder& b, const Xor& instr )
    {
        return BuildZ3BinBitwiseExpr( 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;
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Implies& instr )
    bool BuildZ3Op( Builder& b, const Implies& instr )
    {
        return BuildZ3BinLogicExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            return z3::implies( lhs, rhs );
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Shl& instr )
    bool BuildZ3Op( Builder& b, const Shl& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::shl( lhsBV, rhsBV );
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const LShr& instr )
    bool BuildZ3Op( Builder& b, const LShr& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::lshr( lhsBV, rhsBV );
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const AShr& instr )
    bool BuildZ3Op( Builder& b, const AShr& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::ashr( lhsBV, rhsBV );
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Add& instr )
    bool BuildZ3Op( Builder& b, const Add& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs + rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Sub& instr )
    bool BuildZ3Op( Builder& b, const Sub& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs - rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Mul& instr )
    bool BuildZ3Op( Builder& b, const Mul& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs * rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const UDiv& instr )
    bool BuildZ3Op( Builder& b, const UDiv& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::udiv( lhs, rhs ); } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const SDiv& instr )
    bool BuildZ3Op( Builder& b, const SDiv& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs / rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const URem& instr )
    bool BuildZ3Op( Builder& b, const URem& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::urem( lhs, rhs ); } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const SRem& instr )
    bool BuildZ3Op( Builder& b, const SRem& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bv() )
                return z3::srem( lhs, rhs );

            return z3::rem( lhs, rhs );
        } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Eq& instr )
    bool BuildZ3Op( Builder& b, const Eq& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs == rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Neq& instr )
    bool BuildZ3Op( Builder& b, const Neq& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs != rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const UGT& instr )
    bool BuildZ3Op( Builder& b, const UGT& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ugt( lhs, rhs ); } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const UGE& instr )
    bool BuildZ3Op( Builder& b, const UGE& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::uge( lhs, rhs ); } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const ULT& instr )
    bool BuildZ3Op( Builder& b, const ULT& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ult( lhs, rhs ); } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const ULE& instr )
    bool BuildZ3Op( Builder& b, const ULE& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ule( lhs, rhs ); } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const SGT& instr )
    bool BuildZ3Op( Builder& b, const SGT& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs > rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const SGE& instr )
    bool BuildZ3Op( Builder& b, const SGE& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs >= rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const SLT& instr )
    bool BuildZ3Op( Builder& b, const SLT& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs < rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const SLE& instr )
    bool BuildZ3Op( Builder& b, const SLE& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs <= rhs; } );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Assert& instr )
    bool BuildZ3Op( Builder& b, const Assert& instr )
    {
        // TODO: refactor the return value here to be able to indicate failure versus "nothing to do"
        auto cond = BuildZ3ExprFromValue( b, instr.cond() );
        if( cond )
            b.checkAssertion( cond->expr, instr.cond().locationId() );
        return nullopt;
        auto cond = b.pop();
        if( !cond )
            return false;

        b.checkAssertion( cond->expr, instr.locationId() );
        return true;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const Placeholder& instr )
    bool BuildZ3Op( Builder& b, const Placeholder& instr )
    {
        const auto* expr = b.retrievePlaceholder( instr.name() );
        if( expr )
        {
            return Z3Val{ *expr, *EIRToValue( instr.type() ) };

        return BuildZ3ConstantFromType( b, instr.type(), format( "p{}", instr.name().str() ) );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const PHOverride& instr )
            b.push( Z3Val{ *expr, *EIRToValue( instr.type() ) } );
            return true;
        }

        auto result = BuildZ3ConstantFromType( b, instr.type(), format( "p{}", instr.name().str() ) );
        if( !result )
            return false;

        b.push( move( *result ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const PHOverrideSet& instr )
    {
        const auto* savedExpr = b.retrievePlaceholder( instr.name() );
        auto phExpr = b.pop();
        if( !phExpr )
            return false;

        auto newExpr = BuildZ3ExprFromValue( b, instr.phVal() );
        if( newExpr )
            b.setPlaceholder( instr.name(), newExpr->expr );
        else
        b.setPlaceholder( instr.name(), phExpr->expr );
        return true;
            b.unsetPlaceholder( instr.name() );

        auto result = BuildZ3ExprFromValue( b, instr.val() );

    }

    bool BuildZ3Op( Builder& b, const PHOverrideClear& instr )
    {
        if( savedExpr )
            b.setPlaceholder( instr.name(), *savedExpr );
        else
            b.unsetPlaceholder( instr.name() );
        b.unsetPlaceholder( instr.name() );

        return result;
        return true;
    }

    bool BuildZ3Op( Builder& b, const Constant& instr )
    {
        auto v = BuildZ3ExprFromValue( b, instr.value() );
        if( v )
            b.push( move( *v ) );
        else
            b.push( instr.value() );
        return true;
    }

    bool BuildZ3Op( Builder& b, const VarAddr& instr )
    {
        b.push( Address( Address::Origin::Stack, instr.varIndex() ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const TempAddr& instr )
    {
        auto initVal = b.pop();
        if( !initVal )
            return false;

        b.push( Address( Address::Origin::Stack, instr.tempIndex() ) );
        return !!b.setVar( instr.tempIndex(), move( *initVal ) );

    optional< Z3Val > BuildZ3Op( Builder& b, const VarAddr& instr )
    }

    bool BuildZ3Op( Builder& b, const Select& instr )
    {
        return Z3Val
        if( auto cstBaseLoc = b.pop< Address >() )
        {
            GetZ3Context().int_val( instr.varIndex() ).unit(),
            b.push( Address::Select( move( *cstBaseLoc ), instr.memberIndex() ) );
            *EIRToValue( GetValueType< builtins::MemLoc >() )
        };
    }
            return true;
        }

    optional< Z3Val > BuildZ3Op( Builder& b, const TempAddr& instr )
    {
        return Z3Val
        auto symBaseLoc = b.pop();
        if( !symBaseLoc )
            return false;

        b.push( Z3Val
        {
            GetZ3Context().int_val( instr.tempIndex() ).unit(),
            z3::concat( symBaseLoc->expr, GetZ3Context().int_val( instr.memberIndex() ).unit() ),
            *EIRToValue( GetValueType< builtins::MemLoc >() )
        };
    }
        } );

        return true;
    }

    bool BuildZ3Op( Builder& b, const GhostCall& instr )
    {
        auto func = b.pop< Value >();
        if( !func )
            return false;

        auto argCount = instr.numArgs();
        llvm::SmallVector< Z3Val, 16 > args;
        args.reserve( argCount );
    optional< Z3Val > BuildZ3Op( Builder& b, const Select& instr )
    {
        auto baseLoc = BuildZ3Op( b, *instr.baseAddr() );
        if( !baseLoc )
            return nullopt;

        for( uint32_t argIndex = 0; argIndex < argCount; ++argIndex )
        {
            auto zv = b.pop();
            if( !zv )
                return false;

            args.emplace_back( move( *zv ) );
        }
        return Z3Val
        {
            z3::concat( baseLoc->expr, GetZ3Context().int_val( instr.memberIndex() ).unit() ),

        GhostFuncApplication gfa( move( *func ) );

        gfa.args().reserve( args.size() );
        for( auto it = args.rbegin(); it != args.rend(); ++it )
            gfa.args().emplace_back( move( *it ) );

            *EIRToValue( GetValueType< builtins::MemLoc >() )
        };
        b.push( move( gfa ) );
        return true;
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const cir::Instruction& instr )
    bool BuildZ3Op( Builder& b, const cir::Instruction& instr )
    {
        return visit( [&]( auto&& e )
        {
            return BuildZ3Op( b, e );
        }, instr.content() );
    }

    optional< Z3Val > BuildZ3ExprFromValue( Builder& b, const Value& val )
    {
        if( val.isPoison() )
            return nullopt;

        if( val.isConstant() )
            return BuildZ3ValFromConstant( b, val );

        if( auto expr = BuildZ3Op( b, *val.cir() )  )
            return expr;
        if( BuildZ3Op( b, *val.cir() ) )
            return b.pop();

        return BuildZ3ConstantFromType( b, val.type(), format( "val{}", b.newUniqueId() ) );
    }
}