Goose  Diff

        auto retExpr = BuildZ3ConstantFromType( b, ft.returnType(), format( "r{}", b.newUniqueId() ) );

        // Create a temporary builder to construct the z3 expressions out of the
        // function's pre-conditions and postconditions, configured
        // to perform the necessary replacements for arguments and for the
        // return value placeholder.
        Builder cb( b.context(), *b.solver(), b.remapper() );
        Builder cb = b;
        cb.setAssertionHandler( b.assertionHandler() );
        cb.setCurrentPredicate( b.currentPredicate() );
        cb.setLoadMustAssume( false );

        // Inject the arguments in the context.
        // They will be picked up by getVars instructions when refered to
        // by the verification conditions.
        uint32_t index = 0;